# HG changeset patch
# User wenzelm
# Date 1384862276 -3600
# Node ID 570ba266f5b548b78a80cb1a3408782fb8ddbf3c
# Parent  6428dfab652096c665b37ee3a4d32e4e219d2b52
clarified boundary cases of Document.Node.Name;

diff -r 6428dfab6520 -r 570ba266f5b5 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -68,7 +68,7 @@
 
     object Name
     {
-      val empty = Name("", "", "")
+      val empty = Name("")
 
       object Ordering extends scala.math.Ordering[Name]
       {
@@ -76,7 +76,7 @@
       }
     }
 
-    sealed case class Name(node: String, dir: String, theory: String)
+    sealed case class Name(node: String, master_dir: String = "", theory: String = "")
     {
       override def hashCode: Int = node.hashCode
       override def equals(that: Any): Boolean =
diff -r 6428dfab6520 -r 570ba266f5b5 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -339,7 +339,7 @@
           { case Document.Node.Clear() => (Nil, Nil) },  // FIXME unused !?
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
-              val dir = Isabelle_System.posix_path(name.dir)
+              val master_dir = Isabelle_System.posix_path(name.master_dir)
               val imports = header.imports.map(_.node)
               val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
               (Nil,
@@ -347,7 +347,7 @@
                   pair(list(pair(Encode.string,
                     option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
                   list(Encode.string)))))(
-                (dir, (name.theory, (imports, (keywords, header.errors)))))) },
+                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
diff -r 6428dfab6520 -r 570ba266f5b5 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Pure/Thy/thy_info.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -68,7 +68,7 @@
       val dep_files =
         rev_deps.par.map(dep =>
           Exn.capture {
-            dep.load_files(syntax).map(a => Path.explode(dep.name.dir) + Path.explode(a))
+            dep.load_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
           }).toList
       ((Nil: List[Path]) /: dep_files) {
         case (acc_files, files) => Exn.release(files) ::: acc_files
diff -r 6428dfab6520 -r 570ba266f5b5 src/Pure/Thy/thy_load.scala
--- a/src/Pure/Thy/thy_load.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Pure/Thy/thy_load.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -32,9 +32,9 @@
   {
     val path = raw_path.expand
     val node = path.implode
-    val dir = path.dir.implode
     val theory = Thy_Header.thy_name(node).getOrElse("")
-    Document.Node.Name(node, dir, theory)
+    val master_dir = if (theory == "") "" else path.dir.implode
+    Document.Node.Name(node, master_dir, theory)
   }
 
 
@@ -68,12 +68,12 @@
   def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
   {
     val theory = Thy_Header.base_name(s)
-    if (loaded_theories(theory)) Document.Node.Name(theory, "", theory)
+    if (loaded_theories(theory)) Document.Node.Name(theory + ".thy", "", theory)
     else {
       val path = Path.explode(s)
-      val node = append(master.dir, Thy_Load.thy_path(path))
-      val dir = append(master.dir, path.dir)
-      Document.Node.Name(node, dir, theory)
+      val node = append(master.master_dir, Thy_Load.thy_path(path))
+      val master_dir = append(master.master_dir, path.dir)
+      Document.Node.Name(node, master_dir, theory)
     }
   }
 
diff -r 6428dfab6520 -r 570ba266f5b5 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -33,7 +33,7 @@
 
       def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
       var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
-        List((0, node_name.theory, buffer()))
+        List((0, node_name.toString, buffer()))
 
       @tailrec def close(level: Int => Boolean)
       {
@@ -260,7 +260,7 @@
     val files = span_files(syntax, span)
     files.map(file => {
       // FIXME proper thy_load append
-      val file_name = Document.Node.Name(name.dir + file, name.dir, "")
+      val file_name = Document.Node.Name(name.master_dir + file)
       (file_name, all_blobs.get(file_name).map(_.sha1_digest))
     })
   }
diff -r 6428dfab6520 -r 570ba266f5b5 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -137,11 +137,11 @@
 
 
 class Isabelle_Sidekick_Options extends
-  Isabelle_Sidekick_Structure("isabelle-options", b => Some(PIDE.thy_load.dummy_node_name(b)))
+  Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
 
 
 class Isabelle_Sidekick_Root extends
-  Isabelle_Sidekick_Structure("isabelle-root", b => Some(PIDE.thy_load.dummy_node_name(b)))
+  Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
 
 
 class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
diff -r 6428dfab6520 -r 570ba266f5b5 src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -22,13 +22,12 @@
 {
   /* document node names */
 
-  def dummy_node_name(buffer: Buffer): Document.Node.Name =
-    Document.Node.Name(JEdit_Lib.buffer_name(buffer), buffer.getDirectory, buffer.getName)
-
   def node_name(buffer: Buffer): Document.Node.Name =
   {
-    val name = JEdit_Lib.buffer_name(buffer)
-    Document.Node.Name(name, buffer.getDirectory, Thy_Header.thy_name(name).getOrElse(""))
+    val node = JEdit_Lib.buffer_name(buffer)
+    val theory = Thy_Header.thy_name(node).getOrElse("")
+    val master_dir = if (theory == "") "" else buffer.getDirectory
+    Document.Node.Name(node, master_dir, theory)
   }
 
   def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
diff -r 6428dfab6520 -r 570ba266f5b5 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Nov 18 23:46:59 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Nov 19 12:57:56 2013 +0100
@@ -226,7 +226,7 @@
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
-            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             val link = PIDE.editor.hyperlink_file(jedit_file)
             Some(Text.Info(snapshot.convert(info_range), link) :: links)
 
@@ -369,7 +369,7 @@
             Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
           case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
           if Path.is_ok(name) =>
-            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+            val jedit_file = PIDE.thy_load.append(snapshot.node_name.master_dir, Path.explode(name))
             Some(add(prev, r, (true, XML.Text("file " + quote(jedit_file)))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>