# HG changeset patch
# User wenzelm
# Date 1313155710 -7200
# Node ID 8848867501fb8af7783fffdad0c462bc0898652b
# Parent  9a35e88d9dc91269a0411d761a8cb9659a7018e9
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);

diff -r 9a35e88d9dc9 -r 8848867501fb src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Aug 12 15:28:30 2011 +0200
@@ -249,14 +249,13 @@
 
 in
 
-fun run_command thy_name raw_tr st =
+fun run_command node_name raw_tr st =
   (case
       (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) ()
+        SOME name =>
+          Exn.capture (fn () =>
+            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
+            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
       | NONE => Exn.Res raw_tr) of
     Exn.Res tr =>
       let
diff -r 9a35e88d9dc9 -r 8848867501fb src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 12 15:28:30 2011 +0200
@@ -51,8 +51,8 @@
     case class Edits[A](edits: List[A]) extends Edit[A]
     case class Update_Header[A](header: Header) extends Edit[A]
 
-    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header])
-    val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
+    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
+    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
 
     val empty: Node = Node(empty_header, Map(), Linear_Set())
 
diff -r 9a35e88d9dc9 -r 8848867501fb src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Pure/Thy/thy_header.ML	Fri Aug 12 15:28:30 2011 +0200
@@ -9,7 +9,6 @@
   val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
   val read: Position.T -> string -> string * string list * (Path.T * bool) list
   val thy_path: string -> Path.T
-  val split_thy_path: Path.T -> Path.T * string
   val consistent_name: string -> string -> unit
 end;
 
@@ -73,11 +72,6 @@
 
 val thy_path = Path.ext "thy" o Path.basic;
 
-fun split_thy_path path =
-  (case Path.split_ext path of
-    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
-  | _ => error ("Bad theory file specification: " ^ Path.print path));
-
 fun consistent_name name name' =
   if name = name' then ()
   else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
diff -r 9a35e88d9dc9 -r 8848867501fb src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 15:28:30 2011 +0200
@@ -26,16 +26,15 @@
   val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
 
-  /* file name */
+  /* theory file name */
+
+  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+
+  def thy_name(s: String): Option[String] =
+    s match { case Thy_Name(name) => Some(name) case _ => None }
 
   def thy_path(name: String): Path = Path.basic(name).ext("thy")
 
-  def split_thy_path(path: Path): (Path, String) =
-    path.split_ext match {
-      case (path1, "thy") => (path1.dir, path1.base.implode)
-      case _ => error("Bad theory file specification: " + path)
-    }
-
 
   /* header */
 
diff -r 9a35e88d9dc9 -r 8848867501fb src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 15:28:30 2011 +0200
@@ -203,9 +203,9 @@
           val node = nodes(name)
           val update_header =
             (node.header.thy_header, header) match {
-              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header)))
-              if thy_header0 != thy_header => true
-              case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true
+              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
+                thy_header0 != thy_header
+              case _ => true
             }
           if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
       }
diff -r 9a35e88d9dc9 -r 8848867501fb src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 15:28:30 2011 +0200
@@ -45,10 +45,11 @@
     }
   }
 
-  def init(session: Session, buffer: Buffer, master_dir: Path, thy_name: String): Document_Model =
+  def init(session: Session, buffer: Buffer,
+    master_dir: String, node_name: String, thy_name: String): Document_Model =
   {
     exit(buffer)
-    val model = new Document_Model(session, buffer, master_dir, thy_name)
+    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
     buffer.setProperty(key, model)
     model.activate()
     model
@@ -56,15 +57,13 @@
 }
 
 
-class Document_Model(val session: Session,
-  val buffer: Buffer, val master_dir: Path, val thy_name: String)
+class Document_Model(val session: Session, val buffer: Buffer,
+  val master_dir: String, val node_name: String, val thy_name: String)
 {
   /* pending text edits */
 
-  private val node_name = (master_dir + Path.basic(thy_name)).implode
-
-  private def node_header(): Document.Node.Header =
-    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
+  def node_header(): Document.Node.Header =
+    Document.Node.Header(master_dir,
       Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
 
   private object pending_edits  // owned by Swing thread
diff -r 9a35e88d9dc9 -r 8848867501fb src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 12:03:17 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 15:28:30 2011 +0200
@@ -23,6 +23,7 @@
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
+import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
 
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.util.Log
@@ -185,6 +186,15 @@
   def buffer_text(buffer: JEditBuffer): String =
     buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
 
+  def buffer_path(buffer: Buffer): (String, String) =
+  {
+    val master_dir = buffer.getDirectory
+    val path = buffer.getSymlinkPath
+    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
+      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
+    else (master_dir, path)
+  }
+
 
   /* document model and view */
 
@@ -198,16 +208,11 @@
         document_model(buffer) match {
           case Some(model) => Some(model)
           case None =>
-            // FIXME strip protocol prefix of URL
-            {
-              try {
-                Some(Thy_Header.split_thy_path(
-                  Path.explode(Isabelle_System.posix_path(buffer.getPath))))
-              }
-              catch { case _ => None }
-            } map {
-              case (master_dir, thy_name) =>
-                Document_Model.init(session, buffer, master_dir, thy_name)
+            val (master_dir, path) = buffer_path(buffer)
+            Thy_Header.thy_name(path) match {
+              case Some(name) =>
+                Some(Document_Model.init(session, buffer, master_dir, path, name))
+              case None => None
             }
         }
       if (opt_model.isDefined) {