merged
authorAndreas Lochbihler
Wed, 22 Oct 2014 17:34:19 +0200
changeset 58765 c0e46e1beefc
parent 58763 1b943a82d5ed (diff)
parent 58764 ca2f59aef665 (current diff)
child 58768 06dfbfa4b3ea
merged
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Oct 22 13:58:30 2014 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Oct 22 17:34:19 2014 +0200
@@ -331,11 +331,10 @@
 
   @{rail \<open>
     @{syntax_def mixfix}: '('
-      @{syntax template} prios? @{syntax nat}? |
-      (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
-      @'binder' @{syntax template} prios? @{syntax nat} |
-      @'structure'
-    ')'
+      (@{syntax template} prios? @{syntax nat}? |
+        (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
+        @'binder' @{syntax template} prios? @{syntax nat} |
+        @'structure') ')'
     ;
     template: string
     ;
--- a/src/Tools/jEdit/src/structure_matching.scala	Wed Oct 22 13:58:30 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala	Wed Oct 22 17:34:19 2014 +0200
@@ -20,16 +20,18 @@
       open: Token => Boolean,
       close: Token => Boolean,
       reset: Token => Boolean,
+      restrict: Token => Boolean,
       it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
     {
       val range1 = it.next.range
-      it.scanLeft((range1, 1))(
-        { case ((r, d), Text.Info(range, tok)) =>
-            if (open(tok)) (range, d + 1)
-            else if (close(tok)) (range, d - 1)
-            else if (reset(tok)) (range, 0)
-            else (r, d) }
-      ).collectFirst({ case (range2, 0) => (range1, range2) })
+      it.takeWhile(info => !info.info.is_command || restrict(info.info)).
+        scanLeft((range1, 1))(
+          { case ((r, d), Text.Info(range, tok)) =>
+              if (open(tok)) (range, d + 1)
+              else if (close(tok)) (range, d - 1)
+              else if (reset(tok)) (range, 0)
+              else (r, d) }
+        ).collectFirst({ case (range2, 0) => (range1, range2) })
     }
 
     def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
@@ -65,6 +67,9 @@
                 syntax.command_kind(_, Keyword.proof_goal),
                 syntax.command_kind(_, Keyword.qed),
                 syntax.command_kind(_, Keyword.qed_global),
+                t =>
+                  syntax.command_kind(t, Keyword.diag) ||
+                  syntax.command_kind(t, Keyword.proof),
                 caret_iterator())
 
             case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) =>
@@ -72,6 +77,9 @@
                 syntax.command_kind(_, Keyword.proof_goal),
                 syntax.command_kind(_, Keyword.qed),
                 _ => false,
+                t =>
+                  syntax.command_kind(t, Keyword.diag) ||
+                  syntax.command_kind(t, Keyword.proof),
                 caret_iterator())
 
             case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) =>
@@ -89,13 +97,29 @@
                   syntax.command_kind(t, Keyword.proof_goal) ||
                   syntax.command_kind(t, Keyword.theory_goal),
                 _ => false,
+                t =>
+                  syntax.command_kind(t, Keyword.diag) ||
+                  syntax.command_kind(t, Keyword.proof) ||
+                  syntax.command_kind(t, Keyword.theory_goal),
                 rev_caret_iterator())
 
             case Some(Text.Info(range1, tok)) if tok.is_begin =>
-              find_block(_.is_begin, _.is_end, _ => false, caret_iterator())
+              find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
 
             case Some(Text.Info(range1, tok)) if tok.is_end =>
-              find_block(_.is_end, _.is_begin, _ => false, rev_caret_iterator())
+              find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
+              match {
+                case Some((_, range2)) =>
+                  rev_caret_iterator().dropWhile(info => info.range != range2).
+                    find(info =>
+                      // FIXME more precise keyword category
+                      syntax.command_kind(info.info, Set(Keyword.THY_BEGIN, Keyword.THY_DECL)))
+                  match {
+                    case Some(Text.Info(range3, _)) => Some((range1, range3))
+                    case None => None
+                  }
+                case None => None
+              }
 
             case _ => None
           }