1 (* |
1 (* Auxiliary antiquotations for the Cookbook. *) |
2 Auxiliary antiquotations for the Cookbook. |
|
3 |
|
4 *) |
|
5 |
2 |
6 structure AntiquoteSetup: sig end = |
3 structure AntiquoteSetup: sig end = |
7 struct |
4 struct |
8 |
5 |
9 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
6 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
10 |
7 |
11 fun ml_val ys txt = "fn " ^ |
8 fun ml_val_open (ys, xs) txt = |
12 (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ |
9 let fun ml_val_open_aux ys txt = |
13 " => (" ^ 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; |
14 |
16 |
15 fun ml_val_open (ys, []) txt = ml_val ys txt |
17 fun ml_val txt = ml_val_open ([],[]) txt; |
16 | ml_val_open (ys, xs) txt = |
|
17 ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); |
|
18 |
18 |
19 fun ml_pat (rhs, pat) = |
19 fun ml_pat (rhs, pat) = |
20 let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) |
20 let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
21 (Symbol.explode pat)) |
|
22 in |
21 in |
23 "val " ^ pat' ^ " = " ^ rhs |
22 "val " ^ pat' ^ " = " ^ rhs |
24 end; |
23 end; |
25 |
24 |
26 (* modified from original *) |
25 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
27 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
26 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
28 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"; |
27 fun ml_decl txt = txt |
29 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
|
30 |
28 |
31 fun output_verbatim f src ctxt x = |
29 fun output_ml_open ml src ctxt (txt,ovars) = |
32 let val txt = f ctxt x |
30 (ML_Context.eval_in (SOME ctxt) false Position.none (ml ovars txt); |
33 in |
31 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt (space_explode "\n" txt)) |
34 (if ! ThyOutput.source then str_of_source src else txt) |
|
35 |> (if ! ThyOutput.quotes then quote else I) |
|
36 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt |
|
37 end; |
|
38 |
|
39 fun output_ml_old ml = output_verbatim |
|
40 (fn ctxt => fn ((txt, p), pos) => |
|
41 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
|
42 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
|
43 Chunks.transform_cmts |> implode)); |
|
44 |
32 |
45 fun output_ml ml src ctxt txt = |
33 fun output_ml ml src ctxt txt = |
46 (ML_Context.eval_in (SOME ctxt) false Position.none (ml txt); |
34 output_ml_open (K ml) src ctxt (txt,()) |
47 ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt) |
|
48 |
35 |
49 fun add_response_indicator txt = |
36 fun add_response_indicator txt = |
50 space_implode "\n" (map (fn s => "> " ^ s) (space_explode "\n" txt)) |
37 map (fn s => "> " ^ s) (space_explode "\n" txt) |
51 |
38 |
52 fun output_ml_response ml src ctxt (lhs,pat) = |
39 fun output_ml_response ml src ctxt (lhs,pat) = |
53 (ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat)); |
40 (ML_Context.eval_in (SOME ctxt) false Position.none (ml (lhs,pat)); |
54 let val txt = lhs ^ "\n" ^ (add_response_indicator pat) |
41 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
55 in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end) |
42 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
56 |
43 |
57 fun output_ml_response_fake ml src ctxt (lhs,pat) = |
44 fun output_ml_response_fake ml src ctxt (lhs,pat) = |
58 (ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs); |
45 (ML_Context.eval_in (SOME ctxt) false Position.none (ml lhs); |
59 let val txt = lhs ^ "\n" ^ (add_response_indicator pat) |
46 let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat) |
60 in ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt txt end) |
47 in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
61 |
48 |
62 fun check_file_exists ctxt name = |
49 fun check_file_exists ctxt name = |
63 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () |
50 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () |
64 else error ("Source file " ^ quote name ^ " does not exist.") |
51 else error ("Source file " ^ quote name ^ " does not exist.") |
65 |
52 |
66 |
|
67 |
|
68 val _ = ThyOutput.add_commands |
53 val _ = ThyOutput.add_commands |
69 [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
54 [("ML_open", ThyOutput.args (Scan.lift (Args.name -- |
70 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
55 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
71 Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml_old ml_val_open)), |
56 Scan.optional (Args.parens (OuterParse.list1 Args.name)) []))) (output_ml_open ml_val_open)), |
72 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
57 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
73 (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
58 (ThyOutput.output (fn _ => fn s => (check_file_exists s; Pretty.str s)))), |
74 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
59 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
75 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
60 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
76 ("ML", ThyOutput.args (Scan.lift Args.name) (output_ml ml_val)), |
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)), |
77 ("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)), |
63 ("ML_response", ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response ml_pat)), |
78 ("ML_response_fake", |
64 ("ML_response_fake", |
79 ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)), |
65 ThyOutput.args (Scan.lift (Args.name -- Args.name)) (output_ml_response_fake ml_val)), |
80 ("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)), |
66 ("ML_struct", ThyOutput.args (Scan.lift Args.name) (output_ml ml_struct)), |
81 ("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))]; |
67 ("ML_type", ThyOutput.args (Scan.lift Args.name) (output_ml ml_type))]; |