tuned;
authorwenzelm
Sun Jan 08 14:46:04 2017 +0100 (2017-01-08 ago)
changeset 648340a7179ad430d
parent 64833 0f410e3b1d20
child 64835 fd1efd6dd385
tuned;
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/jEdit/src/jedit_resources.scala
     1.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 13:08:17 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Jan 08 14:46:04 2017 +0100
     1.3 @@ -67,6 +67,28 @@
     1.4      else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
     1.5    }
     1.6  
     1.7 +  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
     1.8 +  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
     1.9 +
    1.10 +
    1.11 +  /* file content */
    1.12 +
    1.13 +  def read_file_content(file: JFile): Option[String] =
    1.14 +    try { Some(Line.normalize(File.read(file))) }
    1.15 +    catch { case ERROR(_) => None }
    1.16 +
    1.17 +  def get_file_content(file: JFile): Option[String] =
    1.18 +    get_model(file) match {
    1.19 +      case Some(model) => Some(model.content.text)
    1.20 +      case None => read_file_content(file)
    1.21 +    }
    1.22 +
    1.23 +  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    1.24 +    for {
    1.25 +      (_, model) <- state.value.models.iterator
    1.26 +      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
    1.27 +    } yield Text.Info(range, (entry, model))
    1.28 +
    1.29    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.30    {
    1.31      val file = node_file(name)
    1.32 @@ -83,15 +105,6 @@
    1.33  
    1.34    /* document models */
    1.35  
    1.36 -  def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file)
    1.37 -  def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name))
    1.38 -
    1.39 -  def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
    1.40 -    for {
    1.41 -      (_, model) <- state.value.models.iterator
    1.42 -      Text.Info(range, entry) <- model.content.bibtex_entries.iterator
    1.43 -    } yield Text.Info(range, (entry, model))
    1.44 -
    1.45    def visible_node(name: Document.Node.Name): Boolean =
    1.46      get_model(name) match {
    1.47        case Some(model) => model.node_visible
    1.48 @@ -136,19 +149,6 @@
    1.49        })
    1.50  
    1.51  
    1.52 -  /* file content */
    1.53 -
    1.54 -  def read_file_content(file: JFile): Option[String] =
    1.55 -    try { Some(Line.normalize(File.read(file))) }
    1.56 -    catch { case ERROR(_) => None }
    1.57 -
    1.58 -  def get_file_content(file: JFile): Option[String] =
    1.59 -    get_model(file) match {
    1.60 -      case Some(model) => Some(model.content.text)
    1.61 -      case None => read_file_content(file)
    1.62 -    }
    1.63 -
    1.64 -
    1.65    /* resolve dependencies */
    1.66  
    1.67    val thy_info = new Thy_Info(this)
     2.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 13:08:17 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 14:46:04 2017 +0100
     2.3 @@ -33,7 +33,7 @@
     2.4      base_syntax: Outer_Syntax)
     2.5    extends Resources(loaded_theories, known_theories, base_syntax)
     2.6  {
     2.7 -  /* document node names */
     2.8 +  /* document node name */
     2.9  
    2.10    def node_name(buffer: Buffer): Document.Node.Name =
    2.11    {
    2.12 @@ -49,9 +49,6 @@
    2.13      if (name.is_theory) Some(name) else None
    2.14    }
    2.15  
    2.16 -
    2.17 -  /* file-system operations */
    2.18 -
    2.19    override def append(dir: String, source_path: Path): String =
    2.20    {
    2.21      val path = source_path.expand
    2.22 @@ -67,6 +64,9 @@
    2.23      }
    2.24    }
    2.25  
    2.26 +
    2.27 +  /* file content */
    2.28 +
    2.29    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    2.30    {
    2.31      GUI_Thread.now {
    2.32 @@ -86,8 +86,6 @@
    2.33    }
    2.34  
    2.35  
    2.36 -  /* file content */
    2.37 -
    2.38    private class File_Content_Output(buffer: Buffer) extends
    2.39      ByteArrayOutputStream(buffer.getLength + 1)
    2.40    {