# HG changeset patch # User wenzelm # Date 1459965027 -7200 # Node ID 047129a6e200b89df1dffbb90187c02bd3c7eecd # Parent fca40adc63428e06745bd9129f0d615cce8286bd more robust bootstrap; diff -r fca40adc6342 -r 047129a6e200 src/Pure/General/output.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 ())); diff -r fca40adc6342 -r 047129a6e200 src/Pure/ML/ml_compiler0.ML --- 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";