--- a/ProgTutorial/antiquote_setup.ML	Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Sat May 30 17:40:20 2009 +0200
@@ -1,10 +1,12 @@
 (* Auxiliary antiquotations for the tutorial. *)
 
-structure AntiquoteSetup: sig end =
+structure AntiquoteSetup =
 struct
 
+open OutputTutorial
+
 (* functions for generating appropriate expressions *)
-fun ml_val_open (ys, xs) txt = 
+fun ml_val_open ys xs txt = 
   let fun ml_val_open_aux ys txt = 
           "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
   in
@@ -13,7 +15,7 @@
      | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
   end;
 
-fun ml_val txt = ml_val_open ([],[]) txt;
+fun ml_val txt = ml_val_open [] [] txt;
 
 fun ml_pat (lhs, pat) =
   let 
@@ -28,8 +30,8 @@
   ML_Context.eval_in (SOME ctxt) false Position.none exp
 
 (* string functions *)
-fun string_explode str txt =
-  map (fn s => str ^ s) (space_explode "\n" txt)
+fun string_explode prefix_str txt =
+  map (fn s => prefix_str ^ s) (split_lines txt)
 
 val transform_cmts_str =
      Source.of_string 
@@ -37,45 +39,49 @@
   #> Source.exhaust 
   #> Chunks.transform_cmts 
   #> implode 
-  #> string_explode "";
-
-(* output function *)
-fun output_fn txt =  OutputFN.output txt
+  #> string_explode ""
 
 (* checks and prints open expressions *)
-fun output_ml {context = ctxt, ...} (txt, ovars) =
-  (eval_fn ctxt (ml_val_open ovars txt);
-   output_fn (transform_cmts_str txt))
+fun output_ml {context = ctxt, ...} (txt, (ovars, structs)) =
+  (eval_fn ctxt (ml_val_open ovars structs txt);
+   if structs = []
+   then output_indexed (transform_cmts_str txt) {main = Code txt, minor = ""}
+   else output_indexed (transform_cmts_str txt) 
+             {main = Code txt, minor = ("in {\\tt\\slshape{}" ^ (implode structs) ^ "}")})
 
 val parser_ml = Scan.lift (Args.name --
   (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
    Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])) 
 
 (* checks and prints types and structures *)
-fun output_exp ml {context = ctxt, ...} txt = 
-  (eval_fn ctxt (ml txt);
-   output_fn (string_explode "" txt))
+fun output_struct {context = ctxt, ...} txt = 
+  (eval_fn ctxt (ml_struct txt);
+   output_indexed (string_explode "" txt) {main = Code txt, minor = "structure"})
+
+fun output_type {context = ctxt, ...} txt = 
+  (eval_fn ctxt (ml_type txt);
+   output_indexed (string_explode "" txt) {main = Code txt, minor = "type"})
 
 (* checks and expression agains a result pattern *)
 fun output_response {context = ctxt, ...} (lhs, pat) = 
     (eval_fn ctxt (ml_pat (lhs, pat));
-     output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
+     output ((string_explode "" lhs) @ (string_explode "> " 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_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
+     output ((string_explode "" lhs) @ (string_explode "> " pat)))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun ouput_response_fake_both _ (lhs, pat) = 
-    output_fn ((string_explode "" lhs) @ (string_explode "> " pat))
+    output ((string_explode "" lhs) @ (string_explode "> " pat))
 
 val single_arg = Scan.lift (Args.name)
 val two_args   = Scan.lift (Args.name -- Args.name)
 
 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
-val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type)
-val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct)
+val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
+val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
 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
@@ -91,7 +97,7 @@
 (* 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_fn [href_link txt]
+   then output [href_link txt]
    else error ("Source file " ^ (quote txt) ^ " does not exist."))
 
 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists