theory Antiquotes
imports "../Base"
begin


section {* 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 _ = " ^ 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. 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 + 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