# HG changeset patch
# User wenzelm
# Date 1457340598 -3600
# Node ID b27b7c2200b902a6291cf64b8607daf617ec15ef
# Parent  edee1966fddf525fdc4a01c7e8c29f4196abddb8
tuned signature;

diff -r edee1966fddf -r b27b7c2200b9 bin/isabelle_process
--- 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
diff -r edee1966fddf -r b27b7c2200b9 src/Pure/General/print_mode.ML
--- 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;