--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Wed Oct 29 21:51:25 2008 +0100
@@ -0,0 +1,124 @@
+
+theory Antiquotes
+imports Main
+begin
+
+
+section {* Two Document Antiquotations *}
+
+text {*
+
+  For writing documents using Isabelle it is often uesful to use
+  document antiquotations. Below we give the code for such an 
+  antiquotation that typesets ML-code and also checks whether
+  the code is actually correct. In this way one can achieve that the
+  document is always in sync with code.
+
+  Below we introduce the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which
+  takes a piece of code as argument. We will check this code by sending 
+  the ML-expression @{text "val _ = \<dots>"} to the ML-compiler (i.e.~the 
+  function @{ML "ML_Context.eval_in"}). The code for this antiquotation
+  is as follows:
+*}
+
+ML {*
+fun ml_val txt = "val _ = " ^ txt
+
+fun output_ml ml src ctxt txt =
+  (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt);
+  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
+
+val _ = ThyOutput.add_commands
+ [("ML_checked", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val))]
+*}
+
+text {*
+  
+  Note that the parser @{ML "(Scan.lift Args.name)"} parses a string. If the
+  code is approved by the compiler, the output function 
+  @{ML "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"}
+  pretty prints the code. There are a number of options that are observed
+  when printing the code (for example @{text "[display]"}; for more information
+  about the options see \rsccite{sec:antiq}).
+
+  Since we
+  used the argument @{ML "Position.none"}, the compiler cannot give specific 
+  information about the line number where an error might have occurred. We 
+  can improve this code slightly by writing 
+
+*}
+
+ML {*
+fun output_ml ml src ctxt (txt,pos) =
+  (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
+  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))
+
+val _ = ThyOutput.add_commands
+ [("ML_checked", ThyOutput.args 
+       (Scan.lift (OuterParse.position Args.name)) (output_ml ml_val))]
+*}
+
+text {*
+  where the antiquotation can also handle position information.
+
+  (FIXME: say something about OuterParse.position)
+
+*}
+
+ML {*
+
+fun ml_pat (rhs, pat) =
+  let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
+  in
+    "val " ^ pat' ^ " = " ^ rhs
+  end;
+
+fun add_response_indicator txt =
+  map (fn s => "> " ^ 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)
+  in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+
+*}
+
+
+(*
+val _ = ThyOutput.add_commands
+ [("ML_response", 
+      ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
+      (output_ml_response ml_pat)]
+*)
+
+
+ML {*
+
+let 
+  val i = 1 + 2
+in
+  i * i
+end
+
+*}
+
+(*
+A test: 
+
+@{ML_response [display] "true andalso false" "false"} 
+
+@{ML_response [display]
+"let 
+  val i = 1 + 2
+in
+  i * i
+end" "9"}
+*)
+
+
+
+end
+  
+
+
+