--- a/ProgTutorial/Advanced.thy	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/Advanced.thy	Tue Jun 28 09:22:00 2011 +0100
@@ -287,7 +287,6 @@
 *}
 
 text {* 
-  @{ML_ind "Binding.str_of"} returns the string with markup;
   @{ML_ind "Binding.name_of"} returns the string without markup
 
   @{ML_ind "Binding.conceal"} 

--- a/ProgTutorial/Base.thy	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/Base.thy	Tue Jun 28 09:22:00 2011 +0100
@@ -150,5 +150,7 @@
 use "output_tutorial.ML"
 use "antiquote_setup.ML"
 
+setup {* OutputTutorial.setup *}
+setup {* AntiquoteSetup.setup *}
 
 end
\ No newline at end of file

--- a/ProgTutorial/First_Steps.thy	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/First_Steps.thy	Tue Jun 28 09:22:00 2011 +0100
@@ -852,7 +852,8 @@
   for the antiquotation @{text "term_pat"} is as follows.
 *}
 
-ML %linenosgray{*let
+ML %linenosgray{*val term_pat_setup = 
+let
   val parser = Args.context -- Scan.lift Args.name_source
 
   fun term_pat (ctxt, str) =
@@ -860,9 +861,11 @@
          |> ML_Syntax.print_term
          |> ML_Syntax.atomic
 in
-  ML_Antiquote.inline "term_pat" (parser >> term_pat)
+  ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
 end*}
 
+setup{* term_pat_setup *}
+
 text {*
   The parser in Line 2 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind read_term_pattern in
@@ -878,7 +881,8 @@
   we can write an antiquotation for type patterns.
 *}
 
-ML{*let
+ML{*val type_pat_setup = 
+let
   val parser = Args.context -- Scan.lift Args.name_source
 
   fun typ_pat (ctxt, str) =
@@ -886,9 +890,11 @@
          |> ML_Syntax.print_typ
          |> ML_Syntax.atomic
 in
-  ML_Antiquote.inline "typ_pat" (parser >> typ_pat)
+  ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
 end*}
 
+setup{* type_pat_setup *}
+
 text {*
   \begin{readmore}
   The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions

--- a/ProgTutorial/Recipes/Antiquotes.thy	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Tue Jun 28 09:22:00 2011 +0100
@@ -46,7 +46,9 @@
   (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); 
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
+val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*}
+
+setup {* ml_checked_setup *}
 
 text {*
   The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this
@@ -77,16 +79,18 @@
   (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt);
    Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
 
-val _ = Thy_Output.antiquotation "ML_checked"
+val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"}
          (Scan.lift (Parse.position Args.name)) output_ml *}
 
+setup {* ml_checked_setup2 *}
+
 text {*
   where in Lines 1 and 2 the positional information is properly treated. The
   parser @{ML Parse.position} encodes the positional information in the 
   result.
 
-  We can now write @{text "@{ML_checked \"2 + 3\"}"} in a document in order to
-  obtain @{ML_checked "2 + 3"} and be sure that this code compiles until
+  We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to
+  obtain @{ML_checked2 "2 + 3"} and be sure that this code compiles until
   somebody changes the definition of addition.
 
 
@@ -102,7 +106,7 @@
   give a partial specification by using ellipses. For example @{text "(\<dots>, \<dots>)"}
   for specifying a pair.  In order to check consistency between the pattern
   and the output of the code, we have to change the ML-expression that is sent 
-  to the compiler: in @{text "ML_checked"} we sent the expression @{text [quotes]
+  to the compiler: in @{text "ML_checked2"} we sent the expression @{text [quotes]
   "val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"}
   must be be replaced by the given pattern. However, we have to remove all
   ellipses from it and replace them by @{text [quotes] "_"}. The following 
@@ -136,12 +140,14 @@
      Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) 
    end)
 
-val _ = Thy_Output.antiquotation "ML_resp" 
+val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} 
           (Scan.lift (Parse.position (Args.name -- Args.name))) 
              output_ml_resp*}
 
+setup {* ml_resp_setup *}
+
 text {*
-  In comparison with @{text "ML_checked"}, we only changed the line about 
+  In comparison with @{text "ML_checked2"}, we only changed the line about 
   the compiler (Line~2), the lines about
   the output (Lines 4 to 7) and the parser in the setup (Line 11). Now 
   you can write

--- a/ProgTutorial/antiquote_setup.ML	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Tue Jun 28 09:22:00 2011 +0100
@@ -98,17 +98,18 @@
 val two_args   = Scan.lift (Args.name -- Args.name)
 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
-val _ = Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml
-val _ = Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind
-val _ = Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type
-val _ = Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind
-val _ = Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct
-val _ = Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind
-val _ = Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct
-val _ = Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind
-val _ = Thy_Output.antiquotation @{binding "ML_response"} two_args output_response
-val _ = Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake
-val _ = Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
+val ml_setup = 
+  Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml
+  #> Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind
+  #> Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type
+  #> Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind
+  #> Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct
+  #> Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind
+  #> Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct
+  #> Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind
+  #> Thy_Output.antiquotation @{binding "ML_response"} two_args output_response
+  #> Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake
+  #> Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
 
 (* FIXME: experimental *)
 fun ml_eq (lhs, pat, eq) =
@@ -120,7 +121,8 @@
      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
      output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
-val _ = Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq
+val ml_response_setup = 
+  Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq
 
 (* checks whether a file exists in the Isabelle distribution *)
 fun href_link txt =
@@ -136,7 +138,7 @@
    then output ctxt [href_link txt]
    else error (implode ["Source file ", quote txt, " does not exist."]))
 
-val _ = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists
+val ml_file_setup = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists
 
 
 (* replaces the official subgoal antiquotation with one *)
@@ -176,7 +178,16 @@
   Thy_Output.output ctxt output
 end
 
-val _ = Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals
-val _ = Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
+val subgoals_setup = 
+  Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals
+val raw_goal_state_setup = 
+  Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
+
+val setup =
+  ml_setup #>
+  ml_response_setup #>
+  ml_file_setup #>
+  subgoals_setup #>
+  raw_goal_state_setup
 
 end;

--- a/ProgTutorial/output_tutorial.ML	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/output_tutorial.ML	Tue Jun 28 09:22:00 2011 +0100
@@ -84,9 +84,13 @@
   | boolean "false" = false
   | boolean s = error ("Bad boolean value: " ^ quote s);
 
-val _ = Thy_Output.add_option @{binding "gray"} 
+val gray_setup = Thy_Output.add_option @{binding "gray"} 
   (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
-val _ = Thy_Output.add_option @{binding "linenos"}  
+val linenos_setup = Thy_Output.add_option @{binding "linenos"}  
   (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean)
 
+val setup =
+  gray_setup #>
+  linenos_setup 
+
 end
\ No newline at end of file

Binary file progtutorial.pdf has changed