--- a/bin/isabelle_process Mon Mar 07 08:14:18 2016 +0100
+++ b/bin/isabelle_process Mon Mar 07 09:49:58 2016 +0100
@@ -199,7 +199,7 @@
if [ -n "$MODES" ]; then
FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="--eval"
- FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Unsynchronized.change print_mode (append [$MODES])"
+ FIRST_ML_OPTIONS["${#FIRST_ML_OPTIONS[@]}"]="Print_Mode.add_modes [$MODES]"
fi
if [ -n "$SECURE" ]; then
--- a/src/Pure/General/print_mode.ML Mon Mar 07 08:14:18 2016 +0100
+++ b/src/Pure/General/print_mode.ML Mon Mar 07 09:49:58 2016 +0100
@@ -23,6 +23,7 @@
val setmp: string list -> ('a -> 'b) -> 'a -> 'b
val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
val closure: ('a -> 'b) -> 'a -> 'b
+ val add_modes: string list -> unit
end;
structure Print_Mode: PRINT_MODE =
@@ -51,6 +52,8 @@
fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
fun closure f = with_modes [] f;
+fun add_modes modes = Unsynchronized.change print_mode (append modes);
+
end;
structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;