--- 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";