# HG changeset patch
# User wenzelm
# Date 1414509626 -3600
# Node ID 7a0f675eb67162bf596546e8325823a3653ab184
# Parent  3cc68ec558b0358bba99e874e527d3ae3fe80d8c
proper selectMatch, e.g. relevant for S-click on gutter;

diff -r 3cc68ec558b0 -r 7a0f675eb671 src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 16:19:04 2014 +0100
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 28 16:20:26 2014 +0100
@@ -9,14 +9,20 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher}
+import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
 
 
 object Structure_Matching
 {
   object Isabelle_Matcher extends StructureMatcher
   {
-    def find_block(
+    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,
       reset: Token => Boolean,
@@ -34,16 +40,14 @@
         ).collectFirst({ case (range2, 0) => (range1, range2) })
     }
 
-    def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
+    private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
     {
       val buffer = text_area.getBuffer
       val caret_line = text_area.getCaretLine
       val caret = text_area.getCaretPosition
 
-      PIDE.session.recent_syntax match {
-        case syntax: Outer_Syntax
-        if syntax != Outer_Syntax.empty =>
-
+      get_syntax() match {
+        case Some(syntax) =>
           val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
           def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
@@ -125,7 +129,7 @@
 
             case _ => None
           }
-        case _ => None
+        case None => None
       }
     }
 
@@ -140,7 +144,26 @@
 
     def selectMatch(text_area: TextArea)
     {
-      // FIXME
+      def get_span(offset: Text.Offset): Option[Text.Range] =
+        for {
+          syntax <- get_syntax()
+          span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
+        } yield span.range
+
+      find_pair(text_area) match {
+        case Some((r1, r2)) =>
+          (get_span(r1.start), get_span(r2.start)) match {
+            case (Some(range1), Some(range2)) =>
+              val start = range1.start min range2.start
+              val stop = range1.stop max range2.stop
+
+              text_area.moveCaretPosition(stop, false)
+              if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
+              text_area.addToSelection(new Selection.Range(start, stop))
+            case _ =>
+          }
+        case None =>
+      }
     }
   }
 }