1 (* |
1 (* |
2 Auxiliary antiquotations for the Cookbook. |
2 Auxiliary antiquotations for the Cookbook. |
3 |
3 |
4 *) |
4 *) |
5 |
5 |
6 local structure O = ThyOutput |
6 structure AntiquoteSetup: sig end = |
7 in |
7 struct |
8 fun check_exists f = |
|
9 if File.exists (Path.explode ("~~/src/" ^ f)) then () |
|
10 else error ("Source file " ^ quote f ^ " does not exist.") |
|
11 |
|
12 val _ = O.add_commands |
|
13 [("ML_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name => |
|
14 (check_exists name; Pretty.str name))))]; |
|
15 |
8 |
16 end |
9 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
|
10 |
|
11 fun ml_val ys txt = "fn " ^ |
|
12 (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ |
|
13 " => (" ^ txt ^ ");"; |
|
14 |
|
15 fun ml_val_open (ys, []) txt = ml_val ys txt |
|
16 | ml_val_open (ys, xs) txt = |
|
17 ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); |
|
18 |
|
19 fun output_verbatim f src ctxt x = |
|
20 let val txt = f ctxt x |
|
21 in |
|
22 (if ! ThyOutput.source then str_of_source src else txt) |
|
23 |> (if ! ThyOutput.quotes then quote else I) |
|
24 |> (if ! ThyOutput.display then enclose "\\begin{alltt}\n" "\n\\end{alltt}" |
|
25 else |
|
26 split_lines |
|
27 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
|
28 #> space_implode "\\isasep\\\\%\n") |
|
29 end; |
|
30 |
|
31 fun output_ml ml = output_verbatim |
|
32 (fn ctxt => fn ((txt, p), pos) => |
|
33 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
|
34 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
|
35 Chunks.transform_cmts |> implode)); |
|
36 |
|
37 fun transform_char "\\" = "{\\isacharbackslash}" |
|
38 | transform_char "$" = "{\\$}" |
|
39 | transform_char "{" = "{\\isacharbraceleft}" |
|
40 | transform_char "}" = "{\\isacharbraceright}" |
|
41 | transform_char x = x; |
|
42 |
|
43 fun transform_symbol x = |
|
44 if Symbol.is_char x then transform_char x else Latex.output_symbols [x]; |
|
45 |
|
46 fun transform_str s = implode (map transform_symbol (Symbol.explode s)); |
|
47 |
|
48 fun ml_pat (rhs, pat) = |
|
49 let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) |
|
50 (Symbol.explode pat)) |
|
51 in |
|
52 "val " ^ pat' ^ " = " ^ rhs |
|
53 end; |
|
54 |
|
55 fun output_ml_response ml = output_verbatim |
|
56 (fn ctxt => fn ((x as (rhs, pat), p), pos) => |
|
57 (ML_Context.eval_in (SOME ctxt) false pos (ml p x); |
|
58 transform_str rhs ^ "\n\n" ^ |
|
59 space_implode "\n" (map (enclose "\\textit{" "}") |
|
60 (space_explode "\n" (transform_str pat))))); |
|
61 |
|
62 fun check_exists ctxt name = |
|
63 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () |
|
64 else error ("Source file " ^ quote name ^ " does not exist.") |
|
65 |
|
66 val _ = ThyOutput.add_commands |
|
67 [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
|
68 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
|
69 Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml ml_val_open)), |
|
70 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position |
|
71 ((Args.name -- Args.name) >> rpair ()))) |
|
72 (output_ml_response (K ml_pat))), |
|
73 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
|
74 (ThyOutput.output (fn _ => fn name => (check_exists name; Pretty.str name))))]; |
|
75 |
|
76 end; |