src/Tools/jEdit/src/jedit_resources.scala

--- a/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 26 16:57:07 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Mon Dec 26 17:36:56 2022 +0100
@@ -116,7 +116,7 @@
     def content(): Bytes = Bytes(this.buf, 0, this.count)
   }
 
-  private class File_Content(buffer: Buffer)
+  private class File_Content_Request(buffer: Buffer)
   extends BufferIORequest(null, buffer, null, VFSManager.getVFSForPath(buffer.getPath), buffer.getPath) {
     def _run(): Unit = {}
     def content(): Bytes = {
@@ -126,7 +126,7 @@
     }
   }
 
-  def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content()
+  def make_file_content(buffer: Buffer): Bytes = (new File_Content_Request(buffer)).content()
 
 
   /* theory text edits */