marked some CRITICAL sections;

--- a/src/Pure/General/output.ML	Mon Jul 23 19:45:45 2007 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 23 19:45:46 2007 +0200
@@ -221,7 +221,7 @@
 
 fun time_accumulator name =
   let val ti = time_init name in
-    change time_finish_hooks (cons (fn () => time_finish ti));
+    CRITICAL (fn () => change time_finish_hooks (cons (fn () => time_finish ti)));
     time_add ti
   end;
 

--- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 23 19:45:45 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 23 19:45:46 2007 +0200
@@ -108,17 +108,17 @@
     Symtab.table);
 val global_markups = ref ([]: (string * ThyOutput.markup) list);
 
-fun change_lexicons f =
+fun change_lexicons f = CRITICAL (fn () =>
   let val lexs = f (! global_lexicons) in
     (case (op inter_string) (pairself Scan.dest_lexicon lexs) of
       [] => global_lexicons := lexs
     | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
-  end;
+  end);
 
-fun make_markups () = global_markups :=
-  Symtab.fold (fn (name, (_, SOME m)) => cons (name, m) | _ => I) (! global_parsers) [];
-
-fun change_parsers f = (Library.change global_parsers f; make_markups ());
+fun change_parsers f = CRITICAL (fn () =>
+ (change global_parsers f;
+  global_markups :=
+    Symtab.fold (fn (name, (_, SOME m)) => cons (name, m) | _ => I) (! global_parsers) []));
 
 in
 
@@ -149,10 +149,10 @@
   else warning ("Redefined outer syntax command " ^ quote name);
   Symtab.update (name, (((comment, kind), (int_only, parse)), markup)) tab);
 
-fun add_parsers parsers =
+fun add_parsers parsers = CRITICAL (fn () =>
   (change_parsers (fold add_parser parsers);
     change_lexicons (apsnd (Scan.extend_lexicon
-      (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
+      (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers)))));
 
 end;
 

--- a/src/Pure/Thy/ml_context.ML	Mon Jul 23 19:45:45 2007 +0200
+++ b/src/Pure/Thy/ml_context.ML	Mon Jul 23 19:45:46 2007 +0200
@@ -68,10 +68,11 @@
     (y, SOME context') => (y, context')
   | (_, NONE) => error "Lost context in ML");
 
-fun save f x = setmp (get_context ()) f x;
+fun save f x = CRITICAL (fn () => setmp (get_context ()) f x);
 
-fun change_theory f =
-  set_context (SOME (Context.map_theory f (the_generic_context ())));
+fun change_theory f = CRITICAL (fn () =>
+  set_context (SOME (Context.map_theory f (the_generic_context ()))));
+
 
 
 (** ML antiquotations **)
@@ -80,8 +81,8 @@
 
 val global_lexicon = ref Scan.empty_lexicon;
 
-fun add_keywords keywords =
-  change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords));
+fun add_keywords keywords = CRITICAL (fn () =>
+  change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)));
 
 
 (* maintain commands *)
@@ -92,10 +93,11 @@
 
 local
 
-fun add_item kind name scan = change global_parsers (fn tab =>
- (if not (Symtab.defined tab name) then ()
-  else warning ("Redefined ML antiquotation: " ^ quote name);
-  Symtab.update (name, scan >> kind) tab));
+fun add_item kind name scan = CRITICAL (fn () =>
+  change global_parsers (fn tab =>
+   (if not (Symtab.defined tab name) then ()
+    else warning ("Redefined ML antiquotation: " ^ quote name);
+    Symtab.update (name, scan >> kind) tab)));
 
 in
 
@@ -115,8 +117,7 @@
   let val ((name, _), pos) = Args.dest_src src in
     (case Symtab.lookup (! global_parsers) name of
       NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
-    | SOME scan => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos))
-        (fn () => syntax scan src) ())
+    | SOME scan => syntax scan src)
   end;
 
 
@@ -137,7 +138,7 @@
 val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
 val isabelle_struct0 = isabelle_struct "";
 
-fun eval_antiquotes txt =
+fun eval_antiquotes txt = CRITICAL (fn () =>
   let
     val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
 
@@ -158,7 +159,7 @@
     val (decls, body) =
       fold_map expand ants ML_Syntax.reserved
       |> #1 |> split_list |> pairself implode;
-  in (isabelle_struct decls, body) end;
+  in (isabelle_struct decls, body) end);
 
 fun eval name verbose txt =
   Output.ML_errors (use_text name Output.ml_output verbose) txt;

--- a/src/Pure/Thy/thy_info.ML	Mon Jul 23 19:45:45 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Jul 23 19:45:46 2007 +0200
@@ -57,7 +57,7 @@
 local
   val hooks = ref ([]: (action -> string -> unit) list);
 in
-  fun add_hook f = hooks := f :: ! hooks;
+  fun add_hook f = CRITICAL (fn () => change hooks (cons f));
   fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks);
 end;
 
@@ -122,7 +122,7 @@
   val database = ref (Graph.empty: thy Graph.T);
 in
   fun get_thys () = ! database;
-  val change_thys = Library.change database;
+  fun change_thys f = CRITICAL (fn () => Library.change database f);
 end;
 
 
@@ -150,7 +150,8 @@
     SOME thy => thy
   | NONE => error (loader_msg "nothing known about theory" [name]));
 
-fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f));
+fun change_thy name f = CRITICAL (fn () =>
+  (get_thy name; change_thys (Graph.map_node name f)));
 
 
 (* access deps *)
@@ -229,8 +230,9 @@
 
 fun outdate_thy name =
   if is_finished name orelse is_outdated name then ()
-  else (change_deps name (Option.map (fn {outdated = _, master, parents, files} =>
-    make_deps true master parents files)); perform Outdate name);
+  else CRITICAL (fn () =>
+   (change_deps name (Option.map (fn {outdated = _, master, parents, files} =>
+    make_deps true master parents files)); perform Outdate name));
 
 fun check_unfinished name =
   if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE)
@@ -317,9 +319,10 @@
     if null missing_files then ()
     else warning (loader_msg "unresolved dependencies of theory" [name] ^
       " on file(s): " ^ commas_quote missing_files);
-    change_deps name
-      (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files));
-    perform Update name
+    CRITICAL (fn () =>
+     (change_deps name
+        (Option.map (fn {parents, ...} => make_deps false (SOME master) parents files));
+      perform Update name))
   end;
 
 
@@ -420,8 +423,7 @@
   else
     let val succs = thy_graph Graph.all_succs [name] in
       priority (loader_msg "removing" succs);
-      List.app (perform Remove) succs;
-      change_thys (Graph.del_nodes succs)
+      CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
     end;
 
 
@@ -496,7 +498,7 @@
   in
     if not (null nonfinished) then err "non-finished parent theories" nonfinished
     else if not (null variants) then err "different versions of parent theories" variants
-    else (change_thys register; perform Update name)
+    else CRITICAL (fn () => (change_thys register; perform Update name))
   end;
 
 val _ = register_theory ProtoPure.thy;