clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
authorwenzelm
Fri Aug 12 15:28:30 2011 +0200 (2011-08-12 ago)
changeset 441608848867501fb
parent 44159 9a35e88d9dc9
child 44161 c1da9897b6c9
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
src/Pure/PIDE/document.ML
src/Pure/PIDE/document.scala
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Aug 12 12:03:17 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Aug 12 15:28:30 2011 +0200
     1.3 @@ -249,14 +249,13 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun run_command thy_name raw_tr st =
     1.8 +fun run_command node_name raw_tr st =
     1.9    (case
    1.10        (case Toplevel.init_of raw_tr of
    1.11 -        SOME name => Exn.capture (fn () =>
    1.12 -          let
    1.13 -            val path = Path.explode thy_name;
    1.14 -            val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
    1.15 -          in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
    1.16 +        SOME name =>
    1.17 +          Exn.capture (fn () =>
    1.18 +            let val master_dir = Path.dir (Path.explode node_name);  (* FIXME move to Scala side *)
    1.19 +            in Toplevel.modify_master (SOME master_dir) raw_tr end) ()
    1.20        | NONE => Exn.Res raw_tr) of
    1.21      Exn.Res tr =>
    1.22        let
     2.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 12 12:03:17 2011 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 12 15:28:30 2011 +0200
     2.3 @@ -51,8 +51,8 @@
     2.4      case class Edits[A](edits: List[A]) extends Edit[A]
     2.5      case class Update_Header[A](header: Header) extends Edit[A]
     2.6  
     2.7 -    sealed case class Header(val master_dir: Path, val thy_header: Exn.Result[Thy_Header])
     2.8 -    val empty_header = Header(Path.current, Exn.Exn(ERROR("Bad theory header")))
     2.9 +    sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
    2.10 +    val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    2.11  
    2.12      val empty: Node = Node(empty_header, Map(), Linear_Set())
    2.13  
     3.1 --- a/src/Pure/Thy/thy_header.ML	Fri Aug 12 12:03:17 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Aug 12 15:28:30 2011 +0200
     3.3 @@ -9,7 +9,6 @@
     3.4    val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
     3.5    val read: Position.T -> string -> string * string list * (Path.T * bool) list
     3.6    val thy_path: string -> Path.T
     3.7 -  val split_thy_path: Path.T -> Path.T * string
     3.8    val consistent_name: string -> string -> unit
     3.9  end;
    3.10  
    3.11 @@ -73,11 +72,6 @@
    3.12  
    3.13  val thy_path = Path.ext "thy" o Path.basic;
    3.14  
    3.15 -fun split_thy_path path =
    3.16 -  (case Path.split_ext path of
    3.17 -    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
    3.18 -  | _ => error ("Bad theory file specification: " ^ Path.print path));
    3.19 -
    3.20  fun consistent_name name name' =
    3.21    if name = name' then ()
    3.22    else error ("Bad file name " ^ Path.print (thy_path name) ^ " for theory " ^ quote name');
     4.1 --- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 12:03:17 2011 +0200
     4.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 15:28:30 2011 +0200
     4.3 @@ -26,16 +26,15 @@
     4.4    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
     4.5  
     4.6  
     4.7 -  /* file name */
     4.8 +  /* theory file name */
     4.9 +
    4.10 +  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
    4.11 +
    4.12 +  def thy_name(s: String): Option[String] =
    4.13 +    s match { case Thy_Name(name) => Some(name) case _ => None }
    4.14  
    4.15    def thy_path(name: String): Path = Path.basic(name).ext("thy")
    4.16  
    4.17 -  def split_thy_path(path: Path): (Path, String) =
    4.18 -    path.split_ext match {
    4.19 -      case (path1, "thy") => (path1.dir, path1.base.implode)
    4.20 -      case _ => error("Bad theory file specification: " + path)
    4.21 -    }
    4.22 -
    4.23  
    4.24    /* header */
    4.25  
     5.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 12:03:17 2011 +0200
     5.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Aug 12 15:28:30 2011 +0200
     5.3 @@ -203,9 +203,9 @@
     5.4            val node = nodes(name)
     5.5            val update_header =
     5.6              (node.header.thy_header, header) match {
     5.7 -              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header)))
     5.8 -              if thy_header0 != thy_header => true
     5.9 -              case (Exn.Exn(_), Document.Node.Header(_, Exn.Res(thy_header))) => true
    5.10 +              case (Exn.Res(thy_header0), Document.Node.Header(_, Exn.Res(thy_header))) =>
    5.11 +                thy_header0 != thy_header
    5.12 +              case _ => true
    5.13              }
    5.14            if (update_header) doc_edits += (name -> Document.Node.Update_Header(header))
    5.15        }
     6.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 12:03:17 2011 +0200
     6.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Aug 12 15:28:30 2011 +0200
     6.3 @@ -45,10 +45,11 @@
     6.4      }
     6.5    }
     6.6  
     6.7 -  def init(session: Session, buffer: Buffer, master_dir: Path, thy_name: String): Document_Model =
     6.8 +  def init(session: Session, buffer: Buffer,
     6.9 +    master_dir: String, node_name: String, thy_name: String): Document_Model =
    6.10    {
    6.11      exit(buffer)
    6.12 -    val model = new Document_Model(session, buffer, master_dir, thy_name)
    6.13 +    val model = new Document_Model(session, buffer, master_dir, node_name, thy_name)
    6.14      buffer.setProperty(key, model)
    6.15      model.activate()
    6.16      model
    6.17 @@ -56,15 +57,13 @@
    6.18  }
    6.19  
    6.20  
    6.21 -class Document_Model(val session: Session,
    6.22 -  val buffer: Buffer, val master_dir: Path, val thy_name: String)
    6.23 +class Document_Model(val session: Session, val buffer: Buffer,
    6.24 +  val master_dir: String, val node_name: String, val thy_name: String)
    6.25  {
    6.26    /* pending text edits */
    6.27  
    6.28 -  private val node_name = (master_dir + Path.basic(thy_name)).implode
    6.29 -
    6.30 -  private def node_header(): Document.Node.Header =
    6.31 -    Document.Node.Header(Path.current,  // FIXME master_dir (!?)
    6.32 +  def node_header(): Document.Node.Header =
    6.33 +    Document.Node.Header(master_dir,
    6.34        Exn.capture { Thy_Header.check(thy_name, buffer.getSegment(0, buffer.getLength)) })
    6.35  
    6.36    private object pending_edits  // owned by Swing thread
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 12:03:17 2011 +0200
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 15:28:30 2011 +0200
     7.3 @@ -23,6 +23,7 @@
     7.4  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
     7.5  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
     7.6  import org.gjt.sp.jedit.gui.DockableWindowManager
     7.7 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
     7.8  
     7.9  import org.gjt.sp.util.SyntaxUtilities
    7.10  import org.gjt.sp.util.Log
    7.11 @@ -185,6 +186,15 @@
    7.12    def buffer_text(buffer: JEditBuffer): String =
    7.13      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    7.14  
    7.15 +  def buffer_path(buffer: Buffer): (String, String) =
    7.16 +  {
    7.17 +    val master_dir = buffer.getDirectory
    7.18 +    val path = buffer.getSymlinkPath
    7.19 +    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
    7.20 +      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
    7.21 +    else (master_dir, path)
    7.22 +  }
    7.23 +
    7.24  
    7.25    /* document model and view */
    7.26  
    7.27 @@ -198,16 +208,11 @@
    7.28          document_model(buffer) match {
    7.29            case Some(model) => Some(model)
    7.30            case None =>
    7.31 -            // FIXME strip protocol prefix of URL
    7.32 -            {
    7.33 -              try {
    7.34 -                Some(Thy_Header.split_thy_path(
    7.35 -                  Path.explode(Isabelle_System.posix_path(buffer.getPath))))
    7.36 -              }
    7.37 -              catch { case _ => None }
    7.38 -            } map {
    7.39 -              case (master_dir, thy_name) =>
    7.40 -                Document_Model.init(session, buffer, master_dir, thy_name)
    7.41 +            val (master_dir, path) = buffer_path(buffer)
    7.42 +            Thy_Header.thy_name(path) match {
    7.43 +              case Some(name) =>
    7.44 +                Some(Document_Model.init(session, buffer, master_dir, path, name))
    7.45 +              case None => None
    7.46              }
    7.47          }
    7.48        if (opt_model.isDefined) {