src/Tools/jEdit/src/jedit_resources.scala

     loaded_theories: Set[String],
     known_theories: Map[String, Document.Node.Name],
     base_syntax: Outer_Syntax)
   extends Resources(loaded_theories, known_theories, base_syntax)
 {
-  /* document node names */
+  /* document node name */
 
   def node_name(buffer: Buffer): Document.Node.Name =
   {
     val node = JEdit_Lib.buffer_name(buffer)
     val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")

   {
     val name = node_name(buffer)
     if (name.is_theory) Some(name) else None
   }
 
-
-  /* file-system operations */
-
   override def append(dir: String, source_path: Path): String =
   {
     val path = source_path.expand
     if (dir == "" || path.is_absolute)
       MiscUtilities.resolveSymlinks(File.platform_path(path))

         MiscUtilities.resolveSymlinks(
           vfs.constructPath(dir, File.platform_path(path)))
       else vfs.constructPath(dir, File.standard_path(path))
     }
   }
+
+
+  /* file content */
 
   override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
     GUI_Thread.now {
       JEdit_Lib.jedit_buffer(name) match {

         else error("No such file: " + quote(file.toString))
       }
     }
   }
 
-
-  /* file content */
 
   private class File_Content_Output(buffer: Buffer) extends
     ByteArrayOutputStream(buffer.getLength + 1)
   {
     def content(): Bytes = Bytes(this.buf, 0, this.count)