author | wenzelm |
Tue, 28 Oct 2014 11:42:51 +0100 | |
changeset 58800 | bfed1c26caed |
parent 58763 | 1b943a82d5ed |
child 58803 | 7a0f675eb671 |
permissions | -rw-r--r-- |
58748 | 1 |
/* Title: Tools/jEdit/src/structure_matching.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Structure matcher for Isabelle/Isar outer syntax. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
12 |
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher} |
|
13 |
||
14 |
||
15 |
object Structure_Matching |
|
16 |
{ |
|
17 |
object Isabelle_Matcher extends StructureMatcher |
|
18 |
{ |
|
58754 | 19 |
def find_block( |
58752 | 20 |
open: Token => Boolean, |
21 |
close: Token => Boolean, |
|
22 |
reset: Token => Boolean, |
|
58762 | 23 |
restrict: Token => Boolean, |
58754 | 24 |
it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] = |
58752 | 25 |
{ |
58754 | 26 |
val range1 = it.next.range |
58762 | 27 |
it.takeWhile(info => !info.info.is_command || restrict(info.info)). |
28 |
scanLeft((range1, 1))( |
|
29 |
{ case ((r, d), Text.Info(range, tok)) => |
|
30 |
if (open(tok)) (range, d + 1) |
|
31 |
else if (close(tok)) (range, d - 1) |
|
32 |
else if (reset(tok)) (range, 0) |
|
33 |
else (r, d) } |
|
34 |
).collectFirst({ case (range2, 0) => (range1, range2) }) |
|
58752 | 35 |
} |
36 |
||
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
37 |
def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = |
58748 | 38 |
{ |
39 |
val buffer = text_area.getBuffer |
|
40 |
val caret_line = text_area.getCaretLine |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
41 |
val caret = text_area.getCaretPosition |
58748 | 42 |
|
43 |
PIDE.session.recent_syntax match { |
|
58750 | 44 |
case syntax: Outer_Syntax |
45 |
if syntax != Outer_Syntax.empty => |
|
46 |
||
47 |
val limit = PIDE.options.value.int("jedit_structure_limit") max 0 |
|
48 |
||
49 |
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
|
58756
eb5d0c58564d
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents:
58755
diff
changeset
|
50 |
Token_Markup.line_token_iterator(syntax, buffer, line, line + lim). |
eb5d0c58564d
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents:
58755
diff
changeset
|
51 |
filter(_.info.is_proper) |
58750 | 52 |
|
53 |
def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = |
|
58756
eb5d0c58564d
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents:
58755
diff
changeset
|
54 |
Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim). |
eb5d0c58564d
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents:
58755
diff
changeset
|
55 |
filter(_.info.is_proper) |
58750 | 56 |
|
58752 | 57 |
def caret_iterator(): Iterator[Text.Info[Token]] = |
58 |
iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
|
59 |
||
60 |
def rev_caret_iterator(): Iterator[Text.Info[Token]] = |
|
61 |
rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) |
|
62 |
||
58756
eb5d0c58564d
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents:
58755
diff
changeset
|
63 |
iterator(caret_line, 1).find(info => info.range.touches(caret)) |
eb5d0c58564d
ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents:
58755
diff
changeset
|
64 |
match { |
58755 | 65 |
case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) => |
66 |
find_block( |
|
67 |
syntax.command_kind(_, Keyword.proof_goal), |
|
68 |
syntax.command_kind(_, Keyword.qed), |
|
69 |
syntax.command_kind(_, Keyword.qed_global), |
|
58762 | 70 |
t => |
71 |
syntax.command_kind(t, Keyword.diag) || |
|
72 |
syntax.command_kind(t, Keyword.proof), |
|
58755 | 73 |
caret_iterator()) |
74 |
||
75 |
case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) => |
|
76 |
find_block( |
|
77 |
syntax.command_kind(_, Keyword.proof_goal), |
|
78 |
syntax.command_kind(_, Keyword.qed), |
|
79 |
_ => false, |
|
58762 | 80 |
t => |
81 |
syntax.command_kind(t, Keyword.diag) || |
|
82 |
syntax.command_kind(t, Keyword.proof), |
|
58755 | 83 |
caret_iterator()) |
84 |
||
58750 | 85 |
case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) => |
58752 | 86 |
rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory)) |
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
87 |
match { |
58750 | 88 |
case Some(Text.Info(range2, tok)) |
89 |
if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
90 |
case _ => None |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
91 |
} |
58752 | 92 |
|
58755 | 93 |
case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) => |
94 |
find_block( |
|
95 |
syntax.command_kind(_, Keyword.qed), |
|
96 |
t => |
|
97 |
syntax.command_kind(t, Keyword.proof_goal) || |
|
98 |
syntax.command_kind(t, Keyword.theory_goal), |
|
99 |
_ => false, |
|
58762 | 100 |
t => |
101 |
syntax.command_kind(t, Keyword.diag) || |
|
102 |
syntax.command_kind(t, Keyword.proof) || |
|
103 |
syntax.command_kind(t, Keyword.theory_goal), |
|
58755 | 104 |
rev_caret_iterator()) |
105 |
||
58752 | 106 |
case Some(Text.Info(range1, tok)) if tok.is_begin => |
58762 | 107 |
find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) |
58752 | 108 |
|
109 |
case Some(Text.Info(range1, tok)) if tok.is_end => |
|
58762 | 110 |
find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator()) |
58763 | 111 |
match { |
112 |
case Some((_, range2)) => |
|
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
113 |
rev_caret_iterator(). |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
114 |
dropWhile(info => info.range != range2). |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
115 |
dropWhile(info => info.range == range2). |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
116 |
find(info => info.info.is_command || info.info.is_begin) |
58763 | 117 |
match { |
58800
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
118 |
case Some(Text.Info(range3, tok)) => |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
119 |
if (syntax.command_kind(tok, Keyword.theory_block)) Some((range1, range3)) |
bfed1c26caed
explicit keyword category for commands that may start a block;
wenzelm
parents:
58763
diff
changeset
|
120 |
else Some((range1, range2)) |
58763 | 121 |
case None => None |
122 |
} |
|
123 |
case None => None |
|
124 |
} |
|
58752 | 125 |
|
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
126 |
case _ => None |
58748 | 127 |
} |
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
128 |
case _ => None |
58748 | 129 |
} |
130 |
} |
|
131 |
||
58749
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
132 |
def getMatch(text_area: TextArea): StructureMatcher.Match = |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
133 |
find_pair(text_area) match { |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
134 |
case Some((_, range)) => |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
135 |
val line = text_area.getBuffer.getLineOfOffset(range.start) |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
136 |
new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher, |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
137 |
line, range.start, line, range.stop) |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
138 |
case None => null |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
139 |
} |
83b0f633190e
some structure matching, based on line token iterators;
wenzelm
parents:
58748
diff
changeset
|
140 |
|
58748 | 141 |
def selectMatch(text_area: TextArea) |
142 |
{ |
|
143 |
// FIXME |
|
144 |
} |
|
145 |
} |
|
146 |
} |
|
147 |