tuned signature;
authorwenzelm
Sat, 19 Sep 2015 19:34:51 +0200
changeset 61192 98eba31c51f8
parent 61191 5977962f8e66
child 61193 dde5ecbd5e10
tuned signature;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/token_markup.scala
--- 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)