132 ML_Context.eval |
132 ML_Context.eval |
133 {SML = SML, exchange = false, redirect = false, verbose = verbose, |
133 {SML = SML, exchange = false, redirect = false, verbose = verbose, |
134 writeln = writeln_message, warning = warning_message} |
134 writeln = writeln_message, warning = warning_message} |
135 Position.none; |
135 Position.none; |
136 |
136 |
137 in |
137 fun eval_context thread_name index SML toks = |
138 |
138 let |
139 fun eval thread_name index SML txt1 txt2 = |
139 val context1 = |
140 let |
140 ML_Context.the_generic_context () |
141 val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); |
|
142 |
|
143 val evaluate_verbose = evaluate {SML = SML, verbose = true}; |
|
144 val context1 = ML_Context.the_generic_context () |
|
145 |> Context_Position.set_visible_generic false |
141 |> Context_Position.set_visible_generic false |
146 |> Config.put_generic ML_Options.debugger false |
142 |> Config.put_generic ML_Options.debugger false |
147 |> ML_Env.add_name_space {SML = SML} |
143 |> ML_Env.add_name_space {SML = SML} |
148 (ML_Debugger.debug_name_space (the_debug_state thread_name index)); |
144 (ML_Debugger.debug_name_space (the_debug_state thread_name index)); |
149 val context2 = |
145 val context2 = |
150 if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1 |
146 if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks |
151 then context1 |
147 then context1 |
152 else |
148 else |
153 let |
149 let |
154 val context' = context1 |
150 val context' = context1 |
155 |> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1)); |
151 |> ML_Context.exec (fn () => |
|
152 evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks)); |
156 fun try_exec toks = |
153 fun try_exec toks = |
157 try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context'; |
154 try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context'; |
158 in |
155 in |
159 (case get_first try_exec context_attempts of |
156 (case get_first try_exec context_attempts of |
160 SOME context2 => context2 |
157 SOME context2 => context2 |
161 | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic") |
158 | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic") |
162 end; |
159 end; |
163 in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end; |
160 in context2 end; |
|
161 |
|
162 in |
|
163 |
|
164 fun eval thread_name index SML txt1 txt2 = |
|
165 let |
|
166 val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); |
|
167 val context = eval_context thread_name index SML toks1; |
|
168 in Context.setmp_thread_data (SOME context) evaluate {SML = SML, verbose = true} toks2 end; |
|
169 |
|
170 fun print_vals thread_name index SML txt = |
|
171 let |
|
172 val context = eval_context thread_name index SML (ML_Lex.read_source SML (Input.string txt)); |
|
173 val space = ML_Debugger.debug_name_space (the_debug_state thread_name index); |
|
174 |
|
175 fun print x = |
|
176 Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space)); |
|
177 fun print_all () = |
|
178 #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) () |
|
179 |> sort_wrt #1 |> map (Pretty.item o single o print o #2) |
|
180 |> Pretty.chunks |> Pretty.string_of |> writeln_message; |
|
181 in Context.setmp_thread_data (SOME context) print_all () end; |
164 |
182 |
165 end; |
183 end; |
166 |
184 |
167 |
185 |
168 |
186 |
187 | ["step_over"] => (step_over_stepping (); false) |
205 | ["step_over"] => (step_over_stepping (); false) |
188 | ["step_out"] => (step_out_stepping (); false) |
206 | ["step_out"] => (step_out_stepping (); false) |
189 | ["eval", index, SML, txt1, txt2] => |
207 | ["eval", index, SML, txt1, txt2] => |
190 (error_wrapper (fn () => |
208 (error_wrapper (fn () => |
191 eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true) |
209 eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true) |
|
210 | ["print_vals", index, SML, txt] => |
|
211 (error_wrapper (fn () => |
|
212 print_vals thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt); true) |
192 | bad => |
213 | bad => |
193 (Output.system_message |
214 (Output.system_message |
194 ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true)); |
215 ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true)); |
195 |
216 |
196 in |
217 in |