imports "../Base"

section {* Useful Document Antiquotations *}

  {\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:

  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 

                                            (space_explode "\n" txt))

  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 

  The second 

  ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 

                                            (space_explode "\n" txt))

  let val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))