--- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Jun 17 20:24:22 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Jun 19 17:28:48 2017 +0200
@@ -21,8 +21,8 @@
object JEdit_Rendering
{
- def apply(snapshot: Document.Snapshot, options: Options): JEdit_Rendering =
- new JEdit_Rendering(snapshot, options)
+ def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
+ new JEdit_Rendering(snapshot, model, options)
/* popup window bounds */
@@ -148,9 +148,12 @@
}
-class JEdit_Rendering(snapshot: Document.Snapshot, options: Options)
+class JEdit_Rendering(snapshot: Document.Snapshot, _model: Document_Model, options: Options)
extends Rendering(snapshot, options, PIDE.session)
{
+ def model: Document_Model = _model
+
+
/* colors */
def color(s: String): Color =