diff -r de49d5780f57 -r 74f0a06f751f ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Thu Aug 20 22:30:20 2009 +0200
@@ -6,84 +6,84 @@
 open OutputTutorial
 
 (* functions for generating appropriate expressions *)
-fun ml_val_open ys istruct txt = 
-let 
-  fun ml_val_open_aux ys txt = 
-    implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"];
-in
- (case istruct of
-    NONE    => ml_val_open_aux ys txt
-  | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
-end
+fun translate_string f str =
+  implode (map f (Symbol.explode str))
+
+fun prefix_lines prfx txt = 
+  map (fn s => prfx ^ s) (split_lines txt)
 
-fun ml_val txt = ml_val_open [] NONE txt;
-fun ml_val_ind istruct txt = ml_val_open [] istruct txt;
+fun ml_with_vars ys txt = 
+    implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]
+
+fun ml_with_struct (NONE) txt = txt 
+  | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"]
+
+fun ml_val vs stru txt = 
+    txt |> ml_with_struct stru
+        |> ml_with_vars  vs 
 
 fun ml_pat (lhs, pat) =
-  let 
-     val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
-  in "val " ^ pat' ^ " = " ^ lhs end;
+  implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs] 
 
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
+fun ml_struct txt = 
+  implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"]
+
+fun ml_type txt = 
+  implode ["val _ = NONE : (", txt, ") option"];
 
 (* eval function *)
 fun eval_fn ctxt exp =
   ML_Context.eval_in (SOME ctxt) false Position.none exp
 
-(* string functions *)
-fun string_explode prefix_str txt =
-  map (fn s => prefix_str ^ s) (split_lines txt)
-
-val transform_cmts_str =
-     Source.of_string 
-  #> ML_Lex.source 
-  #> Source.exhaust 
-  #> Chunks.transform_cmts 
-  #> implode 
-  #> string_explode ""
-
 (* checks and prints a possibly open expressions, no index *)
-fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) =
-  (eval_fn ctxt (ml_val_open ovars istruc txt); output (string_explode "" txt))
+fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
+  (eval_fn ctxt (ml_val vs stru txt); 
+   output (split_lines txt))
 
 val parser_ml = Scan.lift (Args.name --
   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
    Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 
 
-(* checks and prinds a single entity, with index *)
-fun output_ml_ind {context = ctxt, ...} (txt, istruc) =
-  (eval_fn ctxt (ml_val_ind istruc txt); 
-   case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt)  of
-     (NONE, bn, "")  => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
-   | (NONE, bn, qn)  => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn}
-   | (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st})
+(* checks and prints a single ML-item and produces an index entry *)
+fun output_ml_ind {context = ctxt, ...} (txt, stru) =
+  (eval_fn ctxt (ml_val [] stru txt); 
+   case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
+     (NONE, bn, "")  => output_indexed {main = Code txt, minor = NoString} (split_lines txt)
+   | (NONE, bn, qn)  => output_indexed {main = Code bn,  minor = Struct qn} (split_lines txt)
+   | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt))
 
 val parser_ml_ind = Scan.lift (Args.name --
   Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))
 
-(* checks and prints types and structures *)
-fun output_struct {context = ctxt, ...} txt = 
-  (eval_fn ctxt (ml_struct txt);
-   output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"})
+(* checks and prints structures *)
+fun gen_output_struct outfn {context = ctxt, ...} txt = 
+  (eval_fn ctxt (ml_struct txt); 
+   outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
+
+val output_struct = gen_output_struct (K output)
+val output_struct_ind = gen_output_struct output_indexed
 
-fun output_type {context = ctxt, ...} txt = 
-  (eval_fn ctxt (ml_type txt);
-   output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "type"})
+(* checks and prints types *)
+fun gen_output_type outfn {context = ctxt, ...} txt = 
+  (eval_fn ctxt (ml_type txt); 
+   outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
+
+val output_type = gen_output_type (K output)
+val output_type_ind = gen_output_type output_indexed
 
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_pat (lhs, pat));
-     output ((string_explode "" lhs) @ (string_explode "> " pat)))
+     output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake {context = ctxt, ...} (lhs, pat) = 
-    (eval_fn ctxt (ml_val lhs);
-     output ((string_explode "" lhs) @ (string_explode "> " pat)))
+    (eval_fn ctxt (ml_val [] NONE lhs);
+     output ((split_lines lhs) @ (prefix_lines "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun ouput_response_fake_both _ (lhs, pat) = 
-    output ((string_explode "" lhs) @ (string_explode "> " pat))
+    output ((split_lines lhs) @ (prefix_lines "> " pat))
 
 val single_arg = Scan.lift (Args.name)
 val two_args   = Scan.lift (Args.name -- Args.name)
@@ -91,7 +91,9 @@
 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind
 val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
+val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind
 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
+val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
 val _ = ThyOutput.antiquotation "ML_response" two_args output_response
 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
@@ -101,14 +103,15 @@
   val raw = Symbol.encode_raw
   val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
 in
- (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}")
+ implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
 end 
 
 (* checks whether a file exists in the Isabelle distribution *)
 fun check_file_exists _ txt =
   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
    then output [href_link txt]
-   else error ("Source file " ^ (quote txt) ^ " does not exist."))
+   else error (implode ["Source file ", quote txt, " does not exist."]))
+
 
 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
 
@@ -150,7 +153,6 @@
   ThyOutput.output output
 end
 
-
 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
 val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state