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