# 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;