CookBook/antiquote_setup.ML
changeset 45 78aeca00bb54
child 49 a0edabf14457
equal deleted inserted replaced
44:dee4b3e66dfe 45:78aeca00bb54
       
     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),pos) =
       
    30   (ML_Context.eval_in (SOME ctxt) false pos (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,pos) =
       
    34   output_ml_open (K ml) src ctxt ((txt,()),pos) 
       
    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),pos) = 
       
    40   (ML_Context.eval_in (SOME ctxt) false pos (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),pos) = 
       
    45   (ML_Context.eval_in (SOME ctxt) false pos (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 txt =
       
    50   if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
       
    51   else error ("Source file " ^ quote txt ^ " does not exist.")
       
    52 
       
    53 val _ = ThyOutput.add_commands
       
    54   [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (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 (OuterParse.position Args.name)) (output_ml ml_val)),
       
    62    ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       
    63       (output_ml_response ml_pat)),
       
    64    ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) 
       
    65       (output_ml_response_fake ml_val)),
       
    66    ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_struct)),
       
    67    ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml ml_type))];
       
    68    
       
    69 end;