src/Tools/jEdit/src/jedit_resources.scala
changeset 64834 0a7179ad430d
parent 64813 7283f41d05ab
child 64835 fd1efd6dd385
     1.1 --- a/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 13:08:17 2017 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit_resources.scala	Sun Jan 08 14:46:04 2017 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4      base_syntax: Outer_Syntax)
     1.5    extends Resources(loaded_theories, known_theories, base_syntax)
     1.6  {
     1.7 -  /* document node names */
     1.8 +  /* document node name */
     1.9  
    1.10    def node_name(buffer: Buffer): Document.Node.Name =
    1.11    {
    1.12 @@ -49,9 +49,6 @@
    1.13      if (name.is_theory) Some(name) else None
    1.14    }
    1.15  
    1.16 -
    1.17 -  /* file-system operations */
    1.18 -
    1.19    override def append(dir: String, source_path: Path): String =
    1.20    {
    1.21      val path = source_path.expand
    1.22 @@ -67,6 +64,9 @@
    1.23      }
    1.24    }
    1.25  
    1.26 +
    1.27 +  /* file content */
    1.28 +
    1.29    override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
    1.30    {
    1.31      GUI_Thread.now {
    1.32 @@ -86,8 +86,6 @@
    1.33    }
    1.34  
    1.35  
    1.36 -  /* file content */
    1.37 -
    1.38    private class File_Content_Output(buffer: Buffer) extends
    1.39      ByteArrayOutputStream(buffer.getLength + 1)
    1.40    {