--- a/src/Tools/jEdit/src/completion_popup.scala Mon Dec 01 15:21:49 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Mon Dec 01 17:43:23 2014 +0100
@@ -157,7 +157,7 @@
val buffer = text_area.getBuffer
val decode = Isabelle_Encoding.is_active(buffer)
- Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
+ Isabelle.buffer_syntax(buffer) match {
case Some(syntax) =>
val context =
(for {
--- a/src/Tools/jEdit/src/isabelle.scala Mon Dec 01 15:21:49 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Mon Dec 01 17:43:23 2014 +0100
@@ -15,6 +15,7 @@
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.{jEdit, View, Buffer}
+import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.textarea.{JEditTextArea, StructureMatcher}
import org.gjt.sp.jedit.syntax.TokenMarker
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
@@ -65,6 +66,9 @@
case _ => None
}
+ def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
+ mode_syntax(JEdit_Lib.buffer_mode(buffer))
+
/* token markers */
--- a/src/Tools/jEdit/src/structure_matching.scala Mon Dec 01 15:21:49 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala Mon Dec 01 17:43:23 2014 +0100
@@ -40,7 +40,7 @@
val caret_line = text_area.getCaretLine
val caret = text_area.getCaretPosition
- Isabelle.session_syntax() match {
+ Isabelle.buffer_syntax(text_area.getBuffer) match {
case Some(syntax) =>
val limit = PIDE.options.value.int("jedit_structure_limit") max 0
@@ -143,7 +143,7 @@
{
def get_span(offset: Text.Offset): Option[Text.Range] =
for {
- syntax <- Isabelle.session_syntax()
+ syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
} yield span.range