author | wenzelm |
Mon, 11 Jul 2016 20:37:28 +0200 | |
changeset 63450 | afd657fffdf9 |
parent 63447 | 55b1bed86c44 |
child 63474 | f66e3c3b0fb1 |
permissions | -rw-r--r-- |
63422 | 1 |
/* Title: Tools/jEdit/src/text_structure.scala |
58748 | 2 |
Author: Makarius |
3 |
||
63422 | 4 |
Text structure based on Isabelle/Isar outer syntax. |
58748 | 5 |
*/ |
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
63422 | 12 |
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} |
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
13 |
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} |
63422 | 14 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
63423 | 15 |
import org.gjt.sp.jedit.Buffer |
58748 | 16 |
|
17 |
||
63422 | 18 |
object Text_Structure |
58748 | 19 |
{ |
63425 | 20 |
/* token navigator */ |
21 |
||
63447 | 22 |
class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean) |
63425 | 23 |
{ |
24 |
val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
|
25 |
||
26 |
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
|
63445
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
27 |
{ |
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
28 |
val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) |
63447 | 29 |
if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) |
63445
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
30 |
} |
63425 | 31 |
|
63427 | 32 |
def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
63445
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
33 |
{ |
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
34 |
val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) |
63447 | 35 |
if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) |
63445
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
36 |
} |
63425 | 37 |
} |
38 |
||
39 |
||
63422 | 40 |
/* indentation */ |
41 |
||
42 |
object Indent_Rule extends IndentRule |
|
43 |
{ |
|
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
44 |
private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
45 |
private val keyword_close = Keyword.proof_close |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
46 |
|
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
47 |
def apply(buffer: JEditBuffer, current_line: Int, prev_line: Int, prev_prev_line: Int, |
63422 | 48 |
actions: java.util.List[IndentAction]) |
49 |
{ |
|
63425 | 50 |
Isabelle.buffer_syntax(buffer) match { |
51 |
case Some(syntax) if buffer.isInstanceOf[Buffer] => |
|
52 |
val keywords = syntax.keywords |
|
63445
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
53 |
val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true) |
63422 | 54 |
|
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
55 |
def head_token(line: Int): Option[Token] = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
56 |
nav.iterator(line, 1).toStream.headOption.map(_.info) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
57 |
|
63434 | 58 |
def head_is_quasi_command(line: Int): Boolean = |
59 |
head_token(line) match { |
|
60 |
case None => false |
|
61 |
case Some(tok) => keywords.is_quasi_command(tok) |
|
62 |
} |
|
63 |
||
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
64 |
def prev_command: Option[Token] = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
65 |
nav.reverse_iterator(prev_line, 1). |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
66 |
collectFirst({ case Text.Info(_, tok) if tok.is_command => tok }) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
67 |
|
63434 | 68 |
def prev_span: Iterator[Token] = |
69 |
nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_command) |
|
70 |
||
63450 | 71 |
def prev_line_span: Iterator[Token] = |
72 |
nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command) |
|
73 |
||
63434 | 74 |
|
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
75 |
def line_indent(line: Int): Int = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
76 |
if (line < 0 || line >= buffer.getLineCount) 0 |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
77 |
else buffer.getCurrentIndentForLine(line, null) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
78 |
|
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
79 |
val indent_size = buffer.getIndentSize |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
80 |
|
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
81 |
def indent_indent(tok: Token): Int = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
82 |
if (keywords.is_command(tok, keyword_open)) indent_size |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
83 |
else if (keywords.is_command(tok, keyword_close)) - indent_size |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
84 |
else 0 |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
85 |
|
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
86 |
def indent_offset(tok: Token): Int = |
63446 | 87 |
if (keywords.is_command(tok, Keyword.proof_enclose) || tok.is_begin) indent_size |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
88 |
else 0 |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
89 |
|
63450 | 90 |
def indent_brackets: Int = |
91 |
(0 /: prev_line_span)( |
|
92 |
{ case (i, tok) => |
|
93 |
if (tok.is_open_bracket) i + indent_size |
|
94 |
else if (tok.is_close_bracket) i - indent_size |
|
95 |
else i }) |
|
96 |
||
63434 | 97 |
def indent_extra: Int = |
98 |
if (prev_span.exists(keywords.is_quasi_command(_))) indent_size |
|
99 |
else 0 |
|
100 |
||
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
101 |
def indent_structure: Int = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
102 |
nav.reverse_iterator(current_line - 1).scanLeft((0, false))( |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
103 |
{ case ((ind, _), Text.Info(range, tok)) => |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
104 |
val ind1 = ind + indent_indent(tok) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
105 |
if (tok.is_command) { |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
106 |
val line = buffer.getLineOfOffset(range.start) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
107 |
if (head_token(line) == Some(tok)) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
108 |
(ind1 + indent_offset(tok) + line_indent(line), true) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
109 |
else (ind1, false) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
110 |
} |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
111 |
else (ind1, false) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
112 |
}).collectFirst({ case (i, true) => i }).getOrElse(0) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
113 |
|
63440 | 114 |
def nesting(it: Iterator[Token], open: Token => Boolean, close: Token => Boolean): Int = |
115 |
(0 /: it)({ case (d, tok) => if (open(tok)) d + 1 else if (close(tok)) d - 1 else d }) |
|
116 |
||
117 |
def indent_begin: Int = |
|
118 |
(nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) * |
|
119 |
indent_size |
|
120 |
||
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
121 |
val indent = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
122 |
head_token(current_line) match { |
63450 | 123 |
case None => indent_structure + indent_brackets + indent_extra |
63431 | 124 |
case Some(tok) => |
63442 | 125 |
if (keywords.is_before_command(tok) || |
126 |
keywords.is_command(tok, Keyword.theory)) indent_begin |
|
63440 | 127 |
else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok) |
63434 | 128 |
else { |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
129 |
prev_command match { |
63434 | 130 |
case None => |
131 |
val extra = |
|
132 |
(keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |
|
133 |
case (true, true) | (false, false) => 0 |
|
134 |
case (true, false) => - indent_extra |
|
135 |
case (false, true) => indent_extra |
|
136 |
} |
|
63450 | 137 |
line_indent(prev_line) - indent_offset(tok) + indent_brackets + extra |
63431 | 138 |
case Some(prev_tok) => |
63450 | 139 |
indent_structure - indent_offset(tok) - indent_offset(prev_tok) + |
140 |
indent_brackets - indent_indent(prev_tok) + indent_size |
|
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
141 |
} |
63434 | 142 |
} |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
143 |
} |
63423 | 144 |
|
63425 | 145 |
actions.clear() |
63439 | 146 |
actions.add(new IndentAction.AlignOffset(indent max 0)) |
63423 | 147 |
case _ => |
148 |
} |
|
63422 | 149 |
} |
150 |
} |
|
151 |
||
152 |
||
153 |
/* structure matching */ |
|
154 |
||
155 |
object Matcher extends StructureMatcher |
|
58748 | 156 |
{ |
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
157 |
private def find_block( |
58752 | 158 |
open: Token => Boolean, |
159 |
close: Token => Boolean, |
|
160 |
reset: Token => Boolean, |
|
58762 | 161 |
restrict: Token => Boolean, |
58754 | 162 |
it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] = |
58752 | 163 |
{ |
58754 | 164 |
val range1 = it.next.range |
58762 | 165 |
it.takeWhile(info => !info.info.is_command || restrict(info.info)). |
166 |
scanLeft((range1, 1))( |
|
167 |
{ case ((r, d), Text.Info(range, tok)) => |
|
168 |
if (open(tok)) (range, d + 1) |
|
169 |
else if (close(tok)) (range, d - 1) |
|
170 |
else if (reset(tok)) (range, 0) |
|
171 |
else (r, d) } |
|
172 |
).collectFirst({ case (range2, 0) => (range1, range2) }) |
|
58752 | 173 |
} |
174 |
||
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
175 |
private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = |
58748 | 176 |
{ |
177 |
val buffer = text_area.getBuffer |
|
178 |
val caret_line = text_area.getCaretLine |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
179 |
val caret = text_area.getCaretPosition |
58748 | 180 |
|
59074 | 181 |
Isabelle.buffer_syntax(text_area.getBuffer) match { |
63425 | 182 |
case Some(syntax) if buffer.isInstanceOf[Buffer] => |
63424 | 183 |
val keywords = syntax.keywords |
58750 | 184 |
|
63445
5761bb8592dc
observe comments in indentation, but not in fold structure;
wenzelm
parents:
63442
diff
changeset
|
185 |
val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false) |
58750 | 186 |
|
58752 | 187 |
def caret_iterator(): Iterator[Text.Info[Token]] = |
63425 | 188 |
nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
58752 | 189 |
|
63427 | 190 |
def reverse_caret_iterator(): Iterator[Text.Info[Token]] = |
191 |
nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
|
58752 | 192 |
|
63425 | 193 |
nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) |
58756
eb5d0c58564d
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents:
58755
diff
changeset
|
194 |
match { |
63424 | 195 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => |
58755 | 196 |
find_block( |
63424 | 197 |
keywords.is_command(_, Keyword.proof_goal), |
198 |
keywords.is_command(_, Keyword.qed), |
|
199 |
keywords.is_command(_, Keyword.qed_global), |
|
58762 | 200 |
t => |
63424 | 201 |
keywords.is_command(t, Keyword.diag) || |
202 |
keywords.is_command(t, Keyword.proof), |
|
58755 | 203 |
caret_iterator()) |
204 |
||
63424 | 205 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) => |
58755 | 206 |
find_block( |
63424 | 207 |
keywords.is_command(_, Keyword.proof_goal), |
208 |
keywords.is_command(_, Keyword.qed), |
|
58755 | 209 |
_ => false, |
58762 | 210 |
t => |
63424 | 211 |
keywords.is_command(t, Keyword.diag) || |
212 |
keywords.is_command(t, Keyword.proof), |
|
58755 | 213 |
caret_iterator()) |
214 |
||
63424 | 215 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => |
63427 | 216 |
reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) |
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
217 |
match { |
58750 | 218 |
case Some(Text.Info(range2, tok)) |
63424 | 219 |
if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) |
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
220 |
case _ => None |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
221 |
} |
58752 | 222 |
|
63424 | 223 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) => |
58755 | 224 |
find_block( |
63424 | 225 |
keywords.is_command(_, Keyword.qed), |
58755 | 226 |
t => |
63424 | 227 |
keywords.is_command(t, Keyword.proof_goal) || |
228 |
keywords.is_command(t, Keyword.theory_goal), |
|
58755 | 229 |
_ => false, |
58762 | 230 |
t => |
63424 | 231 |
keywords.is_command(t, Keyword.diag) || |
232 |
keywords.is_command(t, Keyword.proof) || |
|
233 |
keywords.is_command(t, Keyword.theory_goal), |
|
63427 | 234 |
reverse_caret_iterator()) |
58755 | 235 |
|
58752 | 236 |
case Some(Text.Info(range1, tok)) if tok.is_begin => |
58762 | 237 |
find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) |
58752 | 238 |
|
239 |
case Some(Text.Info(range1, tok)) if tok.is_end => |
|
63427 | 240 |
find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) |
58763 | 241 |
match { |
242 |
case Some((_, range2)) => |
|
63427 | 243 |
reverse_caret_iterator(). |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
244 |
dropWhile(info => info.range != range2). |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
245 |
dropWhile(info => info.range == range2). |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
246 |
find(info => info.info.is_command || info.info.is_begin) |
58763 | 247 |
match { |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
248 |
case Some(Text.Info(range3, tok)) => |
63424 | 249 |
if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3)) |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
250 |
else Some((range1, range2)) |
58763 | 251 |
case None => None |
252 |
} |
|
253 |
case None => None |
|
254 |
} |
|
58752 | 255 |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
256 |
case _ => None |
58748 | 257 |
} |
63425 | 258 |
case _ => None |
58748 | 259 |
} |
260 |
} |
|
261 |
||
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
262 |
def getMatch(text_area: TextArea): StructureMatcher.Match = |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
263 |
find_pair(text_area) match { |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
264 |
case Some((_, range)) => |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
265 |
val line = text_area.getBuffer.getLineOfOffset(range.start) |
63422 | 266 |
new StructureMatcher.Match(Matcher, line, range.start, line, range.stop) |
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
267 |
case None => null |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
268 |
} |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
269 |
|
58748 | 270 |
def selectMatch(text_area: TextArea) |
271 |
{ |
|
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
272 |
def get_span(offset: Text.Offset): Option[Text.Range] = |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
273 |
for { |
59074 | 274 |
syntax <- Isabelle.buffer_syntax(text_area.getBuffer) |
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
275 |
span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset) |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
276 |
} yield span.range |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
277 |
|
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
278 |
find_pair(text_area) match { |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
279 |
case Some((r1, r2)) => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
280 |
(get_span(r1.start), get_span(r2.start)) match { |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
281 |
case (Some(range1), Some(range2)) => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
282 |
val start = range1.start min range2.start |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
283 |
val stop = range1.stop max range2.stop |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
284 |
|
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
285 |
text_area.moveCaretPosition(stop, false) |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
286 |
if (!text_area.isMultipleSelectionEnabled) text_area.selectNone |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
287 |
text_area.addToSelection(new Selection.Range(start, stop)) |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
288 |
case _ => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
289 |
} |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
290 |
case None => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
291 |
} |
58748 | 292 |
} |
293 |
} |
|
294 |
} |