Mercurial Mercurial > hg > isabelle-cookbook / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
further cleanup
authorChristian Urban <urbanc@in.tum.de>
Sat, 07 Feb 2009 14:21:33 +0000
changeset 103 fe10da5354a3
parent 102 5e309df58557
child 104 5dcad9348e4d
further cleanup
CookBook/antiquote_setup.ML file | annotate | diff | comparison | revisions
cookbook.pdf file | annotate | diff | comparison | revisions 
--- a/CookBook/antiquote_setup.ML	Sat Feb 07 12:05:02 2009 +0000
+++ b/CookBook/antiquote_setup.ML	Sat Feb 07 14:21:33 2009 +0000
@@ -35,23 +35,28 @@
 fun output_ml_aux ml src ctxt (txt,pos) =
   output_ml (K ml) src ctxt ((txt,()),pos) 
 
-fun add_response_indicator txt =
-  map (fn s => "> " ^ s) (space_explode "\n" txt)
+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 = (space_explode "\n" lhs) @ (add_response_indicator pat)
+      val txt = (string_explode "" lhs) @ (string_explode "> " pat)
   in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt 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 = (space_explode "\n" lhs) @ (add_response_indicator pat)
+  let val txt = (string_explode "" lhs) @ (string_explode "> " pat)
   in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
 
-fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = 
-  let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
-  in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
+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))
+in
+  ThyOutput.args (Scan.lift (Args.name -- Args.name)) ouput src node
+end
 
 fun check_file_exists src node =
 let 
@@ -100,8 +105,7 @@
       (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_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
-      (output_ml_response_fake_both ml_val)),
+   ("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)),
    ("subgoals", output_goals)];
Binary file cookbook.pdf has changed
isabelle-cookbook