# HG changeset patch
# User wenzelm
# Date 1417452203 -3600
# Node ID 7836d927ffca8fe5ec93efb7d902b6a2f3b02ed4
# Parent  dcecfcc56dced1faa75e09935ca039132f0f0700
tuned signature;

diff -r dcecfcc56dce -r 7836d927ffca src/Tools/jEdit/src/completion_popup.scala
--- 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 {
diff -r dcecfcc56dce -r 7836d927ffca src/Tools/jEdit/src/isabelle.scala
--- 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 */
 
diff -r dcecfcc56dce -r 7836d927ffca src/Tools/jEdit/src/structure_matching.scala
--- 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