|
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; |