14 |
14 |
15 fun ml_val_open (ys, []) txt = ml_val ys txt |
15 fun ml_val_open (ys, []) txt = ml_val ys txt |
16 | ml_val_open (ys, xs) txt = |
16 | ml_val_open (ys, xs) txt = |
17 ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); |
17 ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); |
18 |
18 |
|
19 fun ml_pat (rhs, pat) = |
|
20 let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) |
|
21 (Symbol.explode pat)) |
|
22 in |
|
23 "val " ^ pat' ^ " = " ^ rhs |
|
24 end; |
|
25 |
|
26 (* modified from original *) |
|
27 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
|
28 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"; |
|
29 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
|
30 |
19 fun output_verbatim f src ctxt x = |
31 fun output_verbatim f src ctxt x = |
20 let val txt = f ctxt x |
32 let val txt = f ctxt x |
21 in |
33 in |
22 (if ! ThyOutput.source then str_of_source src else txt) |
34 (if ! ThyOutput.source then str_of_source src else txt) |
23 |> (if ! ThyOutput.quotes then quote else I) |
35 |> (if ! ThyOutput.quotes then quote else I) |
24 |> (if ! ThyOutput.display then enclose "\\begin{alltt}\n" "\n\\end{alltt}" |
36 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt |
25 else |
|
26 split_lines |
|
27 #> map (space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|") |
|
28 #> space_implode "\\isasep\\\\%\n") |
|
29 end; |
37 end; |
30 |
38 |
31 fun output_ml ml = output_verbatim |
39 fun output_ml ml = output_verbatim |
32 (fn ctxt => fn ((txt, p), pos) => |
40 (fn ctxt => fn ((txt, p), pos) => |
33 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
41 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
34 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
42 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
35 Chunks.transform_cmts |> implode)); |
43 Chunks.transform_cmts |> implode)); |
36 |
44 |
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 |
45 fun output_ml_response ml = output_verbatim |
56 (fn ctxt => fn ((x as (rhs, pat), p), pos) => |
46 (fn ctxt => fn ((x as (rhs, pat), p), pos) => |
57 (ML_Context.eval_in (SOME ctxt) false pos (ml p x); |
47 (ML_Context.eval_in (SOME ctxt) false pos (ml p x); |
58 transform_str rhs ^ "\n\n" ^ |
48 rhs ^ "\n" ^ |
59 space_implode "\n" (map (enclose "\\textit{" "}") |
49 space_implode "\n" (map (fn s => "> " ^ s) |
60 (space_explode "\n" (transform_str pat))))); |
50 (space_explode "\n" pat)))); |
61 |
51 |
62 fun check_exists ctxt name = |
52 fun output_ml_checked ml src ctxt (txt, pos) = |
|
53 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
|
54 (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) |
|
55 |> (if ! ThyOutput.quotes then quote else I) |
|
56 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt) |
|
57 |
|
58 fun check_file_exists ctxt name = |
63 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () |
59 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode name)) then () |
64 else error ("Source file " ^ quote name ^ " does not exist.") |
60 else error ("Source file " ^ quote name ^ " does not exist.") |
65 |
61 |
66 val _ = ThyOutput.add_commands |
62 val _ = ThyOutput.add_commands |
67 [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
63 [("ML_open", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
68 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
64 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
69 Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml ml_val_open)), |
65 Scan.optional (Args.parens (OuterParse.list1 Args.name)) [])))) (output_ml ml_val_open)), |
70 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position |
66 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position |
71 ((Args.name -- Args.name) >> rpair ()))) |
67 ((Args.name -- Args.name) >> rpair ()))) (output_ml_response (K ml_pat))), |
72 (output_ml_response (K ml_pat))), |
|
73 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
68 ("ML_file", ThyOutput.args (Scan.lift Args.name) |
74 (ThyOutput.output (fn _ => fn name => (check_exists name; Pretty.str name))))]; |
69 (ThyOutput.output (fn _ => fn name => (check_file_exists name; Pretty.str name)))), |
75 |
70 ("ML_text", ThyOutput.args (Scan.lift Args.name) |
|
71 (ThyOutput.output (fn _ => fn s => Pretty.str s))), |
|
72 ("ML", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_val)), |
|
73 ("ML_struct", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_struct)), |
|
74 ("ML_type", ThyOutput.args (Scan.lift Args.name_source_position) (output_ml_checked ml_type))]; |
|
75 |
76 end; |
76 end; |