1.1 --- a/src/Pure/General/markup.ML	Wed Jul 06 20:14:13 2011 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Wed Jul 06 20:46:06 2011 +0200
     1.3 @@ -378,12 +378,13 @@
     1.4  
     1.5  local
     1.6    val default = {output = default_output};
     1.7 -  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     1.8 +  val modes = Synchronized.var "Markup.modes" (Symtab.make [("", default)]);
     1.9  in
    1.10 -  fun add_mode name output = CRITICAL (fn () =>
    1.11 -    Unsynchronized.change modes (Symtab.update_new (name, {output = output})));
    1.12 +  fun add_mode name output =
    1.13 +    Synchronized.change modes (Symtab.update_new (name, {output = output}));
    1.14    fun get_mode () =
    1.15 -    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    1.16 +    the_default default
    1.17 +      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    1.18  end;
    1.19  
    1.20  fun output m = if is_empty m then no_output else #output (get_mode ()) m;

     2.1 --- a/src/Pure/General/output.ML	Wed Jul 06 20:14:13 2011 +0200
     2.2 +++ b/src/Pure/General/output.ML	Wed Jul 06 20:46:06 2011 +0200
     2.3 @@ -55,12 +55,13 @@
     2.4  
     2.5  local
     2.6    val default = {output = default_output, escape = default_escape};
     2.7 -  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     2.8 +  val modes = Synchronized.var "Output.modes" (Symtab.make [("", default)]);
     2.9  in
    2.10 -  fun add_mode name output escape = CRITICAL (fn () =>
    2.11 -    Unsynchronized.change modes (Symtab.update_new (name, {output = output, escape = escape})));
    2.12 +  fun add_mode name output escape =
    2.13 +    Synchronized.change modes (Symtab.update_new (name, {output = output, escape = escape}));
    2.14    fun get_mode () =
    2.15 -    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    2.16 +    the_default default
    2.17 +      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    2.18  end;
    2.19  
    2.20  fun output_width x = #output (get_mode ()) x;

     3.1 --- a/src/Pure/General/pretty.ML	Wed Jul 06 20:14:13 2011 +0200
     3.2 +++ b/src/Pure/General/pretty.ML	Wed Jul 06 20:46:06 2011 +0200
     3.3 @@ -75,12 +75,13 @@
     3.4  
     3.5  local
     3.6    val default = {indent = default_indent};
     3.7 -  val modes = Unsynchronized.ref (Symtab.make [("", default)]);
     3.8 +  val modes = Synchronized.var "Pretty.modes" (Symtab.make [("", default)]);
     3.9  in
    3.10 -  fun add_mode name indent = CRITICAL (fn () =>
    3.11 -    Unsynchronized.change modes (Symtab.update_new (name, {indent = indent})));
    3.12 +  fun add_mode name indent =
    3.13 +    Synchronized.change modes (Symtab.update_new (name, {indent = indent}));
    3.14    fun get_mode () =
    3.15 -    the_default default (Library.get_first (Symtab.lookup (! modes)) (print_mode_value ()));
    3.16 +    the_default default
    3.17 +      (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
    3.18  end;
    3.19  
    3.20  fun mode_indent x y = #indent (get_mode ()) x y;

     4.1 --- a/src/Pure/Isar/code.ML	Wed Jul 06 20:14:13 2011 +0200
     4.2 +++ b/src/Pure/Isar/code.ML	Wed Jul 06 20:46:06 2011 +0200
     4.3 @@ -247,11 +247,12 @@
     4.4  
     4.5  type kind = { empty: Object.T };
     4.6  
     4.7 -val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
     4.8 +val kinds = Synchronized.var "Code_Data" (Datatab.empty: kind Datatab.table);
     4.9  
    4.10 -fun invoke f k = case Datatab.lookup (! kinds) k
    4.11 - of SOME kind => f kind
    4.12 -  | NONE => raise Fail "Invalid code data identifier";
    4.13 +fun invoke f k =
    4.14 +  (case Datatab.lookup (Synchronized.value kinds) k of
    4.15 +    SOME kind => f kind
    4.16 +  | NONE => raise Fail "Invalid code data identifier");
    4.17  
    4.18  in
    4.19  
    4.20 @@ -259,7 +260,7 @@
    4.21    let
    4.22      val k = serial ();
    4.23      val kind = { empty = empty };
    4.24 -    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    4.25 +    val _ = Synchronized.change kinds (Datatab.update (k, kind));
    4.26    in k end;
    4.27  
    4.28  fun invoke_init k = invoke (fn kind => #empty kind) k;

     5.1 --- a/src/Pure/ROOT.ML	Wed Jul 06 20:14:13 2011 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Wed Jul 06 20:46:06 2011 +0200
     5.3 @@ -20,6 +20,13 @@
     5.4  use "General/print_mode.ML";
     5.5  use "General/alist.ML";
     5.6  use "General/table.ML";
     5.7 +
     5.8 +use "Concurrent/simple_thread.ML";
     5.9 +
    5.10 +use "Concurrent/synchronized.ML";
    5.11 +if Multithreading.available then ()
    5.12 +else use "Concurrent/synchronized_sequential.ML";
    5.13 +
    5.14  use "General/output.ML";
    5.15  use "General/timing.ML";
    5.16  use "General/properties.ML";
    5.17 @@ -63,16 +70,10 @@
    5.18  
    5.19  (* concurrency within the ML runtime *)
    5.20  
    5.21 -use "Concurrent/simple_thread.ML";
    5.22 -
    5.23  use "Concurrent/single_assignment.ML";
    5.24  if Multithreading.available then ()
    5.25  else use "Concurrent/single_assignment_sequential.ML";
    5.26  
    5.27 -use "Concurrent/synchronized.ML";
    5.28 -if Multithreading.available then ()
    5.29 -else use "Concurrent/synchronized_sequential.ML";
    5.30 -
    5.31  if String.isPrefix "smlnj" ml_system then ()
    5.32  else use "Concurrent/time_limit.ML";
    5.33  

     6.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jul 06 20:14:13 2011 +0200
     6.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Jul 06 20:46:06 2011 +0200
     6.3 @@ -20,7 +20,7 @@
     6.4    val is_active: unit -> bool
     6.5    val add_command: string -> (string list -> unit) -> unit
     6.6    val command: string -> string list -> unit
     6.7 -  val crashes: exn list Unsynchronized.ref
     6.8 +  val crashes: exn list Synchronized.var
     6.9    val init: string -> string -> unit
    6.10  end;
    6.11  
    6.12 @@ -41,18 +41,19 @@
    6.13  
    6.14  local
    6.15  
    6.16 -val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table);
    6.17 +val commands =
    6.18 +  Synchronized.var "Isabelle_Process.commands" (Symtab.empty: (string list -> unit) Symtab.table);
    6.19  
    6.20  in
    6.21  
    6.22 -fun add_command name cmd = CRITICAL (fn () =>
    6.23 -  Unsynchronized.change global_commands (fn cmds =>
    6.24 +fun add_command name cmd =
    6.25 +  Synchronized.change commands (fn cmds =>
    6.26     (if not (Symtab.defined cmds name) then ()
    6.27      else warning ("Redefining Isabelle process command " ^ quote name);
    6.28 -    Symtab.update (name, cmd) cmds)));
    6.29 +    Symtab.update (name, cmd) cmds));
    6.30  
    6.31  fun command name args =
    6.32 -  (case Symtab.lookup (! global_commands) name of
    6.33 +  (case Symtab.lookup (Synchronized.value commands) name of
    6.34      NONE => error ("Undefined Isabelle process command " ^ quote name)
    6.35    | SOME cmd => cmd args);
    6.36  
    6.37 @@ -118,12 +119,12 @@
    6.38  
    6.39  (* protocol loop -- uninterruptible *)
    6.40  
    6.41 -val crashes = Unsynchronized.ref ([]: exn list);
    6.42 +val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list);
    6.43  
    6.44  local
    6.45  
    6.46  fun recover crash =
    6.47 -  (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
    6.48 +  (Synchronized.change crashes (cons crash);
    6.49      warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
    6.50  
    6.51  fun read_chunk stream len =

     7.1 --- a/src/Pure/System/isar.ML	Wed Jul 06 20:14:13 2011 +0200
     7.2 +++ b/src/Pure/System/isar.ML	Wed Jul 06 20:46:06 2011 +0200
     7.3 @@ -17,7 +17,7 @@
     7.4    val undo: int -> unit
     7.5    val kill: unit -> unit
     7.6    val kill_proof: unit -> unit
     7.7 -  val crashes: exn list Unsynchronized.ref
     7.8 +  val crashes: exn list Synchronized.var
     7.9    val toplevel_loop: TextIO.instream ->
    7.10      {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
    7.11    val loop: unit -> unit
    7.12 @@ -113,7 +113,7 @@
    7.13  
    7.14  (* toplevel loop -- uninterruptible *)
    7.15  
    7.16 -val crashes = Unsynchronized.ref ([]: exn list);
    7.17 +val crashes = Synchronized.var "Isar.crashes" ([]: exn list);
    7.18  
    7.19  local
    7.20  
    7.21 @@ -128,7 +128,7 @@
    7.22      handle exn =>
    7.23        (Output.error_msg (ML_Compiler.exn_message exn)
    7.24          handle crash =>
    7.25 -          (CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
    7.26 +          (Synchronized.change crashes (cons crash);
    7.27              warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
    7.28          raw_loop secure src)
    7.29    end;

     8.1 --- a/src/Pure/context.ML	Wed Jul 06 20:14:13 2011 +0200
     8.2 +++ b/src/Pure/context.ML	Wed Jul 06 20:46:06 2011 +0200
     8.3 @@ -128,10 +128,10 @@
     8.4    extend: Object.T -> Object.T,
     8.5    merge: pretty -> Object.T * Object.T -> Object.T};
     8.6  
     8.7 -val kinds = Unsynchronized.ref (Datatab.empty: kind Datatab.table);
     8.8 +val kinds = Synchronized.var "Theory_Data" (Datatab.empty: kind Datatab.table);
     8.9  
    8.10  fun invoke name f k x =
    8.11 -  (case Datatab.lookup (! kinds) k of
    8.12 +  (case Datatab.lookup (Synchronized.value kinds) k of
    8.13      SOME kind =>
    8.14        if ! timing andalso name <> "" then
    8.15          Timing.cond_timeit true ("Theory_Data." ^ name ^ Position.str_of (#pos kind))
    8.16 @@ -149,7 +149,7 @@
    8.17    let
    8.18      val k = serial ();
    8.19      val kind = {pos = pos, empty = empty, extend = extend, merge = merge};
    8.20 -    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, kind)));
    8.21 +    val _ = Synchronized.change kinds (Datatab.update (k, kind));
    8.22    in k end;
    8.23  
    8.24  val extend_data = Datatab.map invoke_extend;
    8.25 @@ -475,15 +475,15 @@
    8.26  
    8.27  local
    8.28  
    8.29 -val kinds = Unsynchronized.ref (Datatab.empty: (theory -> Object.T) Datatab.table);
    8.30 +val kinds = Synchronized.var "Proof_Data" (Datatab.empty: (theory -> Object.T) Datatab.table);
    8.31  
    8.32  fun invoke_init k =
    8.33 -  (case Datatab.lookup (! kinds) k of
    8.34 +  (case Datatab.lookup (Synchronized.value kinds) k of
    8.35      SOME init => init
    8.36    | NONE => raise Fail "Invalid proof data identifier");
    8.37  
    8.38  fun init_data thy =
    8.39 -  Datatab.map (fn k => fn _ => invoke_init k thy) (! kinds);
    8.40 +  Datatab.map (fn k => fn _ => invoke_init k thy) (Synchronized.value kinds);
    8.41  
    8.42  fun init_new_data data thy =
    8.43    Datatab.merge (K true) (data, init_data thy);
    8.44 @@ -511,7 +511,7 @@
    8.45  fun declare init =
    8.46    let
    8.47      val k = serial ();
    8.48 -    val _ = CRITICAL (fn () => Unsynchronized.change kinds (Datatab.update (k, init)));
    8.49 +    val _ = Synchronized.change kinds (Datatab.update (k, init));
    8.50    in k end;
    8.51  
    8.52  fun get k dest prf =