added node_name(String): imitate jEdit buffer operations;
authorwenzelm
Sun Jan 08 19:08:26 2017 +0100 (2017-01-08 ago)
changeset 64841d53696aed874
parent 64840 d67253005c0c
child 64842 9c69b495c05d
added node_name(String): imitate jEdit buffer operations;
more uniform get_file_content for external source file references;
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 17:53:44 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 08 19:08:26 2017 +0100
     1.3 @@ -90,14 +90,17 @@
     1.4      }
     1.5      yield {
     1.6        Line.Node_Range(file.getPath,
     1.7 -        resources.get_file_content(file) match {
     1.8 -          case Some(text) if range.start > 0 =>
     1.9 -            val chunk = Symbol.Text_Chunk(text)
    1.10 -            val doc = Line.Document(text, resources.text_length)
    1.11 -            doc.range(chunk.decode(range))
    1.12 -          case _ =>
    1.13 -            Line.Range(Line.Position((line1 - 1) max 0))
    1.14 -        })
    1.15 +        if (range.start > 0) {
    1.16 +          resources.get_file_content(file) match {
    1.17 +            case Some(text) =>
    1.18 +              val chunk = Symbol.Text_Chunk(text)
    1.19 +              val doc = Line.Document(text, resources.text_length)
    1.20 +              doc.range(chunk.decode(range))
    1.21 +            case _ =>
    1.22 +              Line.Range(Line.Position((line1 - 1) max 0))
    1.23 +          }
    1.24 +        }
    1.25 +        else Line.Range(Line.Position((line1 - 1) max 0)))
    1.26      }
    1.27    }
    1.28  
     2.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 17:53:44 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Jan 08 19:08:26 2017 +0100
     2.3 @@ -250,19 +250,22 @@
     2.4      : Option[Hyperlink] =
     2.5    {
     2.6      for (name <- PIDE.resources.source_file(source_name)) yield {
     2.7 -      JEdit_Lib.jedit_buffer(name) match {
     2.8 -        case Some(buffer) if offset > 0 =>
     2.9 -          val pos =
    2.10 -            JEdit_Lib.buffer_lock(buffer) {
    2.11 +      def hyperlink(pos: Line.Position) =
    2.12 +        hyperlink_file(focus, Line.Node_Position(name, pos))
    2.13 +
    2.14 +      if (offset > 0) {
    2.15 +        PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match {
    2.16 +          case Some(text) =>
    2.17 +            hyperlink(
    2.18                (Line.Position.zero /:
    2.19 -                (Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
    2.20 +                (Symbol.iterator(text).
    2.21                    zipWithIndex.takeWhile(p => p._2 < offset - 1).
    2.22 -                  map(_._1)))(_.advance(_, Text.Length))
    2.23 -            }
    2.24 -          hyperlink_file(focus, Line.Node_Position(name, pos))
    2.25 -        case _ =>
    2.26 -          hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0)))
    2.27 +                  map(_._1)))(_.advance(_, Text.Length)))
    2.28 +          case None =>
    2.29 +            hyperlink(Line.Position((line1 - 1) max 0))
    2.30 +        }
    2.31        }
    2.32 +      else hyperlink(Line.Position((line1 - 1) max 0))
    2.33      }
    2.34    }
    2.35  
     3.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 17:53:44 2017 +0100
     3.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 19:08:26 2017 +0100
     3.3 @@ -43,6 +43,15 @@
     3.4      Document.Node.Name(node, master_dir, theory)
     3.5    }
     3.6  
     3.7 +  def node_name(path: String): Document.Node.Name =
     3.8 +  {
     3.9 +    val vfs = VFSManager.getVFSForPath(path)
    3.10 +    val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
    3.11 +    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
    3.12 +    val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
    3.13 +    Document.Node.Name(node, master_dir, theory)
    3.14 +  }
    3.15 +
    3.16    def theory_node_name(buffer: Buffer): Option[Document.Node.Name] =
    3.17    {
    3.18      val name = node_name(buffer)
    3.19 @@ -79,14 +88,20 @@
    3.20      catch { case ERROR(_) => None }
    3.21    }
    3.22  
    3.23 +  def get_file_content(node_name: Document.Node.Name): Option[String] =
    3.24 +    Document_Model.get(node_name) match {
    3.25 +      case Some(model: Buffer_Model) => Some(JEdit_Lib.buffer_text(model.buffer))
    3.26 +      case Some(model: File_Model) => Some(model.content.text)
    3.27 +      case None => read_file_content(node_name)
    3.28 +    }
    3.29 +
    3.30    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    3.31    {
    3.32      GUI_Thread.now {
    3.33        Document_Model.get(name) match {
    3.34 -        case Some(buffer_model: Buffer_Model) =>
    3.35 -          val buffer = buffer_model.buffer
    3.36 -          JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) }
    3.37 -        case Some(file_model: File_Model) => Some(f(Scan.char_reader(file_model.content.text)))
    3.38 +        case Some(model: Buffer_Model) =>
    3.39 +          JEdit_Lib.buffer_lock(model.buffer) { Some(f(JEdit_Lib.buffer_reader(model.buffer))) }
    3.40 +        case Some(model: File_Model) => Some(f(Scan.char_reader(model.content.text)))
    3.41          case None => None
    3.42        }
    3.43      } getOrElse {