--- a/src/Pure/Tools/debugger.ML Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/Tools/debugger.ML Mon Aug 27 20:43:01 2018 +0200
@@ -131,18 +131,19 @@
"Context.put_generic_context (SOME (Context.Proof ML_context))",
"Context.put_generic_context (SOME ML_context)"];
-fun make_environment sml = if sml then ML_Env.SML else ML_Env.Isabelle;
+fun environment SML = if SML then ML_Env.SML else ML_Env.Isabelle;
+fun operations SML = if SML then ML_Env.SML_operations else ML_Env.Isabelle_operations;
fun evaluate {SML, verbose} =
ML_Context.eval
- {environment = make_environment SML, redirect = false, verbose = verbose,
+ {environment = environment SML, redirect = false, verbose = verbose,
debug = SOME false, writeln = writeln_message, warning = warning_message}
Position.none;
fun eval_setup thread_name index SML context =
context
|> Context_Position.set_visible_generic false
- |> ML_Env.add_name_space (make_environment SML)
+ |> ML_Env.add_name_space (environment SML)
(PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
fun eval_context thread_name index SML toks =
@@ -170,13 +171,13 @@
fun eval thread_name index SML txt1 txt2 =
let
- val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
+ val (toks1, toks2) = apply2 (#read_source (operations SML) o Input.string) (txt1, txt2);
val context = eval_context thread_name index SML toks1;
in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
fun print_vals thread_name index SML txt =
let
- val toks = ML_Lex.read_source SML (Input.string txt)
+ val toks = #read_source (operations SML) (Input.string txt)
val context = eval_context thread_name index SML toks;
val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);