96 |
96 |
97 |
97 |
98 |
98 |
99 (* eval ML *) |
99 (* eval ML *) |
100 |
100 |
|
101 local |
|
102 |
|
103 val context_attempts = |
|
104 map ML_Lex.read |
|
105 ["Context.set_thread_data (SOME (Context.Theory ML_context))", |
|
106 "Context.set_thread_data (SOME (Context.Proof ML_context))", |
|
107 "Context.set_thread_data (SOME ML_context)"]; |
|
108 |
|
109 fun evaluate {SML, verbose} = |
|
110 ML_Context.eval |
|
111 {SML = SML, exchange = false, redirect = false, verbose = verbose, |
|
112 writeln = writeln_message, warning = warning_message} |
|
113 Position.none; |
|
114 |
|
115 in |
|
116 |
101 fun eval thread_name index SML txt1 txt2 = |
117 fun eval thread_name index SML txt1 txt2 = |
102 let |
118 let |
103 fun evaluate verbose = |
119 val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); |
104 ML_Context.eval |
120 |
105 {SML = SML, exchange = false, redirect = false, verbose = verbose, |
121 val evaluate_verbose = evaluate {SML = SML, verbose = true}; |
106 writeln = writeln_message, warning = warning_message} |
|
107 Position.none; |
|
108 |
|
109 val debug_state = the_debug_state thread_name index; |
|
110 val context1 = ML_Context.the_generic_context () |
122 val context1 = ML_Context.the_generic_context () |
111 |> Context_Position.set_visible_generic false |
123 |> Context_Position.set_visible_generic false |
112 |> ML_Env.add_name_space {SML = SML} (ML_Debugger.debug_name_space debug_state); |
124 |> ML_Env.add_name_space {SML = SML} |
113 val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2); |
125 (ML_Debugger.debug_name_space (the_debug_state thread_name index)); |
114 in |
126 val context2 = |
115 if null (filter_out (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1) |
127 if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1 |
116 then Context.setmp_thread_data (SOME context1) (fn () => evaluate true toks2) () |
128 then context1 |
117 else error "FIXME" |
129 else |
118 end; |
130 let |
|
131 val context' = context1 |
|
132 |> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1)); |
|
133 fun try_exec toks = |
|
134 try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context'; |
|
135 in |
|
136 (case get_first try_exec context_attempts of |
|
137 SOME context2 => context2 |
|
138 | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic") |
|
139 end; |
|
140 in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end; |
|
141 |
|
142 end; |
119 |
143 |
120 |
144 |
121 (* debugger entry point *) |
145 (* debugger entry point *) |
122 |
146 |
123 local |
147 local |