# HG changeset patch
# User wenzelm
# Date 1310069070 -7200
# Node ID 77ce24aa1770fb21272324aa04b41bdd6b8fa930
# Parent  58bb7ca5c7a2972b95380bf64895645adeb65e6d
explicit Document.Node.Header, with master_dir and thy_name;
imitate ML path operations more closely;

diff -r 58bb7ca5c7a2 -r 77ce24aa1770 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Jul 07 14:10:50 2011 +0200
+++ b/src/Pure/General/path.scala	Thu Jul 07 22:04:30 2011 +0200
@@ -8,6 +8,9 @@
 package isabelle
 
 
+import scala.util.matching.Regex
+
+
 object Path
 {
   /* path elements */
@@ -139,6 +142,17 @@
       prfx + Path.basic(s + "." + e)
     }
 
+  private val Ext = new Regex("(.*)\\.([^.]*)")
+
+  def split_ext: (Path, String) =
+  {
+    val (prefix, base) = split_path
+    base match {
+      case Ext(b, e) => (prefix + Path.basic(b), e)
+      case _ => (Path.basic(base), "")
+    }
+  }
+
 
   /* expand */
 
diff -r 58bb7ca5c7a2 -r 77ce24aa1770 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Jul 07 14:10:50 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Jul 07 22:04:30 2011 +0200
@@ -46,7 +46,10 @@
 
   object Node
   {
-    val empty: Node = new Node(Linear_Set())
+    class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
+    val empty_header = new Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
+
+    val empty: Node = new Node(empty_header, Linear_Set())
 
     def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
       : Iterator[(Command, Text.Offset)] =
@@ -62,8 +65,15 @@
 
   private val block_size = 1024
 
-  class Node(val commands: Linear_Set[Command])
+  class Node(val header: Node.Header, val commands: Linear_Set[Command])
   {
+    /* header */
+
+    def set_header(header: Node.Header): Node = new Node(header, commands)
+
+
+    /* commands */
+
     private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
     {
       val blocks = new mutable.ListBuffer[(Command, Text.Offset)]
diff -r 58bb7ca5c7a2 -r 77ce24aa1770 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Jul 07 14:10:50 2011 +0200
+++ b/src/Pure/System/session.scala	Thu Jul 07 22:04:30 2011 +0200
@@ -159,10 +159,8 @@
   /* actor messages */
 
   private case object Interrupt_Prover
-  private case class Edit_Node(thy_name: String,
-    header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
-  private case class Init_Node(thy_name: String,
-    header: Exn.Result[Thy_Header.Header], text: String)
+  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+  private case class Init_Node(name: String, header: Document.Node.Header, text: String)
   private case class Start(timeout: Time, args: List[String])
 
   var verbose: Boolean = false
@@ -293,15 +291,17 @@
         case Interrupt_Prover =>
           prover.map(_.interrupt)
 
-        case Edit_Node(thy_name, header, text_edits) if prover.isDefined =>
-          edit_version(List((thy_name, Some(text_edits))))
+        case Edit_Node(name, header, text_edits) if prover.isDefined =>
+          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
+          edit_version(List((node_name, Some(text_edits))))
           reply(())
 
-        case Init_Node(thy_name, header, text) if prover.isDefined =>
+        case Init_Node(name, header, text) if prover.isDefined =>
           // FIXME compare with existing node
+          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
           edit_version(List(
-            (thy_name, None),
-            (thy_name, Some(List(Text.Edit.insert(0, text))))))
+            (node_name, None),
+            (node_name, Some(List(Text.Edit.insert(0, text))))))
           reply(())
 
         case change: Document.Change if prover.isDefined =>
@@ -341,14 +341,14 @@
 
   def interrupt() { session_actor ! Interrupt_Prover }
 
-  def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
+  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
   {
-    session_actor !? Edit_Node(thy_name, header, edits)
+    session_actor !? Edit_Node(name, header, edits)
   }
 
-  def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String)
+  def init_node(name: String, header: Document.Node.Header, text: String)
   {
-    session_actor !? Init_Node(thy_name, header, text)
+    session_actor !? Init_Node(name, header, text)
   }
 
   def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
diff -r 58bb7ca5c7a2 -r 77ce24aa1770 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Jul 07 14:10:50 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Thu Jul 07 22:04:30 2011 +0200
@@ -38,14 +38,10 @@
 
   def thy_path(name: String): Path = Path.basic(name).ext("thy")
 
-  private val Thy_Path1 = new Regex("([^/]*)\\.thy")
-  private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
-
-  def split_thy_path(path: String): Option[(String, String)] =
-    path match {
-      case Thy_Path1(name) => Some(("", name))
-      case Thy_Path2(dir, name) => Some((dir, name))
-      case _ => None
+  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)
     }
 
 
diff -r 58bb7ca5c7a2 -r 77ce24aa1770 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Thu Jul 07 14:10:50 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Jul 07 22:04:30 2011 +0200
@@ -181,7 +181,8 @@
           nodes -= name
 
         case (name, Some(text_edits)) =>
-          val commands0 = nodes(name).commands
+          val node = nodes(name)
+          val commands0 = node.commands
           val commands1 = edit_text(text_edits, commands0)
           val commands2 = recover_spans(commands1)   // FIXME somewhat slow
 
@@ -193,7 +194,7 @@
             inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
 
           doc_edits += (name -> Some(cmd_edits))
-          nodes += (name -> new Document.Node(commands2))
+          nodes += (name -> new Document.Node(node.header, commands2))
       }
       (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
     }
diff -r 58bb7ca5c7a2 -r 77ce24aa1770 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jul 07 14:10:50 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jul 07 22:04:30 2011 +0200
@@ -45,7 +45,7 @@
     }
   }
 
-  def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model =
+  def init(session: Session, buffer: Buffer, master_dir: Path, thy_name: String): Document_Model =
   {
     exit(buffer)
     val model = new Document_Model(session, buffer, master_dir, thy_name)
@@ -57,14 +57,13 @@
 
 
 class Document_Model(val session: Session,
-  val buffer: Buffer, val master_dir: String, val thy_name: String)
+  val buffer: Buffer, val master_dir: Path, val thy_name: String)
 {
   /* pending text edits */
 
-  private def capture_header(): Exn.Result[Thy_Header.Header] =
-    Exn.capture {
-      Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength))
-    }
+  private def node_header(): Document.Node.Header =
+    new 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
   {
@@ -78,14 +77,14 @@
         case Nil =>
         case edits =>
           pending.clear
-          session.edit_node(master_dir + "/" + thy_name, capture_header(), edits)
+          session.edit_node(thy_name, node_header(), edits)
       }
     }
 
     def init()
     {
       flush()
-      session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer))
+      session.init_node(thy_name, node_header(), Isabelle.buffer_text(buffer))
     }
 
     private val delay_flush =
@@ -105,7 +104,8 @@
   def snapshot(): Document.Snapshot =
   {
     Swing_Thread.require()
-    session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot())
+    val node_name = (master_dir + Path.basic(thy_name)).implode  // FIXME
+    session.snapshot(node_name, pending_edits.snapshot())
   }
 
 
diff -r 58bb7ca5c7a2 -r 77ce24aa1770 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Jul 07 14:10:50 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jul 07 22:04:30 2011 +0200
@@ -199,10 +199,15 @@
           case Some(model) => Some(model)
           case None =>
             // FIXME strip protocol prefix of URL
-            Thy_Header.split_thy_path(Isabelle_System.posix_path(buffer.getPath)) match {
-              case Some((master_dir, thy_name)) =>
-                Some(Document_Model.init(session, buffer, master_dir, thy_name))
-              case None => None
+            {
+              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)
             }
         }
       if (opt_model.isDefined) {