# HG changeset patch
# User wenzelm
# Date 1313179849 -7200
# Node ID 32e0c150c0103433e9a311fc9427074040888ba2
# Parent  5434899d955c1e56da6d7e22a06e3de6afd755ac
normalized theory dependencies wrt. file_store;

diff -r 5434899d955c -r 32e0c150c010 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 12 20:32:25 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 12 22:10:49 2011 +0200
@@ -52,6 +52,15 @@
     case class Update_Header[A](header: Header) extends Edit[A]
 
     sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
+    {
+      def norm_deps(f: (String, Path) => String): Header =
+        copy(thy_header =
+          thy_header match {
+            case Exn.Res(header) =>
+              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
+            case exn => exn
+          })
+    }
     val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
 
     val empty: Node = Node(empty_header, Map(), Linear_Set())
diff -r 5434899d955c -r 32e0c150c010 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Fri Aug 12 20:32:25 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Aug 12 22:10:49 2011 +0200
@@ -20,7 +20,8 @@
 
   abstract class File_Store
   {
-    def read(path: Path): String
+    def append(master_dir: String, path: Path): String
+    def require(file: String): Unit
   }
 
 
@@ -186,7 +187,8 @@
       val syntax = current_syntax()
       val previous = global_state().history.tip.version
       val doc_edits =
-        (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit))
+        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
+          edits.map(edit => (name, edit))
       val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
       val change =
         global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
diff -r 5434899d955c -r 32e0c150c010 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 20:32:25 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 22:10:49 2011 +0200
@@ -110,5 +110,8 @@
 {
   def map(f: String => String): Thy_Header =
     Thy_Header(f(name), imports.map(f), uses.map(f))
+
+  def norm_deps(f: String => String): Thy_Header =
+    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
 }
 
diff -r 5434899d955c -r 32e0c150c010 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 20:32:25 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 22:10:49 2011 +0200
@@ -327,15 +327,20 @@
 
   private val file_store = new Session.File_Store
   {
-    def read(path: Path): String =
+    def append(master_dir: String, path: Path): String =
     {
-      val platform_path = Isabelle_System.platform_path(path)
-      val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
+      val vfs = VFSManager.getVFSForPath(master_dir)
+      if (vfs.isInstanceOf[FileVFS])
+        MiscUtilities.resolveSymlinks(
+          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
+      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
+    }
 
-      Isabelle.jedit_buffers().find(buffer =>
-          MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
-        case Some(buffer) => Isabelle.buffer_text(buffer)
-        case None => Standard_System.read_file(new File(platform_path))
+    def require(canonical_name: String)
+    {
+      Swing_Thread.later {
+        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
+          jEdit.openFile(null: View, canonical_name)
       }
     }
   }