--- a/CookBook/antiquote_setup.ML	Thu Feb 12 16:35:05 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Fri Feb 13 01:05:09 2009 +0000
@@ -3,7 +3,8 @@
 structure AntiquoteSetup: sig end =
 struct
 
-(* main body *)
+(* functions for generating appropriate expressions *)
+
 fun ml_val_open (ys, xs) txt = 
   let fun ml_val_open_aux ys txt = 
           "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
@@ -15,49 +16,91 @@
 
 fun ml_val txt = ml_val_open ([],[]) txt;
 
-fun ml_pat (rhs, pat) =
+fun ml_pat (lhs, pat) =
   let 
      val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
-  in "val " ^ pat' ^ " = " ^ rhs end;
+  in "val " ^ pat' ^ " = " ^ lhs end;
 
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
 
-val transform_cmts_str =
-  Source.of_string #> ML_Lex.source #> Source.exhaust #>
-  Chunks.transform_cmts #> implode;
+(* eval function *)
+fun eval_fn ctxt pos exp =
+  ML_Context.eval_in (SOME ctxt) false pos exp
 
-fun output_ml ml src ctxt ((txt,ovars),pos) =
-  (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);
-   txt |> transform_cmts_str |> space_explode "\n" |>
-   Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt)
-
-fun output_ml_aux ml src ctxt (txt,pos) =
-  output_ml (K ml) src ctxt ((txt,()),pos) 
-
+(* string functions *)
 fun string_explode str txt =
   map (fn s => str ^ s) (space_explode "\n" txt)
 
-fun output_ml_response ml src ctxt ((lhs,pat),pos) = 
-  (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat));
-  let 
-      val txt = (string_explode "" lhs) @ (string_explode "> " pat)
-  in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+val transform_cmts_str =
+     Source.of_string 
+  #> ML_Lex.source 
+  #> Source.exhaust 
+  #> Chunks.transform_cmts 
+  #> implode 
+  #> string_explode "";
+
+(* parser for single and two arguments *)
+val single_arg = Scan.lift (OuterParse.position Args.name)
+val two_args = Scan.lift (OuterParse.position (Args.name -- Args.name))
+
+(* output function *)
+val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s)
+
+(* checks and prints open expressions *)
+fun output_ml src node =
+let
+  fun output src ctxt ((txt,ovars),pos) =
+    (eval_fn ctxt pos (ml_val_open ovars txt);
+     output_fn src ctxt (transform_cmts_str txt))
+
+  val parser = Scan.lift (OuterParse.position (Args.name --
+      (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
+       Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) 
+in
+  ThyOutput.args parser output src node
+end
 
-fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = 
-  (ML_Context.eval_in (SOME ctxt) false pos (ml lhs);
-  let val txt = (string_explode "" lhs) @ (string_explode "> " pat)
-  in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+(* checks and prints types and structures *)
+fun output_exp ml src node =
+let 
+  fun output src ctxt (txt,pos) = 
+    (eval_fn ctxt pos (ml txt);
+     output_fn src ctxt (string_explode "" txt))
+in
+  ThyOutput.args single_arg output src node
+end
 
+(* checks and expression agains a result pattern *)
+fun output_ml_response src node =
+let
+  fun output src ctxt ((lhs,pat),pos) = 
+    (eval_fn ctxt pos (ml_pat (lhs,pat));
+     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
+in
+  ThyOutput.args two_args output src node
+end
+
+(* checks the expressions, but does not check it against a result pattern *)
+fun output_ml_response_fake src node =
+let
+  fun output src ctxt ((lhs,pat),pos) = 
+    (eval_fn ctxt pos (ml_val lhs);
+     output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
+in
+  ThyOutput.args two_args output src node
+end
+
+(* just prints an expression and a result pattern *)
 fun output_ml_response_fake_both src node =
 let 
-  fun ouput src ctxt (lhs,pat) = 
-    Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt 
-     ((string_explode "" lhs) @ (string_explode "> " pat))
+  fun ouput src ctxt ((lhs,pat), _) = 
+    output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))
 in
-  ThyOutput.args (Scan.lift (Args.name -- Args.name)) ouput src node
+  ThyOutput.args two_args ouput src node
 end
 
+(* checks whether a file exists in the Isabelle distribution *)
 fun check_file_exists src node =
 let 
   fun check txt =
@@ -94,20 +137,14 @@
    (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node
 end
 
-
 val _ = ThyOutput.add_commands
-  [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
-      (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
-       Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) 
-                                                                 (output_ml ml_val_open)),
+  [("ML", output_ml),
    ("ML_file", check_file_exists),
-   ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
-      (output_ml_response ml_pat)),
-   ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
-      (output_ml_response_fake ml_val)),
+   ("ML_response", output_ml_response),
+   ("ML_response_fake", output_ml_response_fake),
    ("ML_response_fake_both", output_ml_response_fake_both),
-   ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
-   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)),
+   ("ML_struct", output_exp ml_struct),
+   ("ML_type", output_exp ml_type),
    ("subgoals", output_goals)];
    
 end;