(* Auxiliary antiquotations for the Cookbook. *)

structure AntiquoteSetup: sig end =
struct

(* rebuilding the output_list function from ThyOutput in order to *)
(* enable the option [gray] *)

val gray = ref false;

fun boolean "" = true
  | boolean "true" = true
  | boolean "false" = false
  | boolean s = error ("Bad boolean value: " ^ quote s);

fun output_list pretty src ctxt xs =
  map (pretty ctxt) xs        (*always pretty in order to exhibit errors!*)
  |> (if ! ThyOutput.source then K [ThyOutput.pretty_text (ThyOutput.str_of_source src)] else I)
  |> (if ! ThyOutput.quotes then map Pretty.quote else I)
  |> (if ! ThyOutput.display then
    map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
    #> space_implode "\\isasep\\isanewline%\n"
    #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I) 
    #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
 else
    map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
    #> space_implode "\\isasep\\isanewline%\n"
    #> enclose "\\isa{" "}");

val _ = ThyOutput.add_options
 [("gray", Library.setmp gray o boolean)]


(* main body *)
fun ml_val_open (ys, xs) txt = 
  let fun ml_val_open_aux ys txt = 
          "fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
  in
    (case xs of
       [] => ml_val_open_aux ys txt
     | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
  end;

fun ml_val txt = ml_val_open ([],[]) txt;

fun ml_pat (rhs, pat) =
  let 
     val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))
  in "val " ^ pat' ^ " = " ^ rhs end;

fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";

val transform_cmts_str =
  Source.of_string #> ML_Lex.source #> Source.exhaust #>
  Chunks.transform_cmts #> implode;

fun output_ml ml src ctxt ((txt,ovars),pos) =
  (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt);
   txt |> transform_cmts_str |> space_explode "\n" |>
   output_list (fn _ => fn s => Pretty.str s) src ctxt)

fun output_ml_aux ml src ctxt (txt,pos) =
  output_ml (K ml) src ctxt ((txt,()),pos) 

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 output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)

fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = 
  (ML_Context.eval_in (SOME ctxt) false pos (ml lhs);
  let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
  in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)

fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) = 
  let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
  in output_list (fn _ => fn s => Pretty.str s) src ctxt txt end

fun check_file_exists ctxt txt =
  if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
  else error ("Source file " ^ quote txt ^ " does not exist.")

val _ = ThyOutput.add_commands
  [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
      (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
       Scan.optional (Args.$$$ "in"  |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) 
                                                                 (output_ml ml_val_open)),
   ("ML_file", ThyOutput.args (Scan.lift Args.name)
      (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))),
   ("ML_text", ThyOutput.args (Scan.lift Args.name)
      (ThyOutput.output (fn _ => fn s => Pretty.str s))),
   ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
      (output_ml_response ml_pat)),
   ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
      (output_ml_response_fake ml_val)),
   ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
      (output_ml_response_fake_both ml_val)),
   ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
   ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))];
   
end;