# 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) {