tuned signature;

--- a/src/Tools/jEdit/src/isabelle.scala	Tue Oct 28 16:20:26 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Oct 28 16:27:11 2014 +0100
@@ -47,13 +47,15 @@
   private lazy val news_syntax: Outer_Syntax =
     Outer_Syntax.init().no_tokens
 
+  def session_syntax(): Option[Outer_Syntax] =
+    PIDE.session.recent_syntax match {
+      case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
+      case _ => None
+    }
+
   def mode_syntax(name: String): Option[Outer_Syntax] =
     name match {
-      case "isabelle" | "isabelle-markup" =>
-        PIDE.session.recent_syntax match {
-          case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
-          case _ => None
-        }
+      case "isabelle" | "isabelle-markup" => session_syntax()
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Build.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)

--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 16:20:26 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 16:27:11 2014 +0100
@@ -16,12 +16,6 @@
 {
   object Isabelle_Matcher extends StructureMatcher
   {
-    private def get_syntax(): Option[Outer_Syntax] =
-      PIDE.session.recent_syntax match {
-        case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
-        case _ => None
-      }
-
     private def find_block(
       open: Token => Boolean,
       close: Token => Boolean,
@@ -46,7 +40,7 @@
       val caret_line = text_area.getCaretLine
       val caret = text_area.getCaretPosition
 
-      get_syntax() match {
+      Isabelle.session_syntax() match {
         case Some(syntax) =>
           val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
@@ -146,7 +140,7 @@
     {
       def get_span(offset: Text.Offset): Option[Text.Range] =
         for {
-          syntax <- get_syntax()
+          syntax <- Isabelle.session_syntax()
           span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
         } yield span.range