# HG changeset patch
# User wenzelm
# Date 918059112 -3600
# Node ID dd3d3da0f458b914de271d4367fa72f4ff48fcc4
# Parent  c7ad5b27894fdd659d64361e30b4149c5445dc73
added reset_path;
added ml_path;
loader primitives: ml and time arg;

diff -r c7ad5b27894f -r dd3d3da0f458 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Wed Feb 03 17:23:35 1999 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Feb 03 17:25:12 1999 +0100
@@ -10,25 +10,26 @@
   val show_path: unit -> string list
   val add_path: string -> unit
   val del_path: string -> unit
+  val reset_path: unit -> unit
 end;
 
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
-  val thy_ext: string
+  val ml_path: string -> Path.T
   val find_file: Path.T -> (Path.T * File.info) option
   val check_file: Path.T -> File.info option
   val load_file: Path.T -> File.info
   val check_thy: string -> File.info
-  val deps_thy: string -> File.info * (string list * Path.T list)
-  val load_thy: string -> File.info * theory
+  val deps_thy: string -> bool -> File.info * (string list * Path.T list)
+  val load_thy: string -> bool -> bool -> File.info
 end;
 
 signature PRIVATE_THY_LOAD =
 sig
   include THY_LOAD
-  val deps_thy_fn: (Path.T -> string list * Path.T list) ref
-  val load_thy_fn: (Path.T -> theory) ref
+  val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
+  val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
 end;
 
 structure ThyLoad: PRIVATE_THY_LOAD =
@@ -43,6 +44,7 @@
 fun show_path () = map Path.pack (! load_path);
 fun add_path s = change_path (fn path => path @ [Path.unpack s]);
 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
+fun reset_path () = load_path := [Path.current];
 
 
 (* find / check file *)
@@ -65,13 +67,15 @@
     Some (path, info) => (Use.use_path path; info)
   | None => error ("Could not find ML file " ^ quote (Path.pack raw_path)));
 
+val ml_path = Path.ext "ML" o Path.basic;
+
 
 (* process theory files *)
 
-val thy_ext = "thy";
+val thy_ext = Path.ext "thy";
 
 fun process_thy f name =
-  let val path = Path.ext thy_ext (Path.basic name) in
+  let val path = thy_ext (Path.basic name) in
     (case find_file path of
       Some (path, info) => (info, f path)
     | None => error ("Could not find theory file " ^ quote (Path.pack path)))
@@ -79,12 +83,12 @@
 
 (*hooks for theory syntax dependent operations*)
 fun undefined _ = raise Match;
-val deps_thy_fn = ref (undefined: Path.T -> string list * Path.T list);
-val load_thy_fn = ref (undefined: Path.T -> theory);
+val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
+val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
 
 val check_thy = #1 o process_thy (K ());
-val deps_thy = process_thy (fn path => ! deps_thy_fn path);
-val load_thy = process_thy (fn path => ! load_thy_fn path);
+fun deps_thy name ml = process_thy (fn path => ! deps_thy_fn name ml path) name;
+fun load_thy name ml time = #1 (process_thy (fn path => ! load_thy_fn name ml time path) name);
 
 
 end;