# HG changeset patch
# User wenzelm
# Date 1413308369 -7200
# Node ID c9b7a00d5a103907e5d536a47fa0ad8b669603f4
# Parent  542fa5093ebf17722cbbf809301bc20f2b910ade
buffer_line_context via untyped access;

diff -r 542fa5093ebf -r c9b7a00d5a10 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Oct 14 19:38:41 2014 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Oct 14 19:39:29 2014 +0200
@@ -18,7 +18,7 @@
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet,
   ModeProvider, XModeHandler, SyntaxStyle}
 import org.gjt.sp.jedit.textarea.{TextArea, Selection}
-import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
 
 import javax.swing.text.Segment
 
@@ -186,6 +186,17 @@
       }
   }
 
+  def buffer_line_context[C](buffer: JEditBuffer, line: Int): Option[Generic_Line_Context[C]] =
+    Untyped.get(buffer, "lineMgr") match {
+      case line_mgr: LineManager =>
+        line_mgr.getLineContext(line) match {
+          case ctxt: Generic_Line_Context[C] => Some(ctxt)
+          case _ => None
+        }
+      case _ => None
+    }
+
+
   private val context_rules = new ParserRuleSet("isabelle", "MAIN")
 
   private class Line_Context(context: Option[Scan.Line_Context])