author | wenzelm |
Fri, 12 Aug 2022 12:50:19 +0200 | |
changeset 75816 | 91f02f224b80 |
parent 75423 | d164bf04d05e |
child 76765 | c654103e9c9d |
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 |
||
73909 | 12 |
import java.util.{List => JList} |
13 |
||
63422 | 14 |
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
|
15 |
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} |
63422 | 16 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
63423 | 17 |
import org.gjt.sp.jedit.Buffer |
58748 | 18 |
|
19 |
||
75393 | 20 |
object Text_Structure { |
63425 | 21 |
/* token navigator */ |
22 |
||
75393 | 23 |
class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean) { |
71601 | 24 |
val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0 |
63425 | 25 |
|
75393 | 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 |
val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) |
68730 | 28 |
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
|
29 |
} |
63425 | 30 |
|
75393 | 31 |
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
|
32 |
val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) |
68730 | 33 |
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
|
34 |
} |
63425 | 35 |
} |
36 |
||
37 |
||
63422 | 38 |
/* indentation */ |
39 |
||
75393 | 40 |
object Indent_Rule extends IndentRule { |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
41 |
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
|
42 |
private val keyword_close = Keyword.proof_close |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
43 |
|
75393 | 44 |
def apply( |
45 |
buffer: JEditBuffer, |
|
46 |
current_line: Int, |
|
47 |
prev_line0: Int, |
|
48 |
prev_prev_line0: Int, |
|
49 |
actions: JList[IndentAction] |
|
50 |
): Unit = { |
|
63425 | 51 |
Isabelle.buffer_syntax(buffer) match { |
66183 | 52 |
case Some(syntax) => |
63425 | 53 |
val keywords = syntax.keywords |
66183 | 54 |
val nav = new Navigator(syntax, buffer, true) |
63422 | 55 |
|
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
56 |
val indent_size = buffer.getIndentSize |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
57 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
58 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
59 |
def line_indent(line: Int): Int = |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
60 |
if (line < 0 || line >= buffer.getLineCount) 0 |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
61 |
else buffer.getCurrentIndentForLine(line, null) |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
62 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
63 |
def line_head(line: Int): Option[Text.Info[Token]] = |
73345 | 64 |
nav.iterator(line, 1).nextOption() |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
65 |
|
63434 | 66 |
def head_is_quasi_command(line: Int): Boolean = |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
67 |
line_head(line) match { |
63434 | 68 |
case None => false |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
69 |
case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok) |
63434 | 70 |
} |
71 |
||
64518 | 72 |
val prev_line: Int = |
73 |
Range.inclusive(current_line - 1, 0, -1).find(line => |
|
66176 | 74 |
Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && |
66178 | 75 |
(!Token_Markup.Line_Context.after(buffer, line).structure.improper || |
76 |
Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1 |
|
64518 | 77 |
|
63477
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63474
diff
changeset
|
78 |
def prev_line_command: Option[Token] = |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
79 |
nav.reverse_iterator(prev_line, 1). |
63477
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63474
diff
changeset
|
80 |
collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok }) |
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63474
diff
changeset
|
81 |
|
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63474
diff
changeset
|
82 |
def prev_line_span: Iterator[Token] = |
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63474
diff
changeset
|
83 |
nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command) |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
84 |
|
63434 | 85 |
def prev_span: Iterator[Token] = |
63477
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63474
diff
changeset
|
86 |
nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command) |
63450 | 87 |
|
63434 | 88 |
|
75393 | 89 |
val script_indent: Text.Info[Token] => Int = { |
64621 | 90 |
val opt_rendering: Option[JEdit_Rendering] = |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
91 |
if (PIDE.options.value.bool("jedit_indent_script")) |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
92 |
GUI_Thread.now { |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
93 |
(for { |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
94 |
text_area <- JEdit_Lib.jedit_text_areas(buffer) |
64882 | 95 |
doc_view <- Document_View.get(text_area) |
73367 | 96 |
} yield doc_view.get_rendering()).nextOption() |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
97 |
} |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
98 |
else None |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
99 |
val limit = PIDE.options.value.int("jedit_indent_script_limit") |
63481 | 100 |
(info: Text.Info[Token]) => |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
101 |
opt_rendering match { |
63481 | 102 |
case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) => |
103 |
(rendering.indentation(info.range) min limit) max 0 |
|
104 |
case _ => 0 |
|
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
105 |
} |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
106 |
} |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
107 |
|
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
108 |
def indent_indent(tok: Token): Int = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
109 |
if (keywords.is_command(tok, keyword_open)) indent_size |
75423 | 110 |
else if (keywords.is_command(tok, keyword_close)) { - indent_size } |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
111 |
else 0 |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
112 |
|
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
113 |
def indent_offset(tok: Token): Int = |
63477
f5c81436b930
clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents:
63474
diff
changeset
|
114 |
if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
115 |
else 0 |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
116 |
|
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
117 |
def indent_structure: Int = |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
118 |
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
|
119 |
{ case ((ind, _), Text.Info(range, tok)) => |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
120 |
val ind1 = ind + indent_indent(tok) |
63479 | 121 |
if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) { |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
122 |
val line = buffer.getLineOfOffset(range.start) |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
123 |
line_head(line) match { |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
124 |
case Some(info) if info.info == tok => |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
125 |
(ind1 + indent_offset(tok) + line_indent(line), true) |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
126 |
case _ => (ind1, false) |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63450
diff
changeset
|
127 |
} |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
128 |
} |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
129 |
else (ind1, false) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
130 |
}).collectFirst({ case (i, true) => i }).getOrElse(0) |
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
131 |
|
63480 | 132 |
def indent_brackets: Int = |
73359 | 133 |
prev_line_span.foldLeft(0) { |
134 |
case (i, tok) => |
|
135 |
if (tok.is_open_bracket) i + indent_size |
|
136 |
else if (tok.is_close_bracket) i - indent_size |
|
137 |
else i |
|
138 |
} |
|
63480 | 139 |
|
140 |
def indent_extra: Int = |
|
71601 | 141 |
if (prev_span.exists(keywords.is_quasi_command)) indent_size |
63480 | 142 |
else 0 |
143 |
||
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
144 |
val indent = |
66179
148d61626014
indent = 0 for blank lines: produce less whitespace by default;
wenzelm
parents:
66178
diff
changeset
|
145 |
if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished) |
148d61626014
indent = 0 for blank lines: produce less whitespace by default;
wenzelm
parents:
66178
diff
changeset
|
146 |
line_indent(current_line) |
148d61626014
indent = 0 for blank lines: produce less whitespace by default;
wenzelm
parents:
66178
diff
changeset
|
147 |
else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0 |
148d61626014
indent = 0 for blank lines: produce less whitespace by default;
wenzelm
parents:
66178
diff
changeset
|
148 |
else { |
64518 | 149 |
line_head(current_line) match { |
73105
578a33042aa6
clarified: command keyword position is sufficient (amending 693a39f2cddc);
wenzelm
parents:
71601
diff
changeset
|
150 |
case Some(info) => |
578a33042aa6
clarified: command keyword position is sufficient (amending 693a39f2cddc);
wenzelm
parents:
71601
diff
changeset
|
151 |
val tok = info.info |
64518 | 152 |
if (tok.is_begin || |
153 |
keywords.is_before_command(tok) || |
|
154 |
keywords.is_command(tok, Keyword.theory)) 0 |
|
155 |
else if (keywords.is_command(tok, Keyword.proof_enclose)) |
|
156 |
indent_structure + script_indent(info) - indent_offset(tok) |
|
157 |
else if (keywords.is_command(tok, Keyword.proof)) |
|
158 |
(indent_structure + script_indent(info) - indent_offset(tok)) max indent_size |
|
159 |
else if (tok.is_command) indent_structure - indent_offset(tok) |
|
160 |
else { |
|
161 |
prev_line_command match { |
|
162 |
case None => |
|
163 |
val extra = |
|
164 |
(keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { |
|
165 |
case (true, true) | (false, false) => 0 |
|
166 |
case (true, false) => - indent_extra |
|
167 |
case (false, true) => indent_extra |
|
168 |
} |
|
169 |
line_indent(prev_line) + indent_brackets + extra - indent_offset(tok) |
|
170 |
case Some(prev_tok) => |
|
171 |
indent_structure + indent_brackets + indent_size - indent_offset(tok) - |
|
172 |
indent_offset(prev_tok) - indent_indent(prev_tok) |
|
173 |
} |
|
64536
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
174 |
} |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
175 |
case None => |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
176 |
prev_line_command match { |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
177 |
case None => |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
178 |
val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0 |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
179 |
line_indent(prev_line) + indent_brackets + extra |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
180 |
case Some(prev_tok) => |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
181 |
indent_structure + indent_brackets + indent_size - |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
182 |
indent_offset(prev_tok) - indent_indent(prev_tok) |
e61de633a3ed
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents:
64518
diff
changeset
|
183 |
} |
64518 | 184 |
} |
63428
005b490f0ce2
indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents:
63427
diff
changeset
|
185 |
} |
63423 | 186 |
|
63425 | 187 |
actions.clear() |
63439 | 188 |
actions.add(new IndentAction.AlignOffset(indent max 0)) |
66183 | 189 |
case None => |
63423 | 190 |
} |
63422 | 191 |
} |
192 |
} |
|
193 |
||
75393 | 194 |
def line_content( |
195 |
buffer: JEditBuffer, |
|
196 |
keywords: Keyword.Keywords, |
|
197 |
range: Text.Range, |
|
198 |
ctxt: Scan.Line_Context |
|
199 |
): (List[Token], Scan.Line_Context) = { |
|
67014 | 200 |
val text = JEdit_Lib.get_text(buffer, range).getOrElse("") |
66175 | 201 |
val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt) |
66173 | 202 |
val toks1 = toks.filterNot(_.is_space) |
66175 | 203 |
(toks1, ctxt1) |
66173 | 204 |
} |
205 |
||
75393 | 206 |
def split_line_content( |
207 |
buffer: JEditBuffer, |
|
208 |
keywords: Keyword.Keywords, |
|
209 |
line: Int, |
|
210 |
caret: Int |
|
211 |
): (List[Token], List[Token]) = { |
|
66173 | 212 |
val line_range = JEdit_Lib.line_range(buffer, line) |
66176 | 213 |
val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context |
66175 | 214 |
val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0) |
215 |
val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1) |
|
66173 | 216 |
(toks1, toks2) |
217 |
} |
|
218 |
||
63422 | 219 |
|
220 |
/* structure matching */ |
|
221 |
||
75393 | 222 |
object Matcher extends StructureMatcher { |
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
223 |
private def find_block( |
58752 | 224 |
open: Token => Boolean, |
225 |
close: Token => Boolean, |
|
226 |
reset: Token => Boolean, |
|
58762 | 227 |
restrict: Token => Boolean, |
75393 | 228 |
it: Iterator[Text.Info[Token]] |
229 |
): Option[(Text.Range, Text.Range)] = { |
|
73344 | 230 |
val range1 = it.next().range |
58762 | 231 |
it.takeWhile(info => !info.info.is_command || restrict(info.info)). |
232 |
scanLeft((range1, 1))( |
|
233 |
{ case ((r, d), Text.Info(range, tok)) => |
|
234 |
if (open(tok)) (range, d + 1) |
|
235 |
else if (close(tok)) (range, d - 1) |
|
236 |
else if (reset(tok)) (range, 0) |
|
237 |
else (r, d) } |
|
238 |
).collectFirst({ case (range2, 0) => (range1, range2) }) |
|
58752 | 239 |
} |
240 |
||
75393 | 241 |
private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = { |
58748 | 242 |
val buffer = text_area.getBuffer |
243 |
val caret_line = text_area.getCaretLine |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
244 |
val caret = text_area.getCaretPosition |
58748 | 245 |
|
59074 | 246 |
Isabelle.buffer_syntax(text_area.getBuffer) match { |
66183 | 247 |
case Some(syntax) => |
63424 | 248 |
val keywords = syntax.keywords |
58750 | 249 |
|
66183 | 250 |
val nav = new Navigator(syntax, buffer, false) |
58750 | 251 |
|
58752 | 252 |
def caret_iterator(): Iterator[Text.Info[Token]] = |
63425 | 253 |
nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
58752 | 254 |
|
63427 | 255 |
def reverse_caret_iterator(): Iterator[Text.Info[Token]] = |
256 |
nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
|
58752 | 257 |
|
63425 | 258 |
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
|
259 |
match { |
63424 | 260 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => |
58755 | 261 |
find_block( |
63424 | 262 |
keywords.is_command(_, Keyword.proof_goal), |
263 |
keywords.is_command(_, Keyword.qed), |
|
264 |
keywords.is_command(_, Keyword.qed_global), |
|
58762 | 265 |
t => |
63424 | 266 |
keywords.is_command(t, Keyword.diag) || |
267 |
keywords.is_command(t, Keyword.proof), |
|
58755 | 268 |
caret_iterator()) |
269 |
||
63424 | 270 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) => |
58755 | 271 |
find_block( |
63424 | 272 |
keywords.is_command(_, Keyword.proof_goal), |
273 |
keywords.is_command(_, Keyword.qed), |
|
58755 | 274 |
_ => false, |
58762 | 275 |
t => |
63424 | 276 |
keywords.is_command(t, Keyword.diag) || |
277 |
keywords.is_command(t, Keyword.proof), |
|
58755 | 278 |
caret_iterator()) |
279 |
||
63424 | 280 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => |
63427 | 281 |
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
|
282 |
match { |
58750 | 283 |
case Some(Text.Info(range2, tok)) |
63424 | 284 |
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
|
285 |
case _ => None |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
286 |
} |
58752 | 287 |
|
63424 | 288 |
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) => |
58755 | 289 |
find_block( |
63424 | 290 |
keywords.is_command(_, Keyword.qed), |
58755 | 291 |
t => |
63424 | 292 |
keywords.is_command(t, Keyword.proof_goal) || |
293 |
keywords.is_command(t, Keyword.theory_goal), |
|
58755 | 294 |
_ => false, |
58762 | 295 |
t => |
63424 | 296 |
keywords.is_command(t, Keyword.diag) || |
297 |
keywords.is_command(t, Keyword.proof) || |
|
298 |
keywords.is_command(t, Keyword.theory_goal), |
|
63427 | 299 |
reverse_caret_iterator()) |
58755 | 300 |
|
58752 | 301 |
case Some(Text.Info(range1, tok)) if tok.is_begin => |
58762 | 302 |
find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) |
58752 | 303 |
|
304 |
case Some(Text.Info(range1, tok)) if tok.is_end => |
|
63427 | 305 |
find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) |
58763 | 306 |
match { |
307 |
case Some((_, range2)) => |
|
63427 | 308 |
reverse_caret_iterator(). |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
309 |
dropWhile(info => info.range != range2). |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
310 |
dropWhile(info => info.range == range2). |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
311 |
find(info => info.info.is_command || info.info.is_begin) |
58763 | 312 |
match { |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
313 |
case Some(Text.Info(range3, tok)) => |
63424 | 314 |
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
|
315 |
else Some((range1, range2)) |
58763 | 316 |
case None => None |
317 |
} |
|
318 |
case None => None |
|
319 |
} |
|
58752 | 320 |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
321 |
case _ => None |
58748 | 322 |
} |
66183 | 323 |
case None => None |
58748 | 324 |
} |
325 |
} |
|
326 |
||
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
327 |
def getMatch(text_area: TextArea): StructureMatcher.Match = |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
328 |
find_pair(text_area) match { |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
329 |
case Some((_, range)) => |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
330 |
val line = text_area.getBuffer.getLineOfOffset(range.start) |
63422 | 331 |
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
|
332 |
case None => null |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
333 |
} |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
334 |
|
75393 | 335 |
def selectMatch(text_area: TextArea): Unit = { |
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
336 |
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
|
337 |
for { |
59074 | 338 |
syntax <- Isabelle.buffer_syntax(text_area.getBuffer) |
58803
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
339 |
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
|
340 |
} yield span.range |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
341 |
|
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
342 |
find_pair(text_area) match { |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
343 |
case Some((r1, r2)) => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
344 |
(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
|
345 |
case (Some(range1), Some(range2)) => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
346 |
val start = range1.start min range2.start |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
347 |
val stop = range1.stop max range2.stop |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
348 |
|
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
349 |
text_area.moveCaretPosition(stop, false) |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
350 |
if (!text_area.isMultipleSelectionEnabled) text_area.selectNone |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
351 |
text_area.addToSelection(new Selection.Range(start, stop)) |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
352 |
case _ => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
353 |
} |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
354 |
case None => |
7a0f675eb671
proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents:
58800
diff
changeset
|
355 |
} |
58748 | 356 |
} |
357 |
} |
|
358 |
} |