21 val buffer = text_area.getBuffer |
21 val buffer = text_area.getBuffer |
22 val caret_line = text_area.getCaretLine |
22 val caret_line = text_area.getCaretLine |
23 val caret = text_area.getCaretPosition |
23 val caret = text_area.getCaretPosition |
24 |
24 |
25 PIDE.session.recent_syntax match { |
25 PIDE.session.recent_syntax match { |
26 case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => |
26 case syntax: Outer_Syntax |
27 Token_Markup.line_token_iterator(syntax, buffer, caret_line). |
27 if syntax != Outer_Syntax.empty => |
28 find({ case (tok, r) => r.touches(caret) }) |
28 |
29 match { |
29 val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
30 case Some((tok, range1)) if (syntax.command_kind(tok, Keyword.qed_global)) => |
30 |
31 Token_Markup.line_token_reverse_iterator(syntax, buffer, caret_line). |
31 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
32 dropWhile({ case (_, r) => caret <= r.stop }). |
32 Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) |
33 find({ case (tok, _) => syntax.command_kind(tok, Keyword.theory) }) |
33 |
|
34 def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
|
35 Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) |
|
36 |
|
37 iterator(caret_line, 1).find(info => info.range.touches(caret)) match { |
|
38 case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) => |
|
39 rev_iterator(caret_line).dropWhile(info => caret <= info.range.stop). |
|
40 find(info => syntax.command_kind(info.info, Keyword.theory)) |
34 match { |
41 match { |
35 case Some((tok, range2)) if syntax.command_kind(tok, Keyword.theory_goal) => |
42 case Some(Text.Info(range2, tok)) |
36 Some((range1, range2)) |
43 if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) |
37 case _ => None |
44 case _ => None |
38 } |
45 } |
39 case _ => None |
46 case _ => None |
40 } |
47 } |
41 case _ => None |
48 case _ => None |