# HG changeset patch
# User wenzelm
# Date 1294936775 -3600
# Node ID 3837045cc8a182974593eb245435c413112f0573
# Parent  47fef6afe756ce8e041d315c6f94fcfd6d7727ab
full theory path enables loading parents via master directory and keeps files strictly separate;

diff -r 47fef6afe756 -r 3837045cc8a1 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Jan 13 17:34:45 2011 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Jan 13 17:39:35 2011 +0100
@@ -214,12 +214,16 @@
 
 in
 
-fun run_command thy_name tr st =
+fun run_command thy_name raw_tr st =
   (case
-      (case Toplevel.init_of tr of
-        SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) ()
-      | NONE => Exn.Result ()) of
-    Exn.Result () =>
+      (case Toplevel.init_of raw_tr of
+        SOME name => Exn.capture (fn () =>
+          let
+            val path = Path.explode thy_name;
+            val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
+          in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
+      | NONE => Exn.Result raw_tr) of
+    Exn.Result tr =>
       let
         val is_init = is_some (Toplevel.init_of tr);
         val is_proof = Keyword.is_proof (Toplevel.name_of tr);
@@ -241,8 +245,8 @@
   | Exn.Exn exn =>
       if Exn.is_interrupt exn then reraise exn
       else
-       (Toplevel.error_msg tr (ML_Compiler.exn_message exn);
-        Toplevel.status tr Markup.failed;
+       (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
+        Toplevel.status raw_tr Markup.failed;
         (false, Toplevel.toplevel)));
 
 end;
diff -r 47fef6afe756 -r 3837045cc8a1 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Jan 13 17:34:45 2011 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Jan 13 17:39:35 2011 +0100
@@ -266,8 +266,8 @@
           case Some(model) => model.refresh; Some(model)
           case None =>
             Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
-              case Some((_, thy_name)) =>
-                Some(Document_Model.init(Isabelle.session, buffer, thy_name))
+              case Some((dir, thy_name)) =>
+                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
               case None => None
             }
         }