# HG changeset patch
# User berghofe
# Date 1093278911 -7200
# Node ID 2ef19a680646d157c0bb5c44421c04713d2e86c0
# Parent  2281784015a51cbb72a74e5d17656f44167a4cd8
begin_theory now takes optional path (current directory) as argument.
This is needed for locating *.ML files connected with theories.

diff -r 2281784015a5 -r 2ef19a680646 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Aug 23 18:33:55 2004 +0200
+++ b/src/Pure/Thy/present.ML	Mon Aug 23 18:35:11 2004 +0200
@@ -24,7 +24,8 @@
   val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
   val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
   val theory_output: string -> string -> unit
-  val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
+  val begin_theory: Path.T option -> 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
@@ -432,16 +433,16 @@
        (html_path name))), name)
   end;
 
-fun begin_theory name raw_parents orig_files thy =
+fun begin_theory optpath 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 ml_path) then [(ml_path, None)] else []);
+      (if is_some (ThyLoad.check_file optpath ml_path) then [(ml_path, None)] else []);
 
     fun prep_file (raw_path, loadit) =
-      (case ThyLoad.check_file raw_path of
+      (case ThyLoad.check_file optpath raw_path of
         Some (path, _) =>
           let
             val base = Path.base path;