src/Pure/Thy/thy_load.ML
changeset 7438 2e0e4253b6c3
parent 7190 ba6f09cd7769
child 7901 c21c3d2256ef
equal deleted inserted replaced
7437:0f99a2103ea0 7438:2e0e4253b6c3
     8 signature BASIC_THY_LOAD =
     8 signature BASIC_THY_LOAD =
     9 sig
     9 sig
    10   val show_path: unit -> string list
    10   val show_path: unit -> string list
    11   val add_path: string -> unit
    11   val add_path: string -> unit
    12   val del_path: string -> unit
    12   val del_path: string -> unit
       
    13   val with_path: string -> ('a -> 'b) -> 'a -> 'b
    13   val reset_path: unit -> unit
    14   val reset_path: unit -> unit
    14 end;
    15 end;
    15 
    16 
    16 signature THY_LOAD =
    17 signature THY_LOAD =
    17 sig
    18 sig
    45 
    46 
    46 fun show_path () = map Path.pack (! load_path);
    47 fun show_path () = map Path.pack (! load_path);
    47 fun add_path s = change_path (cons (Path.unpack s));
    48 fun add_path s = change_path (cons (Path.unpack s));
    48 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    49 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    49 fun reset_path () = load_path := [Path.current];
    50 fun reset_path () = load_path := [Path.current];
       
    51 fun with_path s f x = Library.setmp load_path (Path.unpack s :: ! load_path) f x;
    50 
    52 
    51 fun tmp_add_path path f x =
    53 fun cond_with_path path f x =
    52   if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
    54   if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
    53 
    55 
    54 
    56 
    55 (* file formats *)
    57 (* file formats *)
    56 
    58 
    95   (case check_file (thy_path name) of
    97   (case check_file (thy_path name) of
    96     None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
    98     None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
    97       commas_quote (show_path ()))
    99       commas_quote (show_path ()))
    98   | Some thy_info => (thy_info, check_file (ml_path name)));
   100   | Some thy_info => (thy_info, check_file (ml_path name)));
    99 
   101 
   100 fun check_thy dir name = Master (tmp_add_path dir check_thy_aux name);
   102 fun check_thy dir name = Master (cond_with_path dir check_thy_aux name);
   101 
   103 
   102 
   104 
   103 (* process theory files *)
   105 (* process theory files *)
   104 
   106 
   105 (*hooks for theory syntax dependent operations*)
   107 (*hooks for theory syntax dependent operations*)
   107 val deps_thy_fn = ref (undefined: string -> Path.T -> string list * Path.T list);
   109 val deps_thy_fn = ref (undefined: string -> Path.T -> string list * Path.T list);
   108 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
   110 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
   109 
   111 
   110 fun process_thy dir f name =
   112 fun process_thy dir f name =
   111   let val master as Master ((path, _), _) = check_thy dir name
   113   let val master as Master ((path, _), _) = check_thy dir name
   112   in (master, tmp_add_path dir f path) end;
   114   in (master, cond_with_path dir f path) end;
   113 
   115 
   114 fun deps_thy dir name = process_thy dir (! deps_thy_fn name) name;
   116 fun deps_thy dir name = process_thy dir (! deps_thy_fn name) name;
   115 fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name);
   117 fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name);
   116 
   118 
   117 
   119