9 fun translate_string f str = |
9 fun translate_string f str = |
10 implode (map f (Symbol.explode str)) |
10 implode (map f (Symbol.explode str)) |
11 |
11 |
12 fun prefix_lines prfx txt = |
12 fun prefix_lines prfx txt = |
13 map (fn s => prfx ^ s) (split_lines txt) |
13 map (fn s => prfx ^ s) (split_lines txt) |
|
14 |
|
15 fun is_sep "\<dots>" = true |
|
16 | is_sep s = Symbol.is_ascii_blank s; |
|
17 |
|
18 fun scan_word sep = |
|
19 Scan.many1 sep >> K NONE || |
|
20 Scan.many1 (fn s => not (sep s) andalso Symbol.not_eof s) >> (SOME o implode); |
|
21 |
|
22 fun split_words sep = Symbol.scanner "Bad text" (Scan.repeat (scan_word sep) >> map_filter I); |
|
23 |
|
24 fun explode_words sep = split_words sep o Symbol.explode; |
|
25 |
|
26 fun match_string sep pat str = |
|
27 let |
|
28 fun match [] _ = true |
|
29 | match (p :: ps) s = |
|
30 size p <= size s andalso |
|
31 (case try (unprefix p) s of |
|
32 SOME s' => match ps s' |
|
33 | NONE => match (p :: ps) (String.substring (s, 1, size s - 1))); |
|
34 in match (explode_words sep pat) str end; |
14 |
35 |
15 fun ml_with_vars' ys txt = |
36 fun ml_with_vars' ys txt = |
16 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"] |
37 implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"] |
17 |
38 |
18 fun ml_with_vars ys src = |
39 fun ml_with_vars ys src = |
68 |
89 |
69 val parser_ml = Scan.lift (Args.text_input -- |
90 val parser_ml = Scan.lift (Args.text_input -- |
70 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
91 (Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] -- |
71 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
92 Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name))) |
72 |
93 |
73 fun output_ml_response ctxt src = |
94 fun output_ml_response ignore_pat ctxt (src, opat) = |
74 let |
95 let |
75 val res = eval_response ctxt src |
96 val res = eval_response ctxt src |
|
97 val _ = writeln res |
|
98 val cnt = YXML.content_of res |
|
99 val pat = case opat of NONE => cnt |
|
100 | SOME p => p |> Input.source_content |
|
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]) |
|
103 val out = if ignore_pat then cnt else pat |
76 in |
104 in |
77 OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " res]) |
105 OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " out]) |
78 end |
106 end |
79 |
|
80 |
107 |
81 (* 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 *) |
82 fun output_ml_ind ctxt (src, stru) = |
109 fun output_ml_ind ctxt (src, stru) = |
83 let |
110 let |
84 val txt = Input.source_content src |
111 val txt = Input.source_content src |
147 (output ctxt ((split_lines (Input.source_content lhs)) @ |
174 (output ctxt ((split_lines (Input.source_content lhs)) @ |
148 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
175 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
149 |
176 |
150 val single_arg = Scan.lift (Args.text_input) |
177 val single_arg = Scan.lift (Args.text_input) |
151 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) |
152 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)) |
153 |
181 |
154 val ml_setup = |
182 val ml_setup = |
155 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
183 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
156 #> Thy_Output.antiquotation_raw @{binding "ML_response"} single_arg output_ml_response |
184 #> Thy_Output.antiquotation_raw @{binding "ML_response"} maybe_two_args (output_ml_response false) |
|
185 #> Thy_Output.antiquotation_raw @{binding "ML_response_ignore"} maybe_two_args (output_ml_response true) |
157 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
186 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
158 #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind |
187 #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind |
159 #> Thy_Output.antiquotation_raw @{binding "ML_structure_ind"} single_arg output_struct_ind |
188 #> Thy_Output.antiquotation_raw @{binding "ML_structure_ind"} single_arg output_struct_ind |
160 #> Thy_Output.antiquotation_raw @{binding "ML_functor_ind"} single_arg output_funct_ind |
189 #> Thy_Output.antiquotation_raw @{binding "ML_functor_ind"} single_arg output_funct_ind |
161 #> Thy_Output.antiquotation_raw @{binding "ML_matchresult"} two_args output_response |
190 #> Thy_Output.antiquotation_raw @{binding "ML_matchresult"} two_args output_response |