1.1 --- a/src/Pure/General/path.scala	Thu Jul 07 14:10:50 2011 +0200
     1.2 +++ b/src/Pure/General/path.scala	Thu Jul 07 22:04:30 2011 +0200
     1.3 @@ -8,6 +8,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.util.matching.Regex
     1.8 +
     1.9 +
    1.10  object Path
    1.11  {
    1.12    /* path elements */
    1.13 @@ -139,6 +142,17 @@
    1.14        prfx + Path.basic(s + "." + e)
    1.15      }
    1.16  
    1.17 +  private val Ext = new Regex("(.*)\\.([^.]*)")
    1.18 +
    1.19 +  def split_ext: (Path, String) =
    1.20 +  {
    1.21 +    val (prefix, base) = split_path
    1.22 +    base match {
    1.23 +      case Ext(b, e) => (prefix + Path.basic(b), e)
    1.24 +      case _ => (Path.basic(base), "")
    1.25 +    }
    1.26 +  }
    1.27 +
    1.28  
    1.29    /* expand */
    1.30  

     2.1 --- a/src/Pure/PIDE/document.scala	Thu Jul 07 14:10:50 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Jul 07 22:04:30 2011 +0200
     2.3 @@ -46,7 +46,10 @@
     2.4  
     2.5    object Node
     2.6    {
     2.7 -    val empty: Node = new Node(Linear_Set())
     2.8 +    class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header.Header])
     2.9 +    val empty_header = new Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
    2.10 +
    2.11 +    val empty: Node = new Node(empty_header, Linear_Set())
    2.12  
    2.13      def command_starts(commands: Iterator[Command], offset: Text.Offset = 0)
    2.14        : Iterator[(Command, Text.Offset)] =
    2.15 @@ -62,8 +65,15 @@
    2.16  
    2.17    private val block_size = 1024
    2.18  
    2.19 -  class Node(val commands: Linear_Set[Command])
    2.20 +  class Node(val header: Node.Header, val commands: Linear_Set[Command])
    2.21    {
    2.22 +    /* header */
    2.23 +
    2.24 +    def set_header(header: Node.Header): Node = new Node(header, commands)
    2.25 +
    2.26 +
    2.27 +    /* commands */
    2.28 +
    2.29      private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) =
    2.30      {
    2.31        val blocks = new mutable.ListBuffer[(Command, Text.Offset)]

     3.1 --- a/src/Pure/System/session.scala	Thu Jul 07 14:10:50 2011 +0200
     3.2 +++ b/src/Pure/System/session.scala	Thu Jul 07 22:04:30 2011 +0200
     3.3 @@ -159,10 +159,8 @@
     3.4    /* actor messages */
     3.5  
     3.6    private case object Interrupt_Prover
     3.7 -  private case class Edit_Node(thy_name: String,
     3.8 -    header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
     3.9 -  private case class Init_Node(thy_name: String,
    3.10 -    header: Exn.Result[Thy_Header.Header], text: String)
    3.11 +  private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
    3.12 +  private case class Init_Node(name: String, header: Document.Node.Header, text: String)
    3.13    private case class Start(timeout: Time, args: List[String])
    3.14  
    3.15    var verbose: Boolean = false
    3.16 @@ -293,15 +291,17 @@
    3.17          case Interrupt_Prover =>
    3.18            prover.map(_.interrupt)
    3.19  
    3.20 -        case Edit_Node(thy_name, header, text_edits) if prover.isDefined =>
    3.21 -          edit_version(List((thy_name, Some(text_edits))))
    3.22 +        case Edit_Node(name, header, text_edits) if prover.isDefined =>
    3.23 +          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
    3.24 +          edit_version(List((node_name, Some(text_edits))))
    3.25            reply(())
    3.26  
    3.27 -        case Init_Node(thy_name, header, text) if prover.isDefined =>
    3.28 +        case Init_Node(name, header, text) if prover.isDefined =>
    3.29            // FIXME compare with existing node
    3.30 +          val node_name = (header.master_dir + Path.basic(name)).implode  // FIXME
    3.31            edit_version(List(
    3.32 -            (thy_name, None),
    3.33 -            (thy_name, Some(List(Text.Edit.insert(0, text))))))
    3.34 +            (node_name, None),
    3.35 +            (node_name, Some(List(Text.Edit.insert(0, text))))))
    3.36            reply(())
    3.37  
    3.38          case change: Document.Change if prover.isDefined =>
    3.39 @@ -341,14 +341,14 @@
    3.40  
    3.41    def interrupt() { session_actor ! Interrupt_Prover }
    3.42  
    3.43 -  def edit_node(thy_name: String, header: Exn.Result[Thy_Header.Header], edits: List[Text.Edit])
    3.44 +  def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
    3.45    {
    3.46 -    session_actor !? Edit_Node(thy_name, header, edits)
    3.47 +    session_actor !? Edit_Node(name, header, edits)
    3.48    }
    3.49  
    3.50 -  def init_node(thy_name: String, header: Exn.Result[Thy_Header.Header], text: String)
    3.51 +  def init_node(name: String, header: Document.Node.Header, text: String)
    3.52    {
    3.53 -    session_actor !? Init_Node(thy_name, header, text)
    3.54 +    session_actor !? Init_Node(name, header, text)
    3.55    }
    3.56  
    3.57    def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =

     4.1 --- a/src/Pure/Thy/thy_header.scala	Thu Jul 07 14:10:50 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Jul 07 22:04:30 2011 +0200
     4.3 @@ -38,14 +38,10 @@
     4.4  
     4.5    def thy_path(name: String): Path = Path.basic(name).ext("thy")
     4.6  
     4.7 -  private val Thy_Path1 = new Regex("([^/]*)\\.thy")
     4.8 -  private val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy")
     4.9 -
    4.10 -  def split_thy_path(path: String): Option[(String, String)] =
    4.11 -    path match {
    4.12 -      case Thy_Path1(name) => Some(("", name))
    4.13 -      case Thy_Path2(dir, name) => Some((dir, name))
    4.14 -      case _ => None
    4.15 +  def split_thy_path(path: Path): (Path, String) =
    4.16 +    path.split_ext match {
    4.17 +      case (path1, "thy") => (path1.dir, path1.base.implode)
    4.18 +      case _ => error("Bad theory file specification: " + path)
    4.19      }
    4.20  
    4.21  

     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Thu Jul 07 14:10:50 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Thu Jul 07 22:04:30 2011 +0200
     5.3 @@ -181,7 +181,8 @@
     5.4            nodes -= name
     5.5  
     5.6          case (name, Some(text_edits)) =>
     5.7 -          val commands0 = nodes(name).commands
     5.8 +          val node = nodes(name)
     5.9 +          val commands0 = node.commands
    5.10            val commands1 = edit_text(text_edits, commands0)
    5.11            val commands2 = recover_spans(commands1)   // FIXME somewhat slow
    5.12  
    5.13 @@ -193,7 +194,7 @@
    5.14              inserted_commands.map(cmd => (commands2.prev(cmd), Some(cmd)))
    5.15  
    5.16            doc_edits += (name -> Some(cmd_edits))
    5.17 -          nodes += (name -> new Document.Node(commands2))
    5.18 +          nodes += (name -> new Document.Node(node.header, commands2))
    5.19        }
    5.20        (doc_edits.toList, new Document.Version(Document.new_id(), nodes))
    5.21      }

     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Thu Jul 07 14:10:50 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Thu Jul 07 22:04:30 2011 +0200
     6.3 @@ -45,7 +45,7 @@
     6.4      }
     6.5    }
     6.6  
     6.7 -  def init(session: Session, buffer: Buffer, master_dir: String, thy_name: String): Document_Model =
     6.8 +  def init(session: Session, buffer: Buffer, master_dir: Path, thy_name: String): Document_Model =
     6.9    {
    6.10      exit(buffer)
    6.11      val model = new Document_Model(session, buffer, master_dir, thy_name)
    6.12 @@ -57,14 +57,13 @@
    6.13  
    6.14  
    6.15  class Document_Model(val session: Session,
    6.16 -  val buffer: Buffer, val master_dir: String, val thy_name: String)
    6.17 +  val buffer: Buffer, val master_dir: Path, val thy_name: String)
    6.18  {
    6.19    /* pending text edits */
    6.20  
    6.21 -  private def capture_header(): Exn.Result[Thy_Header.Header] =
    6.22 -    Exn.capture {
    6.23 -      Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength))
    6.24 -    }
    6.25 +  private def node_header(): Document.Node.Header =
    6.26 +    new Document.Node.Header(master_dir,
    6.27 +      Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
    6.28  
    6.29    private object pending_edits  // owned by Swing thread
    6.30    {
    6.31 @@ -78,14 +77,14 @@
    6.32          case Nil =>
    6.33          case edits =>
    6.34            pending.clear
    6.35 -          session.edit_node(master_dir + "/" + thy_name, capture_header(), edits)
    6.36 +          session.edit_node(thy_name, node_header(), edits)
    6.37        }
    6.38      }
    6.39  
    6.40      def init()
    6.41      {
    6.42        flush()
    6.43 -      session.init_node(master_dir + "/" + thy_name, capture_header(), Isabelle.buffer_text(buffer))
    6.44 +      session.init_node(thy_name, node_header(), Isabelle.buffer_text(buffer))
    6.45      }
    6.46  
    6.47      private val delay_flush =
    6.48 @@ -105,7 +104,8 @@
    6.49    def snapshot(): Document.Snapshot =
    6.50    {
    6.51      Swing_Thread.require()
    6.52 -    session.snapshot(master_dir + "/" + thy_name, pending_edits.snapshot())
    6.53 +    val node_name = (master_dir + Path.basic(thy_name)).implode  // FIXME
    6.54 +    session.snapshot(node_name, pending_edits.snapshot())
    6.55    }
    6.56  
    6.57  

     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Jul 07 14:10:50 2011 +0200
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Jul 07 22:04:30 2011 +0200
     7.3 @@ -199,10 +199,15 @@
     7.4            case Some(model) => Some(model)
     7.5            case None =>
     7.6              // FIXME strip protocol prefix of URL
     7.7 -            Thy_Header.split_thy_path(Isabelle_System.posix_path(buffer.getPath)) match {
     7.8 -              case Some((master_dir, thy_name)) =>
     7.9 -                Some(Document_Model.init(session, buffer, master_dir, thy_name))
    7.10 -              case None => None
    7.11 +            {
    7.12 +              try {
    7.13 +                Some(Thy_Header.split_thy_path(
    7.14 +                  Path.explode(Isabelle_System.posix_path(buffer.getPath))))
    7.15 +              }
    7.16 +              catch { case _ => None }
    7.17 +            } map {
    7.18 +              case (master_dir, thy_name) =>
    7.19 +                Document_Model.init(session, buffer, master_dir, thy_name)
    7.20              }
    7.21          }
    7.22        if (opt_model.isDefined) {