43 if syntax != Outer_Syntax.empty => |
43 if syntax != Outer_Syntax.empty => |
44 |
44 |
45 val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
45 val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
46 |
46 |
47 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
47 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
48 Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) |
48 Token_Markup.line_token_iterator(syntax, buffer, line, line + lim). |
|
49 filter(_.info.is_proper) |
49 |
50 |
50 def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
51 def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
51 Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) |
52 Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim). |
|
53 filter(_.info.is_proper) |
52 |
54 |
53 def caret_iterator(): Iterator[Text.Info[Token]] = |
55 def caret_iterator(): Iterator[Text.Info[Token]] = |
54 iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
56 iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
55 |
57 |
56 def rev_caret_iterator(): Iterator[Text.Info[Token]] = |
58 def rev_caret_iterator(): Iterator[Text.Info[Token]] = |
57 rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
59 rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
58 |
60 |
59 iterator(caret_line, 1).find(info => info.range.touches(caret)) match |
61 iterator(caret_line, 1).find(info => info.range.touches(caret)) |
60 { |
62 match { |
61 case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) => |
63 case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) => |
62 find_block( |
64 find_block( |
63 syntax.command_kind(_, Keyword.proof_goal), |
65 syntax.command_kind(_, Keyword.proof_goal), |
64 syntax.command_kind(_, Keyword.qed), |
66 syntax.command_kind(_, Keyword.qed), |
65 syntax.command_kind(_, Keyword.qed_global), |
67 syntax.command_kind(_, Keyword.qed_global), |