(*
Auxiliary antiquotations for the Cookbook.

*)

structure AntiquoteSetup: sig end =
struct

val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src;

fun ml_val ys txt = "fn " ^
  (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^
  " => (" ^ txt ^ ");";

fun ml_val_open (ys, []) txt = ml_val ys txt
  | ml_val_open (ys, xs) txt =
      ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end");

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

(* modified from original *)
fun ml_val txt = "fn _ => (" ^ txt ^ ");";
fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;";
fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";

fun output_verbatim f src ctxt x =
  let val txt = f ctxt x
  in
    (if ! ThyOutput.source then str_of_source src else txt)
    |> (if ! ThyOutput.quotes then quote else I)
    |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt
  end;

fun output_ml_old ml = output_verbatim
  (fn ctxt => fn ((txt, p), pos) =>
     (ML_Context.eval_in (SOME ctxt) false pos (ml p txt);
      txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |>
      Chunks.transform_cmts |> implode));

fun output_ml ml src ctxt txt =
  (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt);
  ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt)

fun add_response_indicator txt =
  space_implode "\n" (map (fn s => "> " ^ s) (space_explode "\n" txt))

fun output_ml_response ml src ctxt (lhs,pat) = 
  (ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat));
  let val txt = lhs ^ "\n" ^ (add_response_indicator pat)
  in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end)

fun output_ml_response_fake ml src ctxt (lhs,pat) = 
  (ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs);
  let val txt = lhs ^ "\n" ^ (add_response_indicator pat)
  in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end)

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



val _ = ThyOutput.add_commands
  [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name --
      (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
       Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_old 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", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val)),
   ("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)),
   ("ML_response_fake", 
           ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)),
   ("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)),
   ("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))];
   
end;