diff -r 81e2d73f7191 -r 4daf913fdbe1 CookBook/Recipes/Antiquotes.thy --- a/CookBook/Recipes/Antiquotes.thy Wed Oct 29 21:51:25 2008 +0100 +++ b/CookBook/Recipes/Antiquotes.thy Thu Oct 30 13:36:51 2008 +0100 @@ -1,24 +1,31 @@ theory Antiquotes -imports Main +imports "../Base" begin -section {* Two Document Antiquotations *} +section {* Useful Document Antiquotations *} text {* + {\bf Problem:} + How to keep ML-code included in a document in sync with the actual code.\smallskip - 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. + {\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 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: + 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 {* @@ -26,7 +33,8 @@ 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)) + 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))] @@ -37,21 +45,25 @@ 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}). + 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 + 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)) + ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt + (space_explode "\n" txt)) val _ = ThyOutput.add_commands [("ML_checked", ThyOutput.args @@ -59,16 +71,12 @@ *} 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)) + let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) in "val " ^ pat' ^ " = " ^ rhs end; @@ -80,7 +88,6 @@ (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) - *}