# HG changeset patch
# User wenzelm
# Date 1442684091 -7200
# Node ID 98eba31c51f880d9f68e04e05521215b8cf6c7d7
# Parent  5977962f8e66d0659d86854d7f8764b77587d7f9
tuned signature;

diff -r 5977962f8e66 -r 98eba31c51f8 src/Tools/jEdit/src/document_model.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)
diff -r 5977962f8e66 -r 98eba31c51f8 src/Tools/jEdit/src/jedit_lib.scala
--- 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 */
 
diff -r 5977962f8e66 -r 98eba31c51f8 src/Tools/jEdit/src/token_markup.scala
--- 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)