simplified ThyLoad interfaces: only one additional directory;

--- a/src/Pure/Isar/outer_syntax.ML	Fri Jul 20 15:29:25 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Jul 20 17:54:15 2007 +0200
@@ -245,9 +245,9 @@
 
 local
 
-fun try_ml_file dirs name time =
+fun try_ml_file dir name time =
   let val path = ThyLoad.ml_path name in
-    if is_none (ThyLoad.check_file dirs path) then ()
+    if is_none (ThyLoad.check_file dir path) then ()
     else
       let
         val _ = legacy_feature ("loading attached ML script " ^ quote (Path.implode path));
@@ -256,9 +256,9 @@
       in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
   end;
 
-fun run_thy dirs name time =
+fun run_thy dir name time =
   let
-    val master as ((path, _), _) = ThyLoad.check_thy dirs name false;
+    val master as ((path, _), _) = ThyLoad.check_thy dir name false;
     val text = Source.of_list (Library.untabify (explode (File.read path)));
 
     val _ = Present.init_theory name;
@@ -280,11 +280,11 @@
 
   in master end;
 
-fun load_thy dirs name ml time =
+fun load_thy dir name ml time =
   let
-    val master = run_thy dirs name time;
+    val master = run_thy dir name time;
     val _ = ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
-    val _ = if ml then try_ml_file dirs name time else ();
+    val _ = if ml then try_ml_file dir name time else ();
   in master end;
 
 in

--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Jul 20 15:29:25 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Fri Jul 20 17:54:15 2007 +0200
@@ -80,7 +80,7 @@
                NONE => (NONE, NONE)
              | SOME fname =>
                let val path = Path.explode fname in
-                 case ThyLoad.check_file [] path of
+                 case ThyLoad.check_file Path.current path of
                    SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
                  | NONE => (NONE, SOME fname)
                end);

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 20 15:29:25 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Fri Jul 20 17:54:15 2007 +0200
@@ -692,14 +692,14 @@
 
         fun filerefs f =
             let val thy = thy_name f
-                val (_, (_,filerefs)) = ThyLoad.deps_thy [Path.dir f] thy true
+                val (_, (_,filerefs)) = ThyLoad.deps_thy (Path.dir f) thy true
             in
                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
                                      name=NONE, idtables=[], fileurls=filerefs})
             end
 
         fun thyrefs thy =
-            let val (_, (thyrefs,_)) = ThyLoad.deps_thy [] thy true
+            let val (_, (thyrefs,_)) = ThyLoad.deps_thy Path.current thy true
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,

--- a/src/Pure/Thy/present.ML	Fri Jul 20 15:29:25 2007 +0200
+++ b/src/Pure/Thy/present.ML	Fri Jul 20 17:54:15 2007 +0200
@@ -25,8 +25,7 @@
   val init_theory: string -> unit
   val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
   val theory_output: string -> string -> unit
-  val begin_theory: Path.T list -> string -> string list ->
-    (Path.T * bool) list -> theory -> theory
+  val begin_theory: Path.T -> string -> string list -> (Path.T * bool) list -> theory -> theory
   val add_hook: (string -> (string * thm list) list -> unit) -> unit
   val results: string -> (string * thm list) list -> unit
   val theorem: string -> thm -> unit
@@ -452,16 +451,16 @@
        (html_path name))), name)
   end;
 
-fun begin_theory dirs name raw_parents orig_files thy =
+fun begin_theory dir name raw_parents orig_files thy =
     with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
   let
     val parents = map (parent_link remote_path path) raw_parents;
     val ml_path = ThyLoad.ml_path name;
     val files = map (apsnd SOME) orig_files @
-      (if is_some (ThyLoad.check_file dirs ml_path) then [(ml_path, NONE)] else []);
+      (if is_some (ThyLoad.check_file dir ml_path) then [(ml_path, NONE)] else []);
 
     fun prep_file (raw_path, loadit) =
-      (case ThyLoad.check_ml dirs raw_path of
+      (case ThyLoad.check_ml dir raw_path of
         SOME (path, _) =>
           let
             val base = Path.base path;
@@ -471,8 +470,9 @@
               HTML.ml_file (Url.File base) (File.read path));
             (SOME (Url.File base_html), Url.File raw_path, loadit)
           end
-      | NONE => (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
-          (NONE, Url.File raw_path, loadit)));
+      | NONE =>
+          (warning ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path));
+            (NONE, Url.File raw_path, loadit)));
 
     val files_html = map prep_file files;