buffer_line_context via untyped access;
authorwenzelm
Tue Oct 14 19:39:29 2014 +0200 (2014-10-14)
changeset 58683c9b7a00d5a10
parent 58682 542fa5093ebf
child 58684 56b9eab818ca
buffer_line_context via untyped access;
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/token_markup.scala	Tue Oct 14 19:38:41 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Tue Oct 14 19:39:29 2014 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet,
     1.5    ModeProvider, XModeHandler, SyntaxStyle}
     1.6  import org.gjt.sp.jedit.textarea.{TextArea, Selection}
     1.7 -import org.gjt.sp.jedit.buffer.JEditBuffer
     1.8 +import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
     1.9  
    1.10  import javax.swing.text.Segment
    1.11  
    1.12 @@ -186,6 +186,17 @@
    1.13        }
    1.14    }
    1.15  
    1.16 +  def buffer_line_context[C](buffer: JEditBuffer, line: Int): Option[Generic_Line_Context[C]] =
    1.17 +    Untyped.get(buffer, "lineMgr") match {
    1.18 +      case line_mgr: LineManager =>
    1.19 +        line_mgr.getLineContext(line) match {
    1.20 +          case ctxt: Generic_Line_Context[C] => Some(ctxt)
    1.21 +          case _ => None
    1.22 +        }
    1.23 +      case _ => None
    1.24 +    }
    1.25 +
    1.26 +
    1.27    private val context_rules = new ParserRuleSet("isabelle", "MAIN")
    1.28  
    1.29    private class Line_Context(context: Option[Scan.Line_Context])