130 ["Context.put_generic_context (SOME (Context.Theory ML_context))", |
130 ["Context.put_generic_context (SOME (Context.Theory ML_context))", |
131 "Context.put_generic_context (SOME (Context.Proof ML_context))", |
131 "Context.put_generic_context (SOME (Context.Proof ML_context))", |
132 "Context.put_generic_context (SOME ML_context)"]; |
132 "Context.put_generic_context (SOME ML_context)"]; |
133 |
133 |
134 fun evaluate {SML, verbose} = |
134 fun evaluate {SML, verbose} = |
135 ML_Context.eval |
135 let val env = ML_Env.make_standard SML in |
136 {SML = SML, exchange = false, redirect = false, verbose = verbose, |
136 ML_Context.eval |
137 debug = SOME false, writeln = writeln_message, warning = warning_message} |
137 {read = SOME env, write = SOME env, redirect = false, verbose = verbose, |
138 Position.none; |
138 debug = SOME false, writeln = writeln_message, warning = warning_message} |
|
139 Position.none |
|
140 end; |
139 |
141 |
140 fun eval_setup thread_name index SML context = |
142 fun eval_setup thread_name index SML context = |
141 context |
143 context |
142 |> Context_Position.set_visible_generic false |
144 |> Context_Position.set_visible_generic false |
143 |> ML_Env.add_name_space {SML = SML} |
145 |> ML_Env.add_name_space (ML_Env.make_standard SML) |
144 (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index)); |
146 (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index)); |
145 |
147 |
146 fun eval_context thread_name index SML toks = |
148 fun eval_context thread_name index SML toks = |
147 let |
149 let |
148 val context = Context.the_generic_context (); |
150 val context = Context.the_generic_context (); |