25 |
25 |
26 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
26 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
27 Token_Markup.line_token_iterator(syntax, buffer, line, line + lim). |
27 Token_Markup.line_token_iterator(syntax, buffer, line, line + lim). |
28 filter(_.info.is_proper) |
28 filter(_.info.is_proper) |
29 |
29 |
30 def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
30 def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
31 Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim). |
31 Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim). |
32 filter(_.info.is_proper) |
32 filter(_.info.is_proper) |
33 } |
33 } |
34 |
34 |
35 |
35 |
90 val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer]) |
90 val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer]) |
91 |
91 |
92 def caret_iterator(): Iterator[Text.Info[Token]] = |
92 def caret_iterator(): Iterator[Text.Info[Token]] = |
93 nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
93 nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
94 |
94 |
95 def rev_caret_iterator(): Iterator[Text.Info[Token]] = |
95 def reverse_caret_iterator(): Iterator[Text.Info[Token]] = |
96 nav.rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
96 nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
97 |
97 |
98 nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) |
98 nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) |
99 match { |
99 match { |
100 case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => |
100 case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => |
101 find_block( |
101 find_block( |
116 keywords.is_command(t, Keyword.diag) || |
116 keywords.is_command(t, Keyword.diag) || |
117 keywords.is_command(t, Keyword.proof), |
117 keywords.is_command(t, Keyword.proof), |
118 caret_iterator()) |
118 caret_iterator()) |
119 |
119 |
120 case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => |
120 case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => |
121 rev_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) |
121 reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) |
122 match { |
122 match { |
123 case Some(Text.Info(range2, tok)) |
123 case Some(Text.Info(range2, tok)) |
124 if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) |
124 if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) |
125 case _ => None |
125 case _ => None |
126 } |
126 } |
134 _ => false, |
134 _ => false, |
135 t => |
135 t => |
136 keywords.is_command(t, Keyword.diag) || |
136 keywords.is_command(t, Keyword.diag) || |
137 keywords.is_command(t, Keyword.proof) || |
137 keywords.is_command(t, Keyword.proof) || |
138 keywords.is_command(t, Keyword.theory_goal), |
138 keywords.is_command(t, Keyword.theory_goal), |
139 rev_caret_iterator()) |
139 reverse_caret_iterator()) |
140 |
140 |
141 case Some(Text.Info(range1, tok)) if tok.is_begin => |
141 case Some(Text.Info(range1, tok)) if tok.is_begin => |
142 find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) |
142 find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) |
143 |
143 |
144 case Some(Text.Info(range1, tok)) if tok.is_end => |
144 case Some(Text.Info(range1, tok)) if tok.is_end => |
145 find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator()) |
145 find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) |
146 match { |
146 match { |
147 case Some((_, range2)) => |
147 case Some((_, range2)) => |
148 rev_caret_iterator(). |
148 reverse_caret_iterator(). |
149 dropWhile(info => info.range != range2). |
149 dropWhile(info => info.range != range2). |
150 dropWhile(info => info.range == range2). |
150 dropWhile(info => info.range == range2). |
151 find(info => info.info.is_command || info.info.is_begin) |
151 find(info => info.info.is_command || info.info.is_begin) |
152 match { |
152 match { |
153 case Some(Text.Info(range3, tok)) => |
153 case Some(Text.Info(range3, tok)) => |