# HG changeset patch
# User wenzelm
# Date 1256645776 -3600
# Node ID d27956b4d3b46d5930bef3eb7fce86de33ef3175
# Parent  89ced80833ac90e8a9acdc6f053df76cf50fadce
non-critical atomic accesses;

diff -r 89ced80833ac -r d27956b4d3b4 src/Pure/General/file.ML
--- a/src/Pure/General/file.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/General/file.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -90,10 +90,10 @@
     Unsynchronized.ref (Symtab.empty: {time_stamp: string, id: string} Symtab.table);
 in
 
-fun check_cache (path, time) = CRITICAL (fn () =>
+fun check_cache (path, time) =
   (case Symtab.lookup (! ident_cache) path of
     NONE => NONE
-  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE));
+  | SOME {time_stamp, id} => if time_stamp = time then SOME id else NONE);
 
 fun update_cache (path, (time, id)) = CRITICAL (fn () =>
   Unsynchronized.change ident_cache
diff -r 89ced80833ac -r d27956b4d3b4 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/General/print_mode.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -35,7 +35,7 @@
   let val modes =
     (case Thread.getLocal tag of
       SOME (SOME modes) => modes
-    | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
+    | _ => ! print_mode)
   in subtract (op =) [input, internal] modes end;
 
 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
diff -r 89ced80833ac -r d27956b4d3b4 src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/Isar/isar_document.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -119,13 +119,13 @@
 in
 
 fun change_states f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_states f);
-fun get_states () = NAMED_CRITICAL "Isar" (fn () => ! global_states);
+fun get_states () = ! global_states;
 
 fun change_commands f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_commands f);
-fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
+fun get_commands () = ! global_commands;
 
 fun change_documents f = NAMED_CRITICAL "Isar" (fn () => Unsynchronized.change global_documents f);
-fun get_documents () = NAMED_CRITICAL "Isar" (fn () => ! global_documents);
+fun get_documents () = ! global_documents;
 
 fun init () = NAMED_CRITICAL "Isar" (fn () =>
  (global_states := Symtab.empty;
diff -r 89ced80833ac -r d27956b4d3b4 src/Pure/Isar/outer_keyword.ML
--- a/src/Pure/Isar/outer_keyword.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -121,8 +121,8 @@
 
 in
 
-fun get_commands () = CRITICAL (fn () => ! global_commands);
-fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
+fun get_commands () = ! global_commands;
+fun get_lexicons () = ! global_lexicons;
 
 fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
 fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
diff -r 89ced80833ac -r d27956b4d3b4 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -101,8 +101,8 @@
 
 (* access current syntax *)
 
-fun get_commands () = CRITICAL (fn () => ! global_commands);
-fun get_markups () = CRITICAL (fn () => ! global_markups);
+fun get_commands () = ! global_commands;
+fun get_markups () = ! global_markups;
 
 fun get_command () = Symtab.lookup (get_commands ());
 fun get_syntax () = CRITICAL (fn () => (OuterKeyword.get_lexicons (), get_command ()));
diff -r 89ced80833ac -r d27956b4d3b4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -552,7 +552,7 @@
 local val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list) in
 
 fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f));
-fun get_hooks () = CRITICAL (fn () => ! hooks);
+fun get_hooks () = ! hooks;
 
 end;
 
diff -r 89ced80833ac -r d27956b4d3b4 src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Tue Oct 27 13:15:20 2009 +0100
+++ b/src/Pure/System/isar.ML	Tue Oct 27 13:16:16 2009 +0100
@@ -47,10 +47,10 @@
       | edit n (st, hist) = edit (n - 1) (f st hist);
   in edit count (! global_state, ! global_history) end);
 
-fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
+fun state () = ! global_state;
 
-fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
-fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
+fun exn () = ! global_exn;
+fun set_exn exn =  global_exn := exn;
 
 end;