src/Tools/jEdit/src/plugin.scala
changeset 44185 05641edb5d30
parent 44163 32e0c150c010
child 44221 bff7f7afb2db
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 16:07:26 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Aug 13 20:20:36 2011 +0200
     1.3 @@ -210,8 +210,8 @@
     1.4            case None =>
     1.5              val (master_dir, path) = buffer_path(buffer)
     1.6              Thy_Header.thy_name(path) match {
     1.7 -              case Some(name) =>
     1.8 -                Some(Document_Model.init(session, buffer, master_dir, path, name))
     1.9 +              case Some((prefix, name)) =>
    1.10 +                Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
    1.11                case None => None
    1.12              }
    1.13          }
    1.14 @@ -327,13 +327,17 @@
    1.15  
    1.16    private val file_store = new Session.File_Store
    1.17    {
    1.18 -    def append(master_dir: String, path: Path): String =
    1.19 +    def append(master_dir: String, source_path: Path): String =
    1.20      {
    1.21 -      val vfs = VFSManager.getVFSForPath(master_dir)
    1.22 -      if (vfs.isInstanceOf[FileVFS])
    1.23 -        MiscUtilities.resolveSymlinks(
    1.24 -          vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    1.25 -      else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    1.26 +      val path = source_path.expand
    1.27 +      if (path.is_absolute) Isabelle_System.platform_path(path)
    1.28 +      else {
    1.29 +        val vfs = VFSManager.getVFSForPath(master_dir)
    1.30 +        if (vfs.isInstanceOf[FileVFS])
    1.31 +          MiscUtilities.resolveSymlinks(
    1.32 +            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    1.33 +        else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    1.34 +      }
    1.35      }
    1.36  
    1.37      def require(canonical_name: String)