src/Tools/jEdit/src/plugin.scala
changeset 44615 a4ff8a787202
parent 44609 6ec4a5eb2fc0
child 44699 5199ee17c7d7
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 11:33:44 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 13:34:45 2011 +0200
     1.3 @@ -168,9 +168,6 @@
     1.4  
     1.5    def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
     1.6  
     1.7 -  def buffer_path(buffer: Buffer): (String, String) =
     1.8 -    (buffer.getDirectory, buffer_name(buffer))
     1.9 -
    1.10  
    1.11    /* main jEdit components */
    1.12  
    1.13 @@ -216,10 +213,11 @@
    1.14          document_model(buffer) match {
    1.15            case Some(model) => Some(model)
    1.16            case None =>
    1.17 -            val (master_dir, path) = buffer_path(buffer)
    1.18 -            Thy_Header.thy_name(path) match {
    1.19 -              case Some(name) =>
    1.20 -                Some(Document_Model.init(session, buffer, master_dir, path, name))
    1.21 +            val name = buffer_name(buffer)
    1.22 +            Thy_Header.thy_name(name) match {
    1.23 +              case Some(theory) =>
    1.24 +                val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
    1.25 +                Some(Document_Model.init(session, buffer, node_name))
    1.26                case None => None
    1.27              }
    1.28          }
    1.29 @@ -363,8 +361,8 @@
    1.30  
    1.31        val thys =
    1.32          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
    1.33 -          yield (model.master_dir, model.thy_name)
    1.34 -      val files = thy_info.dependencies(thys).toList.map(_._1).filterNot(loaded_buffer _)
    1.35 +          yield model.name
    1.36 +      val files = thy_info.dependencies(thys).toList.map(_._1.node).filterNot(loaded_buffer _)
    1.37  
    1.38        if (!files.isEmpty) {
    1.39          val files_list = new ListView(Library.sort_strings(files))