--- 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 */