1 (* Auxiliary antiquotations for the Cookbook. *)

     2 

     3 structure AntiquoteSetup: sig end =

     4 struct

     5 

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

     7 

     8 fun ml_val_open (ys, xs) txt = 

     9   let fun ml_val_open_aux ys txt = 

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

    11   in

    12     (case xs of

    13        [] => ml_val_open_aux ys txt

    14      | _  => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))

    15   end;

    16 

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

    18 

    19 fun ml_pat (rhs, pat) =

    20   let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat))

    21   in

    22     "val " ^ pat' ^ " = " ^ rhs

    23   end;

    24 

    25 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";

    26 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";

    27 fun ml_decl txt = txt

    28 

    29 fun output_ml_open ml src ctxt (txt,ovars) =

    30   (ML_Context.eval_in (SOME ctxt) false Position.none (ml ovars txt);

    31   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt))

    32 

    33 fun output_ml ml src ctxt txt =

    34   output_ml_open (K ml) src ctxt (txt,()) 

    35 

    36 fun add_response_indicator txt =

    37   map (fn s => "> " ^ s) (space_explode "\n" txt)

    38 

    39 fun output_ml_response ml src ctxt (lhs,pat) = 

    40   (ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat));

    41   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)

    42   in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)

    43 

    44 fun output_ml_response_fake ml src ctxt (lhs,pat) = 

    45   (ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs);

    46   let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)

    47   in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)

    48 

    49 fun check_file_exists ctxt name =

    50   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then ()

    51   else error ("Source file " ^ quote name ^ " does not exist.")

    52 

    53 val _ = ThyOutput.add_commands

    54   [("ML_open", ThyOutput.args (Scan.lift (Args.name --

    55       (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --

    56        Scan.optional (Args.parens (OuterParse.list1 Args.name)) []))) (output_ml_open ml_val_open)),

    57    ("ML_file", ThyOutput.args (Scan.lift Args.name)

    58       (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))),

    59    ("ML_text", ThyOutput.args (Scan.lift Args.name)

    60       (ThyOutput.output (fn _ => fn s => Pretty.str s))),

    61    ("ML", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val)),

    62    ("ML_decl", ThyOutput.args (Scan.lift Args.name) (output_ml ml_decl)),

    63    ("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)),

    64    ("ML_response_fake", 

    65            ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)),

    66    ("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)),

    67    ("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))];

    68    

    69 end;