more robust bootstrap;
authorwenzelm
Wed, 06 Apr 2016 19:50:27 +0200
changeset 62894 047129a6e200
parent 62893 fca40adc6342
child 62895 54c2abe7e9a4
more robust bootstrap;
src/Pure/General/output.ML
src/Pure/ML/ml_compiler0.ML
--- a/src/Pure/General/output.ML	Wed Apr 06 19:03:29 2016 +0200
+++ b/src/Pure/General/output.ML	Wed Apr 06 19:50:27 2016 +0200
@@ -74,7 +74,8 @@
   val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
 in
   fun add_mode name output escape =
-    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
+    if Thread_Data.is_virtual then ()
+    else Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
   fun get_mode () =
     the_default default
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
--- a/src/Pure/ML/ml_compiler0.ML	Wed Apr 06 19:03:29 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML	Wed Apr 06 19:50:27 2016 +0200
@@ -147,11 +147,13 @@
 
 (* export type-dependent functions *)
 
-ML_Compiler0.use_text
-  (ML_Compiler0.make_context
-    (ML_Name_Space.global_values
-      [("prettyRepresentation", "ML_system_pretty"),
-       ("addPrettyPrinter", "ML_system_pp"),
-       ("addOverload", "ML_system_overload")]))
-  {debug = false, file = "", line = 0, verbose = false}
-  "open PolyML RunCall" handle ERROR _ => ();
+if Thread_Data.is_virtual then ()
+else
+  ML_Compiler0.use_text
+    (ML_Compiler0.make_context
+      (ML_Name_Space.global_values
+        [("prettyRepresentation", "ML_system_pretty"),
+         ("addPrettyPrinter", "ML_system_pp"),
+         ("addOverload", "ML_system_overload")]))
+    {debug = false, file = "", line = 0, verbose = false}
+    "open PolyML RunCall";