38 |
38 |
39 fun ml_with_vars ys src = |
39 fun ml_with_vars ys src = |
40 ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @ |
40 ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @ |
41 ML_Lex.read " => (" @ src @ ML_Lex.read ")" |
41 ML_Lex.read " => (" @ src @ ML_Lex.read ")" |
42 |
42 |
43 fun ml_with_struct (NONE) src = ML_Lex.read_source false src |
43 fun ml_with_struct (NONE) src = ML_Lex.read_source src |
44 | ml_with_struct (SOME st) src = |
44 | ml_with_struct (SOME st) src = |
45 ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end" |
45 ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source src @ ML_Lex.read " end" |
46 |
46 |
47 fun ml_val vs stru txt = |
47 fun ml_val vs stru txt = |
48 txt |> ml_with_struct stru |
48 txt |> ml_with_struct stru |
49 |> ml_with_vars vs |
49 |> ml_with_vars vs |
50 |
50 |
51 fun ml_pat pat lhs = |
51 fun ml_pat pat lhs = |
52 ML_Lex.read "val " @ ML_Lex.read_source false pat @ |
52 ML_Lex.read "val " @ ML_Lex.read_source pat @ |
53 ML_Lex.read " = " @ |
53 ML_Lex.read " = " @ |
54 ML_Lex.read_source false lhs |
54 ML_Lex.read_source lhs |
55 |
55 |
56 |
56 |
57 fun ml_struct src = |
57 fun ml_struct src = |
58 ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @ |
58 ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @ |
59 ML_Lex.read_source false src @ |
59 ML_Lex.read_source src @ |
60 ML_Lex.read " end" |
60 ML_Lex.read " end" |
61 |
61 |
62 fun ml_type src = |
62 fun ml_type src = |
63 ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option" |
63 ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source src @ ML_Lex.read ") option" |
64 |
64 |
65 (* eval function *) |
65 (* eval function *) |
66 fun eval_fn ctxt prep exp = |
66 fun eval_fn ctxt prep exp = |
67 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp) |
67 ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) (prep exp) |
68 |
68 |
69 (* Evalate expression and convert result to a string *) |
69 (* Evalate expression and convert result to a string *) |
70 fun eval_response ctxt exp = |
70 fun eval_response ctxt exp = |
71 let |
71 let |
72 fun compute exp = |
72 fun compute exp = |
73 let |
73 let |
74 val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source false exp @ |
74 val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source exp @ |
75 ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )" |
75 ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )" |
76 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input |
76 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input |
77 in "" |
77 in "" |
78 end |
78 end |
79 in |
79 in |
83 |
83 |
84 (* checks and prints a possibly open expressions, no index *) |
84 (* checks and prints a possibly open expressions, no index *) |
85 |
85 |
86 fun output_ml ctxt (src, (vs, stru)) = |
86 fun output_ml ctxt (src, (vs, stru)) = |
87 (eval_fn ctxt (ml_val vs stru) src; |
87 (eval_fn ctxt (ml_val vs stru) src; |
88 output ctxt (split_lines (Input.source_content src))) |
88 output ctxt (split_lines (fst (Input.source_content src)))) |
89 |
89 |
90 val parser_ml = Scan.lift (Args.text_input -- |
90 val parser_ml = Scan.lift (Args.text_input -- |
91 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
91 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
92 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
92 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
93 |
93 |
95 let |
95 let |
96 val res = eval_response ctxt src |
96 val res = eval_response ctxt src |
97 val _ = writeln res |
97 val _ = writeln res |
98 val cnt = YXML.content_of res |
98 val cnt = YXML.content_of res |
99 val pat = case opat of NONE => cnt |
99 val pat = case opat of NONE => cnt |
100 | SOME p => p |> Input.source_content |
100 | SOME p => p |> fst o Input.source_content |
101 val _ = if ignore_pat orelse Print_Mode.print_mode_active Latex.latexN orelse match_string is_sep pat cnt then () |
101 val _ = if ignore_pat orelse Print_Mode.print_mode_active Latex.latexN orelse match_string is_sep pat cnt then () |
102 else error (cat_lines ["Substring:", pat, "not contained in:", cnt]) |
102 else error (cat_lines ["Substring:", pat, "not contained in:", cnt]) |
103 val out = if ignore_pat then cnt else pat |
103 val out = if ignore_pat then cnt else pat |
104 in |
104 in |
105 OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " out]) |
105 OutputTutorial.output ctxt ([fst (Input.source_content src)] @ [Library.prefix_lines "> " out]) |
106 end |
106 end |
107 |
107 |
108 (* checks and prints a single ML-item and produces an index entry *) |
108 (* checks and prints a single ML-item and produces an index entry *) |
109 fun output_ml_ind ctxt (src, stru) = |
109 fun output_ml_ind ctxt (src, stru) = |
110 let |
110 let |
111 val txt = Input.source_content src |
111 val (txt,_) = Input.source_content src |
112 in |
112 in |
113 (eval_fn ctxt (ml_val [] stru) src; |
113 (eval_fn ctxt (ml_val [] stru) src; |
114 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
114 case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of |
115 (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
115 (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt) |
116 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
116 | (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt) |
121 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
121 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)) |
122 |
122 |
123 (* checks and prints structures *) |
123 (* checks and prints structures *) |
124 fun gen_output_struct outfn ctxt src = |
124 fun gen_output_struct outfn ctxt src = |
125 let |
125 let |
126 val txt = Input.source_content src |
126 val (txt, _) = Input.source_content src |
127 in |
127 in |
128 (eval_fn ctxt ml_struct src; |
128 (eval_fn ctxt ml_struct src; |
129 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
129 outfn {main = Code txt, minor = Plain "structure"} (split_lines txt)) |
130 end |
130 end |
131 |
131 |
133 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt |
133 fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt |
134 |
134 |
135 (* prints functors; no checks *) |
135 (* prints functors; no checks *) |
136 fun gen_output_funct outfn src = |
136 fun gen_output_funct outfn src = |
137 let |
137 let |
138 val txt = Input.source_content src |
138 val (txt, _) = Input.source_content src |
139 in |
139 in |
140 (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) |
140 (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt)) |
141 end |
141 end |
142 |
142 |
143 fun output_funct ctxt = gen_output_funct (K (output ctxt)) |
143 fun output_funct ctxt = gen_output_funct (K (output ctxt)) |
144 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) |
144 fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt) |
145 |
145 |
146 (* checks and prints types *) |
146 (* checks and prints types *) |
147 fun gen_output_type outfn ctxt src = |
147 fun gen_output_type outfn ctxt src = |
148 let |
148 let |
149 val txt = Input.source_content src |
149 val (txt, _) = Input.source_content src |
150 in |
150 in |
151 (eval_fn ctxt ml_type src; |
151 (eval_fn ctxt ml_type src; |
152 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
152 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
153 end |
153 end |
154 |
154 |
158 val dots_pat = translate_string (fn "_" => "\<dots>" | s => s) |
158 val dots_pat = translate_string (fn "_" => "\<dots>" | s => s) |
159 |
159 |
160 (* checks and expression against a result pattern *) |
160 (* checks and expression against a result pattern *) |
161 fun output_response ctxt (lhs, pat) = |
161 fun output_response ctxt (lhs, pat) = |
162 (eval_fn ctxt (ml_pat pat) lhs; |
162 (eval_fn ctxt (ml_pat pat) lhs; |
163 output ctxt ((prefix_lines "" (Input.source_content lhs)) @ |
163 output ctxt ((prefix_lines "" (fst (Input.source_content lhs))) @ |
164 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
164 (prefix_lines "> " (dots_pat (fst (Input.source_content pat)))))) |
165 |
165 |
166 (* checks the expressions, but does not check it against a result pattern *) |
166 (* checks the expressions, but does not check it against a result pattern *) |
167 fun output_response_fake ctxt (lhs, pat) = |
167 fun output_response_fake ctxt (lhs, pat) = |
168 (eval_fn ctxt (ml_val [] NONE) lhs; |
168 (eval_fn ctxt (ml_val [] NONE) lhs; |
169 output ctxt ( (split_lines (Input.source_content lhs)) @ |
169 output ctxt ( (split_lines (fst (Input.source_content lhs))) @ |
170 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
170 (prefix_lines "> " (dots_pat (fst (Input.source_content pat)))))) |
171 |
171 |
172 (* checks the expressions, but does not check it against a result pattern *) |
172 (* checks the expressions, but does not check it against a result pattern *) |
173 fun ouput_response_fake_both ctxt (lhs, pat) = |
173 fun ouput_response_fake_both ctxt (lhs, pat) = |
174 (output ctxt ((split_lines (Input.source_content lhs)) @ |
174 (output ctxt ((split_lines (fst (Input.source_content lhs))) @ |
175 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
175 (prefix_lines "> " (dots_pat (fst ((Input.source_content pat))))))) |
176 |
176 |
177 val single_arg = Scan.lift (Args.text_input) |
177 val single_arg = Scan.lift (Args.text_input) |
178 val two_args = Scan.lift (Args.text_input -- Args.text_input) |
178 val two_args = Scan.lift (Args.text_input -- Args.text_input) |
179 val maybe_two_args = Scan.lift (Args.text_input -- Scan.option Args.text_input) |
179 val maybe_two_args = Scan.lift (Args.text_input -- Scan.option Args.text_input) |
180 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
180 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
200 implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"] |
200 implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"] |
201 end |
201 end |
202 |
202 |
203 fun check_file_exists _ src = |
203 fun check_file_exists _ src = |
204 let |
204 let |
205 val txt = Input.source_content src |
205 val (txt, _) = Input.source_content src |
206 in |
206 in |
207 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
207 (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) |
208 then Latex.string (href_link txt) |
208 then Latex.string (href_link txt) |
209 else error (implode ["Source file ", quote txt, " does not exist."])) |
209 else error (implode ["Source file ", quote txt, " does not exist."])) |
210 end |
210 end |