normalized theory dependencies wrt. file_store;
authorwenzelm
Fri Aug 12 22:10:49 2011 +0200 (2011-08-12)
changeset 4416332e0c150c010
parent 44162 5434899d955c
child 44172 21f97048b478
normalized theory dependencies wrt. file_store;
src/Pure/PIDE/document.scala
src/Pure/System/session.scala
src/Pure/Thy/thy_header.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Aug 12 20:32:25 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Aug 12 22:10:49 2011 +0200
     1.3 @@ -52,6 +52,15 @@
     1.4      case class Update_Header[A](header: Header) extends Edit[A]
     1.5  
     1.6      sealed case class Header(val master_dir: String, val thy_header: Exn.Result[Thy_Header])
     1.7 +    {
     1.8 +      def norm_deps(f: (String, Path) => String): Header =
     1.9 +        copy(thy_header =
    1.10 +          thy_header match {
    1.11 +            case Exn.Res(header) =>
    1.12 +              Exn.capture { header.norm_deps(name => f(master_dir, Path.explode(name))) }
    1.13 +            case exn => exn
    1.14 +          })
    1.15 +    }
    1.16      val empty_header = Header("", Exn.Exn(ERROR("Bad theory header")))
    1.17  
    1.18      val empty: Node = Node(empty_header, Map(), Linear_Set())
     2.1 --- a/src/Pure/System/session.scala	Fri Aug 12 20:32:25 2011 +0200
     2.2 +++ b/src/Pure/System/session.scala	Fri Aug 12 22:10:49 2011 +0200
     2.3 @@ -20,7 +20,8 @@
     2.4  
     2.5    abstract class File_Store
     2.6    {
     2.7 -    def read(path: Path): String
     2.8 +    def append(master_dir: String, path: Path): String
     2.9 +    def require(file: String): Unit
    2.10    }
    2.11  
    2.12  
    2.13 @@ -186,7 +187,8 @@
    2.14        val syntax = current_syntax()
    2.15        val previous = global_state().history.tip.version
    2.16        val doc_edits =
    2.17 -        (name, Document.Node.Update_Header[Text.Edit](header)) :: edits.map(edit => (name, edit))
    2.18 +        (name, Document.Node.Update_Header[Text.Edit](header.norm_deps(file_store.append))) ::
    2.19 +          edits.map(edit => (name, edit))
    2.20        val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, doc_edits) }
    2.21        val change =
    2.22          global_state.change_yield(_.extend_history(previous, doc_edits, result.map(_._2)))
     3.1 --- a/src/Pure/Thy/thy_header.scala	Fri Aug 12 20:32:25 2011 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Aug 12 22:10:49 2011 +0200
     3.3 @@ -110,5 +110,8 @@
     3.4  {
     3.5    def map(f: String => String): Thy_Header =
     3.6      Thy_Header(f(name), imports.map(f), uses.map(f))
     3.7 +
     3.8 +  def norm_deps(f: String => String): Thy_Header =
     3.9 +    copy(imports = imports.map(name => f(name) + ".thy"), uses = uses.map(f))
    3.10  }
    3.11  
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 20:32:25 2011 +0200
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 22:10:49 2011 +0200
     4.3 @@ -327,15 +327,20 @@
     4.4  
     4.5    private val file_store = new Session.File_Store
     4.6    {
     4.7 -    def read(path: Path): String =
     4.8 +    def append(master_dir: String, path: Path): String =
     4.9      {
    4.10 -      val platform_path = Isabelle_System.platform_path(path)
    4.11 -      val canonical_path = MiscUtilities.resolveSymlinks(platform_path)
    4.12 +      val vfs = VFSManager.getVFSForPath(master_dir)
    4.13 +      if (vfs.isInstanceOf[FileVFS])
    4.14 +        MiscUtilities.resolveSymlinks(
    4.15 +          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    4.16 +      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    4.17 +    }
    4.18  
    4.19 -      Isabelle.jedit_buffers().find(buffer =>
    4.20 -          MiscUtilities.resolveSymlinks(buffer.getPath) == canonical_path) match {
    4.21 -        case Some(buffer) => Isabelle.buffer_text(buffer)
    4.22 -        case None => Standard_System.read_file(new File(platform_path))
    4.23 +    def require(canonical_name: String)
    4.24 +    {
    4.25 +      Swing_Thread.later {
    4.26 +        if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name))
    4.27 +          jEdit.openFile(null: View, canonical_name)
    4.28        }
    4.29      }
    4.30    }