13 | _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end")) |
14 | _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end")) |
14 end; |
15 end; |
15 |
16 |
16 fun ml_val txt = ml_val_open ([],[]) txt; |
17 fun ml_val txt = ml_val_open ([],[]) txt; |
17 |
18 |
18 fun ml_pat (rhs, pat) = |
19 fun ml_pat (lhs, pat) = |
19 let |
20 let |
20 val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
21 val pat' = implode (map (fn "\\<dots>" => "_" | s => s) (Symbol.explode pat)) |
21 in "val " ^ pat' ^ " = " ^ rhs end; |
22 in "val " ^ pat' ^ " = " ^ lhs end; |
22 |
23 |
23 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
24 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end"; |
24 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
25 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option"; |
25 |
26 |
26 val transform_cmts_str = |
27 (* eval function *) |
27 Source.of_string #> ML_Lex.source #> Source.exhaust #> |
28 fun eval_fn ctxt pos exp = |
28 Chunks.transform_cmts #> implode; |
29 ML_Context.eval_in (SOME ctxt) false pos exp |
29 |
30 |
30 fun output_ml ml src ctxt ((txt,ovars),pos) = |
31 (* string functions *) |
31 (ML_Context.eval_in (SOME ctxt) false pos (ml ovars txt); |
|
32 txt |> transform_cmts_str |> space_explode "\n" |> |
|
33 Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt) |
|
34 |
|
35 fun output_ml_aux ml src ctxt (txt,pos) = |
|
36 output_ml (K ml) src ctxt ((txt,()),pos) |
|
37 |
|
38 fun string_explode str txt = |
32 fun string_explode str txt = |
39 map (fn s => str ^ s) (space_explode "\n" txt) |
33 map (fn s => str ^ s) (space_explode "\n" txt) |
40 |
34 |
41 fun output_ml_response ml src ctxt ((lhs,pat),pos) = |
35 val transform_cmts_str = |
42 (ML_Context.eval_in (SOME ctxt) false pos (ml (lhs,pat)); |
36 Source.of_string |
43 let |
37 #> ML_Lex.source |
44 val txt = (string_explode "" lhs) @ (string_explode "> " pat) |
38 #> Source.exhaust |
45 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
39 #> Chunks.transform_cmts |
|
40 #> implode |
|
41 #> string_explode ""; |
46 |
42 |
47 fun output_ml_response_fake ml src ctxt ((lhs,pat),pos) = |
43 (* parser for single and two arguments *) |
48 (ML_Context.eval_in (SOME ctxt) false pos (ml lhs); |
44 val single_arg = Scan.lift (OuterParse.position Args.name) |
49 let val txt = (string_explode "" lhs) @ (string_explode "> " pat) |
45 val two_args = Scan.lift (OuterParse.position (Args.name -- Args.name)) |
50 in Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end) |
|
51 |
46 |
|
47 (* output function *) |
|
48 val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s) |
|
49 |
|
50 (* checks and prints open expressions *) |
|
51 fun output_ml src node = |
|
52 let |
|
53 fun output src ctxt ((txt,ovars),pos) = |
|
54 (eval_fn ctxt pos (ml_val_open ovars txt); |
|
55 output_fn src ctxt (transform_cmts_str txt)) |
|
56 |
|
57 val parser = Scan.lift (OuterParse.position (Args.name -- |
|
58 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
|
59 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))) |
|
60 in |
|
61 ThyOutput.args parser output src node |
|
62 end |
|
63 |
|
64 (* checks and prints types and structures *) |
|
65 fun output_exp ml src node = |
|
66 let |
|
67 fun output src ctxt (txt,pos) = |
|
68 (eval_fn ctxt pos (ml txt); |
|
69 output_fn src ctxt (string_explode "" txt)) |
|
70 in |
|
71 ThyOutput.args single_arg output src node |
|
72 end |
|
73 |
|
74 (* checks and expression agains a result pattern *) |
|
75 fun output_ml_response src node = |
|
76 let |
|
77 fun output src ctxt ((lhs,pat),pos) = |
|
78 (eval_fn ctxt pos (ml_pat (lhs,pat)); |
|
79 output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) |
|
80 in |
|
81 ThyOutput.args two_args output src node |
|
82 end |
|
83 |
|
84 (* checks the expressions, but does not check it against a result pattern *) |
|
85 fun output_ml_response_fake src node = |
|
86 let |
|
87 fun output src ctxt ((lhs,pat),pos) = |
|
88 (eval_fn ctxt pos (ml_val lhs); |
|
89 output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))) |
|
90 in |
|
91 ThyOutput.args two_args output src node |
|
92 end |
|
93 |
|
94 (* just prints an expression and a result pattern *) |
52 fun output_ml_response_fake_both src node = |
95 fun output_ml_response_fake_both src node = |
53 let |
96 let |
54 fun ouput src ctxt (lhs,pat) = |
97 fun ouput src ctxt ((lhs,pat), _) = |
55 Chunks.output_list (fn _ => fn s => Pretty.str s) src ctxt |
98 output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)) |
56 ((string_explode "" lhs) @ (string_explode "> " pat)) |
|
57 in |
99 in |
58 ThyOutput.args (Scan.lift (Args.name -- Args.name)) ouput src node |
100 ThyOutput.args two_args ouput src node |
59 end |
101 end |
60 |
102 |
|
103 (* checks whether a file exists in the Isabelle distribution *) |
61 fun check_file_exists src node = |
104 fun check_file_exists src node = |
62 let |
105 let |
63 fun check txt = |
106 fun check txt = |
64 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
107 if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then () |
65 else error ("Source file " ^ (quote txt) ^ " does not exist.") |
108 else error ("Source file " ^ (quote txt) ^ " does not exist.") |
92 in |
135 in |
93 ThyOutput.args (Scan.succeed ()) |
136 ThyOutput.args (Scan.succeed ()) |
94 (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node |
137 (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node |
95 end |
138 end |
96 |
139 |
97 |
|
98 val _ = ThyOutput.add_commands |
140 val _ = ThyOutput.add_commands |
99 [("ML", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- |
141 [("ML", output_ml), |
100 (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] -- |
|
101 Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))) |
|
102 (output_ml ml_val_open)), |
|
103 ("ML_file", check_file_exists), |
142 ("ML_file", check_file_exists), |
104 ("ML_response", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
143 ("ML_response", output_ml_response), |
105 (output_ml_response ml_pat)), |
144 ("ML_response_fake", output_ml_response_fake), |
106 ("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
|
107 (output_ml_response_fake ml_val)), |
|
108 ("ML_response_fake_both", output_ml_response_fake_both), |
145 ("ML_response_fake_both", output_ml_response_fake_both), |
109 ("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)), |
146 ("ML_struct", output_exp ml_struct), |
110 ("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type)), |
147 ("ML_type", output_exp ml_type), |
111 ("subgoals", output_goals)]; |
148 ("subgoals", output_goals)]; |
112 |
149 |
113 end; |
150 end; |