129 map ML_Lex.read |
129 map ML_Lex.read |
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 make_environment sml = if sml then ML_Env.SML else ML_Env.Isabelle; |
|
135 |
134 fun evaluate {SML, verbose} = |
136 fun evaluate {SML, verbose} = |
135 ML_Context.eval |
137 ML_Context.eval |
136 {environment = ML_Env.make_standard SML, redirect = false, verbose = verbose, |
138 {environment = make_environment SML, redirect = false, verbose = verbose, |
137 debug = SOME false, writeln = writeln_message, warning = warning_message} |
139 debug = SOME false, writeln = writeln_message, warning = warning_message} |
138 Position.none; |
140 Position.none; |
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 (ML_Env.make_standard SML) |
145 |> ML_Env.add_name_space (make_environment 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 (); |