src/Pure/ML/ml_compiler.ML
changeset 62889 99c7f31615c2
parent 62878 1cec457e0a03
child 62902 3c0f53eae166
--- a/src/Pure/ML/ml_compiler.ML	Wed Apr 06 14:08:57 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Apr 06 16:33:33 2016 +0200
@@ -52,7 +52,7 @@
 fun report_parse_tree redirect depth space parse_tree =
   let
     val is_visible =
-      (case Context.thread_data () of
+      (case Context.get_generic_context () of
         SOME context => Context_Position.is_visible_generic context
       | NONE => true);
     fun is_reported pos = is_visible andalso Position.is_reported pos;
@@ -135,7 +135,7 @@
     val all_breakpoints = rev (breakpoints_tree parse_tree []);
     val _ = Position.reports (map #1 all_breakpoints);
     val _ =
-      if is_some (Context.thread_data ()) then
+      if is_some (Context.get_generic_context ()) then
         Context.>> (fold (ML_Env.add_breakpoint o #2) all_breakpoints)
       else ();
   in () end;
@@ -146,7 +146,7 @@
 fun eval (flags: flags) pos toks =
   let
     val space = ML_Env.make_name_space {SML = #SML_env flags, exchange = #exchange flags};
-    val opt_context = Context.thread_data ();
+    val opt_context = Context.get_generic_context ();
 
 
     (* input *)