# HG changeset patch
# User wenzelm
# Date 1413919245 -7200
# Node ID eb5d0c58564dc3827b106e6176e16c35c44eaf6e
# Parent  fc822ca2428a749659029a444e4a15a2e25e95a7
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);

diff -r fc822ca2428a -r eb5d0c58564d src/Tools/jEdit/src/structure_matching.scala
--- a/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 21:02:36 2014 +0200
+++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Oct 21 21:20:45 2014 +0200
@@ -45,10 +45,12 @@
           val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
           def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
-            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
+            Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
+              filter(_.info.is_proper)
 
           def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
-            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
+            Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
+              filter(_.info.is_proper)
 
           def caret_iterator(): Iterator[Text.Info[Token]] =
             iterator(caret_line).dropWhile(info => !info.range.touches(caret))
@@ -56,8 +58,8 @@
           def rev_caret_iterator(): Iterator[Text.Info[Token]] =
             rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
 
-          iterator(caret_line, 1).find(info => info.range.touches(caret)) match
-          {
+          iterator(caret_line, 1).find(info => info.range.touches(caret))
+          match {
             case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) =>
               find_block(
                 syntax.command_kind(_, Keyword.proof_goal),