explicit Document.Node.Header, with master_dir and thy_name;
imitate ML path operations more closely;
--- 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 */
--- 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)]
--- 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 =
--- 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)
}
--- 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))
}
--- 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())
}
--- 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) {