--- a/src/Tools/jEdit/src/jedit_rendering.scala Wed Dec 09 14:29:30 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Wed Dec 09 15:14:24 2020 +0100
@@ -161,10 +161,10 @@
}
-class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
+class JEdit_Rendering(snapshot: Document.Snapshot, model: Document_Model, options: Options)
extends Rendering(snapshot, options, PIDE.session)
{
- def model: Document_Model = _model
+ override def get_text(range: Text.Range): Option[String] = model.get_text(range)
/* colors */