src/Tools/jEdit/src/plugin.scala
changeset 44160 8848867501fb
parent 43714 3749d1e6dde9
child 44163 32e0c150c010
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 12:03:17 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Aug 12 15:28:30 2011 +0200
     1.3 @@ -23,6 +23,7 @@
     1.4  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
     1.5  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
     1.6  import org.gjt.sp.jedit.gui.DockableWindowManager
     1.7 +import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
     1.8  
     1.9  import org.gjt.sp.util.SyntaxUtilities
    1.10  import org.gjt.sp.util.Log
    1.11 @@ -185,6 +186,15 @@
    1.12    def buffer_text(buffer: JEditBuffer): String =
    1.13      buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    1.14  
    1.15 +  def buffer_path(buffer: Buffer): (String, String) =
    1.16 +  {
    1.17 +    val master_dir = buffer.getDirectory
    1.18 +    val path = buffer.getSymlinkPath
    1.19 +    if (VFSManager.getVFSForPath(path).isInstanceOf[FileVFS])
    1.20 +      (Isabelle_System.posix_path(master_dir), Isabelle_System.posix_path(path))
    1.21 +    else (master_dir, path)
    1.22 +  }
    1.23 +
    1.24  
    1.25    /* document model and view */
    1.26  
    1.27 @@ -198,16 +208,11 @@
    1.28          document_model(buffer) match {
    1.29            case Some(model) => Some(model)
    1.30            case None =>
    1.31 -            // FIXME strip protocol prefix of URL
    1.32 -            {
    1.33 -              try {
    1.34 -                Some(Thy_Header.split_thy_path(
    1.35 -                  Path.explode(Isabelle_System.posix_path(buffer.getPath))))
    1.36 -              }
    1.37 -              catch { case _ => None }
    1.38 -            } map {
    1.39 -              case (master_dir, thy_name) =>
    1.40 -                Document_Model.init(session, buffer, master_dir, thy_name)
    1.41 +            val (master_dir, path) = buffer_path(buffer)
    1.42 +            Thy_Header.thy_name(path) match {
    1.43 +              case Some(name) =>
    1.44 +                Some(Document_Model.init(session, buffer, master_dir, path, name))
    1.45 +              case None => None
    1.46              }
    1.47          }
    1.48        if (opt_model.isDefined) {