--- a/src/Tools/jEdit/src/document_model.scala Fri Sep 18 16:42:19 2015 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sat Sep 19 19:34:51 2015 +0200
@@ -16,7 +16,7 @@
import org.gjt.sp.jedit.jEdit
import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer, LineManager}
+import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
object Document_Model
@@ -302,7 +302,7 @@
def syntax_changed()
{
- Untyped.get[LineManager](buffer, "lineMgr").setFirstInvalidLineContext(0)
+ JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
invoke(text_area)
--- a/src/Tools/jEdit/src/jedit_lib.scala Fri Sep 18 16:42:19 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Sat Sep 19 19:34:51 2015 +0200
@@ -18,7 +18,7 @@
import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
import org.gjt.sp.jedit.gui.KeyEventWorkaround
-import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
import org.gjt.sp.jedit.syntax.TokenMarker
@@ -114,6 +114,9 @@
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+ def buffer_line_manager(buffer: JEditBuffer): LineManager =
+ Untyped.get[LineManager](buffer, "lineMgr")
+
/* main jEdit components */
--- a/src/Tools/jEdit/src/token_markup.scala Fri Sep 18 16:42:19 2015 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Sat Sep 19 19:34:51 2015 +0200
@@ -18,7 +18,7 @@
import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
import org.gjt.sp.jedit.textarea.{TextArea, Selection}
-import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
+import org.gjt.sp.jedit.buffer.JEditBuffer
import javax.swing.text.Segment
@@ -194,7 +194,7 @@
def buffer_line_context(buffer: JEditBuffer, line: Int): Line_Context =
{
- val line_mgr = Untyped.get[LineManager](buffer, "lineMgr")
+ val line_mgr = JEdit_Lib.buffer_line_manager(buffer)
def context =
line_mgr.getLineContext(line) match {
case c: Line_Context => Some(c)