added with_paths;
authorwenzelm
Wed Jun 21 20:38:25 2000 +0200 (2000-06-21)
changeset 9103ef56f093259d
parent 9102 c7ba07e3bbe8
child 9104 89ca2a172f84
added with_paths;
src/Pure/Thy/thy_load.ML
     1.1 --- a/src/Pure/Thy/thy_load.ML	Wed Jun 21 18:14:28 2000 +0200
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Wed Jun 21 20:38:25 2000 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    val add_path: string -> unit
     1.5    val del_path: string -> unit
     1.6    val with_path: string -> ('a -> 'b) -> 'a -> 'b
     1.7 +  val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
     1.8    val reset_path: unit -> unit
     1.9  end;
    1.10  
    1.11 @@ -52,6 +53,7 @@
    1.12  fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    1.13  fun reset_path () = load_path := [Path.current];
    1.14  fun with_path s f x = Library.setmp load_path (Path.unpack s :: ! load_path) f x;
    1.15 +fun with_paths ss f x = Library.setmp load_path (map Path.unpack ss @ ! load_path) f x;
    1.16  
    1.17  fun cond_with_path path f x =
    1.18    if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;