--- a/ProgTutorial/antiquote_setup.ML	Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Thu Aug 20 14:19:39 2009 +0200
@@ -6,17 +6,18 @@
 open OutputTutorial
 
 (* functions for generating appropriate expressions *)
-fun ml_val_open ys strct txt = 
+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 strct of
+ (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 ml_val txt = ml_val_open [] NONE txt;
+fun ml_val_ind istruct txt = ml_val_open [] istruct txt;
 
 fun ml_pat (lhs, pat) =
   let 
@@ -42,17 +43,24 @@
   #> implode 
   #> string_explode ""
 
-(* checks and prints open expressions, calculates index entry *)
+(* 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);
+  (eval_fn ctxt (ml_val_open ovars istruc txt); output (string_explode "" 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})
 
-val parser_ml = Scan.lift (Args.name --
-  (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-   Scan.option (Args.$$$ "in"  |-- OuterParse.!!! Args.name))) 
+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 = 
@@ -81,6 +89,7 @@
 val two_args   = Scan.lift (Args.name -- Args.name)
 
 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_struct" single_arg output_struct
 val _ = ThyOutput.antiquotation "ML_response" two_args output_response