--- a/src/Pure/Thy/thy_load.ML Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML Tue Sep 29 11:49:22 2009 +0200
@@ -37,14 +37,16 @@
(* maintain load path *)
-local val load_path = ref [Path.current] in
+local val load_path = Unsynchronized.ref [Path.current] in
fun show_path () = map Path.implode (! load_path);
-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 del_path s = CRITICAL (fn () =>
+ Unsynchronized.change load_path (remove (op =) (Path.explode s)));
+fun add_path s = CRITICAL (fn () =>
+ (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
+fun path_add s = CRITICAL (fn () =>
+ (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
fun reset_path () = load_path := [Path.current];
fun with_paths ss f x =
@@ -124,5 +126,5 @@
end;
-structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
-open BasicThyLoad;
+structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
+open Basic_Thy_Load;