marked some CRITICAL sections;

--- a/src/Pure/Thy/present.ML	Mon Jul 23 20:47:55 2007 +0200
+++ b/src/Pure/Thy/present.ML	Mon Jul 23 20:47:56 2007 +0200
@@ -172,7 +172,7 @@
 (* state *)
 
 val browser_info = ref empty_browser_info;
-fun change_browser_info f = browser_info := map_browser_info f (! browser_info);
+fun change_browser_info f = CRITICAL (fn () => change browser_info (map_browser_info f));
 
 val suppress_tex_source = ref false;
 fun no_document f x = Library.setmp suppress_tex_source true f x;
@@ -290,7 +290,7 @@
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
 fun init build info doc doc_graph doc_versions path name doc_prefix2
-    (remote_path, first_time) verbose thys =
+    (remote_path, first_time) verbose thys = CRITICAL (fn () =>
   if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
     (browser_info := empty_browser_info; session_info := NONE)
   else
@@ -327,7 +327,7 @@
       info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
       browser_info := init_browser_info remote_path path thys;
       add_html_index index_text
-    end;
+    end);
 
 
 (* isatool wrappers *)
@@ -371,8 +371,9 @@
   write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
 
 
-fun finish () = with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
-    documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
+fun finish () = CRITICAL (fn () =>
+    with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
+      documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
   let
     val {theories, files, tex_index, html_index, graph} = ! browser_info;
     val thys = Symtab.dest theories;
@@ -429,7 +430,7 @@
 
     browser_info := empty_browser_info;
     session_info := NONE
-  end);
+  end));
 
 
 (* theory elements *)
@@ -503,7 +504,7 @@
 
 
 val hooks = ref ([]: (string -> (string * thm list) list -> unit) list);
-fun add_hook f = hooks := (f :: ! hooks);
+fun add_hook f = CRITICAL (fn () => change hooks (cons f));
 
 fun results k xs =
  (List.app (fn f => (try (fn () => f k xs) (); ())) (! hooks);

--- a/src/Pure/Thy/thy_load.ML	Mon Jul 23 20:47:55 2007 +0200
+++ b/src/Pure/Thy/thy_load.ML	Mon Jul 23 20:47:56 2007 +0200
@@ -46,16 +46,25 @@
 
 (* maintain load path *)
 
-val load_path = ref [Path.current];
+local val load_path = ref [Path.current] in
 
 fun show_path () = map Path.implode (! load_path);
-fun del_path s = change load_path (remove (op =) (Path.explode s));
-fun add_path s = (del_path s; change load_path (cons (Path.explode s)));
-fun path_add s = (del_path s; change load_path (fn path => path @ [Path.explode s]));
+
+fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s)));
+fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s))));
+fun path_add s =
+  CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s])));
 fun reset_path () = load_path := [Path.current];
-fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
+
+fun with_paths ss f x =
+  CRITICAL (fn () => Library.setmp load_path (! load_path @ map Path.explode ss) f x);
 fun with_path s f x = with_paths [s] f x;
 
+fun search_path dir path =
+  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
+
+end;
+
 
 (* file formats *)
 
@@ -66,10 +75,7 @@
 
 (* check files *)
 
-fun search_path dir path =
-  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
-
-fun check_ext exts dir src_path =
+fun check_ext exts paths dir src_path =
   let
     val path = Path.expand src_path;
     val _ = Path.is_current path andalso error "Bad file specification";
@@ -78,16 +84,19 @@
       let val ext_path = Path.expand (Path.ext ext rel_path)
       in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
     fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
-  in get_first try_prfx (search_path dir path) end;
+  in get_first try_prfx paths end;
 
-val check_file = check_ext [];
-val check_ml = check_ext ml_exts;
+fun check_file dir path = check_ext [] (search_path dir path) dir path;
+fun check_ml dir path = check_ext ml_exts (search_path dir path) dir path;
 
 fun check_thy dir name ml =
-  let val thy_file = thy_path name in
-    (case check_file dir thy_file of
+  let
+    val thy_file = thy_path name;
+    val paths = search_path dir thy_file;
+  in
+    (case check_ext [] paths dir thy_file of
       NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
-        " in " ^ commas_quote (map Path.implode (search_path dir thy_file)))
+        " in " ^ commas_quote (map Path.implode paths))
     | SOME thy_id => (thy_id, if ml then check_file dir (ml_path name) else NONE))
   end;
 

--- a/src/Pure/context.ML	Mon Jul 23 20:47:55 2007 +0200
+++ b/src/Pure/context.ML	Mon Jul 23 20:47:56 2007 +0200
@@ -126,7 +126,7 @@
   let
     val k = serial ();
     val kind = {empty = empty, copy = copy, extend = extend, merge = merge};
-    val _ = change kinds (Datatab.update (k, kind));
+    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, kind)));
   in k end;
 
 val copy_data = Datatab.map' invoke_copy;
@@ -449,7 +449,7 @@
 fun declare init =
   let
     val k = serial ();
-    val _ = change kinds (Datatab.update (k, init));
+    val _ = CRITICAL (fn () => change kinds (Datatab.update (k, init)));
   in k end;
 
 fun get k dest prf =
@@ -494,8 +494,8 @@
 local
   val setup_fn = ref (I: theory -> theory);
 in
-  fun add_setup f = setup_fn := (! setup_fn #> f);
-  fun setup () = let val f = ! setup_fn in setup_fn := I; f end;
+  fun add_setup f = CRITICAL (fn () => setup_fn := (! setup_fn #> f));
+  fun setup () = CRITICAL (fn () => let val f = ! setup_fn in setup_fn := I; f end);
 end;
 
 end;