hakked latex so that it does not display ML {* *}; general tuning
theory Antiquotesimports "../Base"beginsection {* Useful Document Antiquotations *}text {* {\bf Problem:} How to keep ML-code included in a document in sync with the actual code.\smallskip {\bf Solution:} This can be achieved using document antiquotations.\smallskip Document antiquotations are a convenient method for type-setting consitently a group of items in a document. They can also be used for sophisticated \LaTeX hacking. Below we give the code for two such antiquotations that can be used to typeset ML-code and also to check whether the code is actually compiles. In this way one can relatively easily keep documents in sync with code. We first describe the antiquotation @{text "@{ML_checked \"\<dots>\"}"} which takes a piece of code as argument. This code is checked by sending the ML-expression @{text "val _ = \<dots>"} containing the given code 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 _ = " ^ txtfun 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. This function expects that the code is a list of strings according to the line breaks (therefore the @{ML_open "(space_explode \"\\n\" txt)" for txt} which produces this list). There are a number of options that are observed by @{ML ThyOutput.output_list} when printing the code (for example @{text "[display]"} and @{text "[source]"}; for more information about these 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 The second *}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 {* (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 + 2in i * iend*}(*A test: @{ML_response [display] "true andalso false" "false"} @{ML_response [display]"let val i = 1 + 2in i * iend" "9"}*)end