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