equal
deleted
inserted
replaced
35 struct |
35 struct |
36 |
36 |
37 |
37 |
38 (* maintain load path *) |
38 (* maintain load path *) |
39 |
39 |
40 local val load_path = ref [Path.current] in |
40 local val load_path = Unsynchronized.ref [Path.current] in |
41 |
41 |
42 fun show_path () = map Path.implode (! load_path); |
42 fun show_path () = map Path.implode (! load_path); |
43 |
43 |
44 fun del_path s = CRITICAL (fn () => change load_path (remove (op =) (Path.explode s))); |
44 fun del_path s = CRITICAL (fn () => |
45 fun add_path s = CRITICAL (fn () => (del_path s; change load_path (cons (Path.explode s)))); |
45 Unsynchronized.change load_path (remove (op =) (Path.explode s))); |
46 fun path_add s = |
46 fun add_path s = CRITICAL (fn () => |
47 CRITICAL (fn () => (del_path s; change load_path (fn path => path @ [Path.explode s]))); |
47 (del_path s; Unsynchronized.change load_path (cons (Path.explode s)))); |
|
48 fun path_add s = CRITICAL (fn () => |
|
49 (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s]))); |
48 fun reset_path () = load_path := [Path.current]; |
50 fun reset_path () = load_path := [Path.current]; |
49 |
51 |
50 fun with_paths ss f x = |
52 fun with_paths ss f x = |
51 CRITICAL (fn () => Library.setmp load_path (! load_path @ map Path.explode ss) f x); |
53 CRITICAL (fn () => Library.setmp load_path (! load_path @ map Path.explode ss) f x); |
52 fun with_path s f x = with_paths [s] f x; |
54 fun with_path s f x = with_paths [s] f x; |
122 NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path)) |
124 NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path)) |
123 | SOME (path, id) => (ML_Context.eval_file path; (path, id))); |
125 | SOME (path, id) => (ML_Context.eval_file path; (path, id))); |
124 |
126 |
125 end; |
127 end; |
126 |
128 |
127 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad; |
129 structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad; |
128 open BasicThyLoad; |
130 open Basic_Thy_Load; |