src/Tools/jEdit/src/plugin.scala
changeset 44222 9d5ef6cd4ee1
parent 44221 bff7f7afb2db
child 44225 a8f921e6484f
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 12:06:49 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Tue Aug 16 21:13:52 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((prefix, name)) =>
     1.8 -                Some(Document_Model.init(session, buffer, master_dir, prefix + name, name))
     1.9 +              case Some(name) =>
    1.10 +                Some(Document_Model.init(session, buffer, master_dir, path, name))
    1.11                case None => None
    1.12              }
    1.13          }
    1.14 @@ -334,8 +334,8 @@
    1.15        else {
    1.16          val vfs = VFSManager.getVFSForPath(master_dir)
    1.17          if (vfs.isInstanceOf[FileVFS])
    1.18 -          vfs.constructPath(master_dir, Isabelle_System.platform_path(path))
    1.19 -          // FIXME MiscUtilities.resolveSymlinks (!?)
    1.20 +          MiscUtilities.resolveSymlinks(
    1.21 +            vfs.constructPath(master_dir, Isabelle_System.platform_path(path)))
    1.22          else vfs.constructPath(master_dir, Isabelle_System.standard_path(path))
    1.23        }
    1.24      }