author | wenzelm |
Fri, 27 Mar 2020 22:01:27 +0100 | |
changeset 71601 | 97ccf48c2f0c |
parent 68729 | 3a02b424d5fb |
child 72740 | 082200ee003d |
permissions | -rw-r--r-- |
34166 | 1 |
/* Title: Pure/Isar/outer_syntax.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Isabelle/Isar outer syntax. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
43411
0206466ee473
some support for partial scans with explicit context;
wenzelm
parents:
40533
diff
changeset
|
10 |
import scala.collection.mutable |
34166 | 11 |
|
12 |
||
43774
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
13 |
object Outer_Syntax |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
14 |
{ |
58706 | 15 |
/* syntax */ |
16 |
||
17 |
val empty: Outer_Syntax = new Outer_Syntax() |
|
18 |
||
66776 | 19 |
def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _) |
66717
67dbf5cdc056
more informative loaded_theories: dependencies and syntax;
wenzelm
parents:
65384
diff
changeset
|
20 |
|
58706 | 21 |
|
22 |
/* string literals */ |
|
23 |
||
43774
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
24 |
def quote_string(str: String): String = |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
25 |
{ |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
26 |
val result = new StringBuilder(str.length + 10) |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
27 |
result += '"' |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
28 |
for (s <- Symbol.iterator(str)) { |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
29 |
if (s.length == 1) { |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
30 |
val c = s(0) |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
31 |
if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') { |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
32 |
result += '\\' |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
33 |
if (c < 10) result += '0' |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
34 |
if (c < 100) result += '0' |
60215 | 35 |
result ++= c.asInstanceOf[Int].toString |
43774
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
36 |
} |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
37 |
else result += c |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
38 |
} |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
39 |
else result ++= s |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
40 |
} |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
41 |
result += '"' |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
42 |
result.toString |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
43 |
} |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
44 |
} |
6dfdb70496fe
added Outer_Syntax.quote_string, which is conceptually a bit different from Token.unparse;
wenzelm
parents:
43695
diff
changeset
|
45 |
|
46712 | 46 |
final class Outer_Syntax private( |
58900 | 47 |
val keywords: Keyword.Keywords = Keyword.Keywords.empty, |
63867 | 48 |
val rev_abbrevs: Thy_Header.Abbrevs = Nil, |
55749 | 49 |
val language_context: Completion.Language_Context = Completion.Language_Context.outer, |
63584
68751fe1c036
tuned signature -- prover-independence is presently theoretical;
wenzelm
parents:
63579
diff
changeset
|
50 |
val has_tokens: Boolean = true) |
34166 | 51 |
{ |
58706 | 52 |
/** syntax content **/ |
53 |
||
58900 | 54 |
override def toString: String = keywords.toString |
56393
22f533e6a049
more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents:
56314
diff
changeset
|
55 |
|
58695 | 56 |
|
63867 | 57 |
/* keywords */ |
58695 | 58 |
|
65383 | 59 |
def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax = |
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
60 |
new Outer_Syntax( |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
61 |
keywords + (name, kind, exts), rev_abbrevs, language_context, has_tokens = true) |
48706 | 62 |
|
48873 | 63 |
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = |
64 |
(this /: keywords) { |
|
65384 | 65 |
case (syntax, (name, spec)) => |
66 |
syntax + |
|
67 |
(Symbol.decode(name), spec.kind, spec.exts) + |
|
68 |
(Symbol.encode(name), spec.kind, spec.exts) |
|
63579 | 69 |
} |
70 |
||
63867 | 71 |
|
72 |
/* abbrevs */ |
|
73 |
||
74 |
def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse |
|
75 |
||
76 |
def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax = |
|
77 |
if (new_abbrevs.isEmpty) this |
|
63579 | 78 |
else { |
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
79 |
val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
80 |
new Outer_Syntax(keywords, rev_abbrevs1, language_context, has_tokens) |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
81 |
} |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
82 |
|
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
83 |
|
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
84 |
/* completion */ |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
85 |
|
67005 | 86 |
private lazy val completion: Completion = |
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
87 |
{ |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
88 |
val completion_keywords = (keywords.minor.iterator ++ keywords.major.iterator).toList |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
89 |
val completion_abbrevs = |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
90 |
completion_keywords.flatMap(name => |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
91 |
(if (Keyword.theory_block.contains(keywords.kinds(name))) |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
92 |
List((name, name + "\nbegin\n\u0007\nend")) |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
93 |
else Nil) ::: |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
94 |
(if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil)) ::: |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
95 |
abbrevs.flatMap( |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
96 |
{ case (a, b) => |
63579 | 97 |
val a1 = Symbol.decode(a) |
98 |
val a2 = Symbol.encode(a) |
|
99 |
val b1 = Symbol.decode(b) |
|
100 |
List((a1, b1), (a2, b1)) |
|
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
101 |
}) |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
102 |
Completion.make(completion_keywords, completion_abbrevs) |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
103 |
} |
34166 | 104 |
|
67005 | 105 |
def complete( |
106 |
history: Completion.History, |
|
107 |
unicode: Boolean, |
|
108 |
explicit: Boolean, |
|
109 |
start: Text.Offset, |
|
110 |
text: CharSequence, |
|
111 |
caret: Int, |
|
112 |
context: Completion.Language_Context): Option[Completion.Result] = |
|
113 |
{ |
|
114 |
completion.complete(history, unicode, explicit, start, text, caret, context) |
|
115 |
} |
|
116 |
||
58695 | 117 |
|
66717
67dbf5cdc056
more informative loaded_theories: dependencies and syntax;
wenzelm
parents:
65384
diff
changeset
|
118 |
/* build */ |
67dbf5cdc056
more informative loaded_theories: dependencies and syntax;
wenzelm
parents:
65384
diff
changeset
|
119 |
|
67dbf5cdc056
more informative loaded_theories: dependencies and syntax;
wenzelm
parents:
65384
diff
changeset
|
120 |
def + (header: Document.Node.Header): Outer_Syntax = |
67dbf5cdc056
more informative loaded_theories: dependencies and syntax;
wenzelm
parents:
65384
diff
changeset
|
121 |
add_keywords(header.keywords).add_abbrevs(header.abbrevs) |
59073 | 122 |
|
63584
68751fe1c036
tuned signature -- prover-independence is presently theoretical;
wenzelm
parents:
63579
diff
changeset
|
123 |
def ++ (other: Outer_Syntax): Outer_Syntax = |
59073 | 124 |
if (this eq other) this |
66776 | 125 |
else if (this eq Outer_Syntax.empty) other |
59073 | 126 |
else { |
63865 | 127 |
val keywords1 = keywords ++ other.keywords |
63867 | 128 |
val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs) |
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
129 |
if ((keywords eq keywords1) && (rev_abbrevs eq rev_abbrevs1)) this |
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
130 |
else new Outer_Syntax(keywords1, rev_abbrevs1, language_context, has_tokens) |
59073 | 131 |
} |
132 |
||
133 |
||
59735 | 134 |
/* load commands */ |
58900 | 135 |
|
63441 | 136 |
def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name) |
58900 | 137 |
def load_commands_in(text: String): Boolean = keywords.load_commands_in(text) |
138 |
||
139 |
||
58706 | 140 |
/* language context */ |
34166 | 141 |
|
58706 | 142 |
def set_language_context(context: Completion.Language_Context): Outer_Syntax = |
67004
af72fa58f71b
clarified lazy Completion within Outer_Syntax: measurable speedup of Sessions.deps;
wenzelm
parents:
66984
diff
changeset
|
143 |
new Outer_Syntax(keywords, rev_abbrevs, context, has_tokens) |
58706 | 144 |
|
145 |
def no_tokens: Outer_Syntax = |
|
46969 | 146 |
{ |
58900 | 147 |
require(keywords.is_empty) |
58706 | 148 |
new Outer_Syntax( |
63867 | 149 |
rev_abbrevs = rev_abbrevs, |
58706 | 150 |
language_context = language_context, |
151 |
has_tokens = false) |
|
46969 | 152 |
} |
40454
2516ea25a54b
some support for nested source structure, based on section headings;
wenzelm
parents:
38471
diff
changeset
|
153 |
|
58706 | 154 |
|
40454
2516ea25a54b
some support for nested source structure, based on section headings;
wenzelm
parents:
38471
diff
changeset
|
155 |
|
58706 | 156 |
/** parsing **/ |
34166 | 157 |
|
58706 | 158 |
/* command spans */ |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
159 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
160 |
def parse_spans(toks: List[Token]): List[Command_Span.Span] = |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
161 |
{ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
162 |
val result = new mutable.ListBuffer[Command_Span.Span] |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
163 |
val content = new mutable.ListBuffer[Token] |
68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
67005
diff
changeset
|
164 |
val ignored = new mutable.ListBuffer[Token] |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
165 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
166 |
def ship(span: List[Token]) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
167 |
{ |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
168 |
val kind = |
68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
67005
diff
changeset
|
169 |
if (span.forall(_.is_ignored)) Command_Span.Ignored_Span |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
170 |
else if (span.exists(_.is_error)) Command_Span.Malformed_Span |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
171 |
else |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
172 |
span.find(_.is_command) match { |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
173 |
case None => Command_Span.Malformed_Span |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
174 |
case Some(cmd) => |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
175 |
val name = cmd.source |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
176 |
val offset = |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
177 |
(0 /: span.takeWhile(_ != cmd)) { |
64616 | 178 |
case (i, tok) => i + Symbol.length(tok.source) } |
179 |
val end_offset = offset + Symbol.length(name) |
|
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
180 |
val pos = Position.Range(Text.Range(offset, end_offset) + 1) |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
181 |
Command_Span.Command_Span(name, pos) |
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
182 |
} |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
183 |
result += Command_Span.Span(kind, span) |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
184 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
185 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
186 |
def flush() |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
187 |
{ |
59319 | 188 |
if (content.nonEmpty) { ship(content.toList); content.clear } |
68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
67005
diff
changeset
|
189 |
if (ignored.nonEmpty) { ship(ignored.toList); ignored.clear } |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
190 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
191 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
192 |
for (tok <- toks) { |
68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
67005
diff
changeset
|
193 |
if (tok.is_ignored) ignored += tok |
63441 | 194 |
else if (keywords.is_before_command(tok) || |
195 |
tok.is_command && |
|
71601 | 196 |
(!content.exists(keywords.is_before_command) || content.exists(_.is_command))) |
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59735
diff
changeset
|
197 |
{ flush(); content += tok } |
68729
3a02b424d5fb
clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
wenzelm
parents:
67005
diff
changeset
|
198 |
else { content ++= ignored; ignored.clear; content += tok } |
57905
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
199 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
200 |
flush() |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
201 |
|
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
202 |
result.toList |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
203 |
} |
c0c5652e796e
separate module Command_Span: mostly syntactic representation;
wenzelm
parents:
57901
diff
changeset
|
204 |
|
57906 | 205 |
def parse_spans(input: CharSequence): List[Command_Span.Span] = |
59083 | 206 |
parse_spans(Token.explode(keywords, input)) |
34166 | 207 |
} |