author | wenzelm |
Sat, 01 Sep 2018 20:20:50 +0200 | |
changeset 68871 | f5c76072db55 |
parent 68822 | 253f04c1e814 |
child 68884 | 9b97d0b20d95 |
permissions | -rw-r--r-- |
45670 | 1 |
/* Title: Pure/PIDE/markup.scala |
27958 | 2 |
Author: Makarius |
3 |
||
56743 | 4 |
Quasi-abstract markup elements. |
27958 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
27970 | 9 |
|
32450 | 10 |
object Markup |
11 |
{ |
|
56743 | 12 |
/* elements */ |
13 |
||
14 |
object Elements |
|
15 |
{ |
|
16 |
def apply(elems: Set[String]): Elements = new Elements(elems) |
|
17 |
def apply(elems: String*): Elements = apply(Set(elems: _*)) |
|
18 |
val empty: Elements = apply() |
|
19 |
val full: Elements = |
|
20 |
new Elements(Set.empty) |
|
21 |
{ |
|
22 |
override def apply(elem: String): Boolean = true |
|
23 |
override def toString: String = "Elements.full" |
|
24 |
} |
|
25 |
} |
|
26 |
||
27 |
sealed class Elements private[Markup](private val rep: Set[String]) |
|
28 |
{ |
|
29 |
def apply(elem: String): Boolean = rep.contains(elem) |
|
30 |
def + (elem: String): Elements = new Elements(rep + elem) |
|
31 |
def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep) |
|
65176 | 32 |
def - (elem: String): Elements = new Elements(rep - elem) |
33 |
def -- (elems: Elements): Elements = new Elements(rep -- elems.rep) |
|
56743 | 34 |
override def toString: String = rep.mkString("Elements(", ",", ")") |
35 |
} |
|
36 |
||
37 |
||
45666 | 38 |
/* properties */ |
29184 | 39 |
|
40 |
val NAME = "name" |
|
43780 | 41 |
val Name = new Properties.String(NAME) |
42136 | 42 |
|
29184 | 43 |
val KIND = "kind" |
43780 | 44 |
val Kind = new Properties.String(KIND) |
29184 | 45 |
|
65937 | 46 |
val CONTENT = "content" |
47 |
val Content = new Properties.String(CONTENT) |
|
48 |
||
60744 | 49 |
val SERIAL = "serial" |
50 |
val Serial = new Properties.Long(SERIAL) |
|
51 |
||
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
52 |
val INSTANCE = "instance" |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
53 |
val Instance = new Properties.String(INSTANCE) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
54 |
|
29184 | 55 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
56 |
/* basic markup */ |
29184 | 57 |
|
45666 | 58 |
val Empty = Markup("", Nil) |
59 |
val Broken = Markup("broken", Nil) |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
60 |
|
55551 | 61 |
class Markup_String(val name: String, prop: String) |
62 |
{ |
|
63 |
private val Prop = new Properties.String(prop) |
|
64 |
||
65 |
def apply(s: String): Markup = Markup(name, Prop(s)) |
|
66 |
def unapply(markup: Markup): Option[String] = |
|
67 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
68 |
} |
|
69 |
||
70 |
class Markup_Int(val name: String, prop: String) |
|
71 |
{ |
|
72 |
private val Prop = new Properties.Int(prop) |
|
73 |
||
74 |
def apply(i: Int): Markup = Markup(name, Prop(i)) |
|
75 |
def unapply(markup: Markup): Option[Int] = |
|
76 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
77 |
} |
|
78 |
||
60744 | 79 |
class Markup_Long(val name: String, prop: String) |
80 |
{ |
|
81 |
private val Prop = new Properties.Long(prop) |
|
82 |
||
83 |
def apply(i: Long): Markup = Markup(name, Prop(i)) |
|
84 |
def unapply(markup: Markup): Option[Long] = |
|
85 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
86 |
} |
|
87 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
88 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
89 |
/* formal entities */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
90 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
91 |
val BINDING = "binding" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
92 |
val ENTITY = "entity" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
93 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
94 |
object Entity |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
95 |
{ |
62986 | 96 |
val Def = new Properties.Long("def") |
97 |
val Ref = new Properties.Long("ref") |
|
98 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
99 |
def unapply(markup: Markup): Option[(String, String)] = |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
100 |
markup match { |
55551 | 101 |
case Markup(ENTITY, props) => |
63337 | 102 |
val kind = Kind.unapply(props).getOrElse("") |
103 |
val name = Name.unapply(props).getOrElse("") |
|
104 |
Some((kind, name)) |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
105 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
106 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
107 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
108 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
109 |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
110 |
/* completion */ |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
111 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
112 |
val COMPLETION = "completion" |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55837
diff
changeset
|
113 |
val NO_COMPLETION = "no_completion" |
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
114 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
115 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
116 |
/* position */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
117 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
118 |
val LINE = "line" |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58853
diff
changeset
|
119 |
val END_LINE = "line" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
120 |
val OFFSET = "offset" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
121 |
val END_OFFSET = "end_offset" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
122 |
val FILE = "file" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
123 |
val ID = "id" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
124 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
125 |
val DEF_LINE = "def_line" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
126 |
val DEF_OFFSET = "def_offset" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
127 |
val DEF_END_OFFSET = "def_end_offset" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
128 |
val DEF_FILE = "def_file" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
129 |
val DEF_ID = "def_id" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
130 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
131 |
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
132 |
val POSITION = "position" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
133 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
134 |
|
58464 | 135 |
/* expression */ |
136 |
||
137 |
val EXPRESSION = "expression" |
|
62806 | 138 |
object Expression |
139 |
{ |
|
140 |
def unapply(markup: Markup): Option[String] = |
|
141 |
markup match { |
|
142 |
case Markup(EXPRESSION, Kind(kind)) => Some(kind) |
|
143 |
case Markup(EXPRESSION, _) => Some("") |
|
144 |
case _ => None |
|
145 |
} |
|
146 |
} |
|
58464 | 147 |
|
148 |
||
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
149 |
/* citation */ |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
150 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
151 |
val CITATION = "citation" |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
152 |
val Citation = new Markup_String(CITATION, NAME) |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
153 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
154 |
|
55550 | 155 |
/* embedded languages */ |
156 |
||
55666 | 157 |
val Symbols = new Properties.Boolean("symbols") |
158 |
val Antiquotes = new Properties.Boolean("antiquotes") |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
159 |
val Delimited = new Properties.Boolean("delimited") |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
160 |
|
55550 | 161 |
val LANGUAGE = "language" |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
162 |
object Language |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
163 |
{ |
67336 | 164 |
val DOCUMENT = "document" |
55616 | 165 |
val ML = "ML" |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
166 |
val SML = "SML" |
56843
b2bfcd8cda80
support for path completion based on file-system content;
wenzelm
parents:
56743
diff
changeset
|
167 |
val PATH = "path" |
55616 | 168 |
val UNKNOWN = "unknown" |
169 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
170 |
def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] = |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
171 |
markup match { |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
172 |
case Markup(LANGUAGE, props) => |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
173 |
(props, props, props, props) match { |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
174 |
case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) => |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
175 |
Some((name, symbols, antiquotes, delimited)) |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
176 |
case _ => None |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
177 |
} |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
178 |
case _ => None |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
179 |
} |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
180 |
} |
55550 | 181 |
|
182 |
||
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
183 |
/* external resources */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
184 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
185 |
val PATH = "path" |
55551 | 186 |
val Path = new Markup_String(PATH, NAME) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
187 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
188 |
val URL = "url" |
55551 | 189 |
val Url = new Markup_String(URL, NAME) |
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
190 |
|
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
191 |
val DOC = "doc" |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
192 |
val Doc = new Markup_String(DOC, NAME) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
193 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
194 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
195 |
/* pretty printing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
196 |
|
61864 | 197 |
val Consistent = new Properties.Boolean("consistent") |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
198 |
val Indent = new Properties.Int("indent") |
61864 | 199 |
val Width = new Properties.Int("width") |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
200 |
|
61864 | 201 |
object Block |
202 |
{ |
|
203 |
val name = "block" |
|
204 |
def apply(c: Boolean, i: Int): Markup = |
|
205 |
Markup(name, |
|
206 |
(if (c) Consistent(c) else Nil) ::: |
|
207 |
(if (i != 0) Indent(i) else Nil)) |
|
208 |
def unapply(markup: Markup): Option[(Boolean, Int)] = |
|
209 |
if (markup.name == name) { |
|
210 |
val c = Consistent.unapply(markup.properties).getOrElse(false) |
|
211 |
val i = Indent.unapply(markup.properties).getOrElse(0) |
|
212 |
Some((c, i)) |
|
213 |
} |
|
214 |
else None |
|
215 |
} |
|
216 |
||
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
217 |
object Break |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
218 |
{ |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
219 |
val name = "break" |
61864 | 220 |
def apply(w: Int, i: Int): Markup = |
221 |
Markup(name, |
|
222 |
(if (w != 0) Width(w) else Nil) ::: |
|
223 |
(if (i != 0) Indent(i) else Nil)) |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
224 |
def unapply(markup: Markup): Option[(Int, Int)] = |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
225 |
if (markup.name == name) { |
61864 | 226 |
val w = Width.unapply(markup.properties).getOrElse(0) |
227 |
val i = Indent.unapply(markup.properties).getOrElse(0) |
|
228 |
Some((w, i)) |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
229 |
} |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
230 |
else None |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
231 |
} |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
232 |
|
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
50975
diff
changeset
|
233 |
val ITEM = "item" |
51574
2b58d7b139d6
ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents:
51570
diff
changeset
|
234 |
val BULLET = "bullet" |
51570
3633828d80fc
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
wenzelm
parents:
50975
diff
changeset
|
235 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
236 |
val SEPARATOR = "separator" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
237 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
238 |
|
56548 | 239 |
/* text properties */ |
240 |
||
241 |
val WORDS = "words" |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
242 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
243 |
val HIDDEN = "hidden" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
244 |
|
68298
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68148
diff
changeset
|
245 |
val DELETE = "delete" |
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68148
diff
changeset
|
246 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
247 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57595
diff
changeset
|
248 |
/* misc entities */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
249 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
250 |
val CLASS = "class" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
251 |
val TYPE_NAME = "type_name" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
252 |
val FIXED = "fixed" |
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53055
diff
changeset
|
253 |
val CASE = "case" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
254 |
val CONSTANT = "constant" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
255 |
val DYNAMIC_FACT = "dynamic_fact" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
256 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
257 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
258 |
/* inner syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
259 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
260 |
val TFREE = "tfree" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
261 |
val TVAR = "tvar" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
262 |
val FREE = "free" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
263 |
val SKOLEM = "skolem" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
264 |
val BOUND = "bound" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
265 |
val VAR = "var" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
266 |
val NUMERAL = "numeral" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
267 |
val LITERAL = "literal" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
268 |
val DELIMITER = "delimiter" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
269 |
val INNER_STRING = "inner_string" |
55033 | 270 |
val INNER_CARTOUCHE = "inner_cartouche" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
271 |
val INNER_COMMENT = "inner_comment" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
272 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
273 |
val TOKEN_RANGE = "token_range" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
274 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
275 |
val SORTING = "sorting" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
276 |
val TYPING = "typing" |
63347 | 277 |
val CLASS_PARAMETER = "class_parameter" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
278 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
279 |
val ATTRIBUTE = "attribute" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
280 |
val METHOD = "method" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
281 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
282 |
|
55550 | 283 |
/* antiquotations */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
284 |
|
55526 | 285 |
val ANTIQUOTED = "antiquoted" |
286 |
val ANTIQUOTE = "antiquote" |
|
287 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
288 |
val ML_ANTIQUOTATION = "ML_antiquotation" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
289 |
val DOCUMENT_ANTIQUOTATION = "document_antiquotation" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
290 |
val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
291 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
292 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
293 |
/* text structure */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
294 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
295 |
val PARAGRAPH = "paragraph" |
50545
00bdc48c5f71
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents:
50543
diff
changeset
|
296 |
val TEXT_FOLD = "text_fold" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
297 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
298 |
|
61449 | 299 |
/* Markdown document structure */ |
300 |
||
301 |
val MARKDOWN_PARAGRAPH = "markdown_paragraph" |
|
67323
d02208cefbdb
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
wenzelm
parents:
67322
diff
changeset
|
302 |
val MARKDOWN_ITEM = "markdown_item" |
67336 | 303 |
val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth") |
61449 | 304 |
val Markdown_List = new Markup_String("markdown_list", "kind") |
67336 | 305 |
|
306 |
val ITEMIZE = "itemize" |
|
307 |
val ENUMERATE = "enumerate" |
|
308 |
val DESCRIPTION = "description" |
|
61449 | 309 |
|
310 |
||
60744 | 311 |
/* ML */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
312 |
|
55505 | 313 |
val ML_KEYWORD1 = "ML_keyword1" |
314 |
val ML_KEYWORD2 = "ML_keyword2" |
|
315 |
val ML_KEYWORD3 = "ML_keyword3" |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
316 |
val ML_DELIMITER = "ML_delimiter" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
317 |
val ML_TVAR = "ML_tvar" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
318 |
val ML_NUMERAL = "ML_numeral" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
319 |
val ML_CHAR = "ML_char" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
320 |
val ML_STRING = "ML_string" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
321 |
val ML_COMMENT = "ML_comment" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
322 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
323 |
val ML_DEF = "ML_def" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
324 |
val ML_OPEN = "ML_open" |
55837 | 325 |
val ML_STRUCTURE = "ML_structure" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
326 |
val ML_TYPING = "ML_typing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
327 |
|
60744 | 328 |
val ML_BREAKPOINT = "ML_breakpoint" |
329 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
330 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
331 |
/* outer syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
332 |
|
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
333 |
val COMMAND = "command" |
66044 | 334 |
val KEYWORD = "keyword" |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
335 |
val KEYWORD1 = "keyword1" |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
336 |
val KEYWORD2 = "keyword2" |
55765 | 337 |
val KEYWORD3 = "keyword3" |
55919
2eb8c13339a5
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
wenzelm
parents:
55914
diff
changeset
|
338 |
val QUASI_KEYWORD = "quasi_keyword" |
56202 | 339 |
val IMPROPER = "improper" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
340 |
val OPERATOR = "operator" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
341 |
val STRING = "string" |
59081 | 342 |
val ALT_STRING = "alt_string" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
343 |
val VERBATIM = "verbatim" |
55033 | 344 |
val CARTOUCHE = "cartouche" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
345 |
val COMMENT = "comment" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
346 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
347 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
348 |
/* timing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
349 |
|
50781 | 350 |
val Elapsed = new Properties.Double("elapsed") |
351 |
val CPU = new Properties.Double("cpu") |
|
352 |
val GC = new Properties.Double("gc") |
|
353 |
||
354 |
object Timing_Properties |
|
355 |
{ |
|
356 |
def apply(timing: isabelle.Timing): Properties.T = |
|
357 |
Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds) |
|
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
358 |
|
50781 | 359 |
def unapply(props: Properties.T): Option[isabelle.Timing] = |
360 |
(props, props, props) match { |
|
361 |
case (Elapsed(elapsed), CPU(cpu), GC(gc)) => |
|
362 |
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) |
|
363 |
case _ => None |
|
364 |
} |
|
365 |
} |
|
366 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
367 |
val TIMING = "timing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
368 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
369 |
object Timing |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
370 |
{ |
50781 | 371 |
def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing)) |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
372 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
373 |
def unapply(markup: Markup): Option[isabelle.Timing] = |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
374 |
markup match { |
50781 | 375 |
case Markup(TIMING, Timing_Properties(timing)) => Some(timing) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
376 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
377 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
378 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
379 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
380 |
|
65317 | 381 |
/* process result */ |
382 |
||
383 |
val Return_Code = new Properties.Int("return_code") |
|
384 |
||
385 |
object Process_Result |
|
386 |
{ |
|
387 |
def apply(result: Process_Result): Properties.T = |
|
388 |
Return_Code(result.rc) ::: |
|
389 |
(if (result.timing.is_zero) Nil else Timing_Properties(result.timing)) |
|
390 |
||
391 |
def unapply(props: Properties.T): Option[Process_Result] = |
|
392 |
props match { |
|
393 |
case Return_Code(rc) => |
|
394 |
val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero) |
|
395 |
Some(isabelle.Process_Result(rc, timing = timing)) |
|
396 |
case _ => None |
|
397 |
} |
|
398 |
} |
|
399 |
||
400 |
||
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
401 |
/* command indentation */ |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
402 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
403 |
object Command_Indent |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
404 |
{ |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
405 |
val name = "command_indent" |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
406 |
def unapply(markup: Markup): Option[Int] = |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
407 |
if (markup.name == name) Indent.unapply(markup.properties) else None |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
408 |
} |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
409 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
410 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
411 |
/* goals */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
412 |
|
50543 | 413 |
val GOAL = "goal" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
414 |
val SUBGOAL = "subgoal" |
50215 | 415 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset
|
416 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
417 |
/* command status */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
418 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
419 |
val TASK = "task" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
420 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
421 |
val ACCEPTED = "accepted" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
422 |
val FORKED = "forked" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
423 |
val JOINED = "joined" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
424 |
val RUNNING = "running" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
425 |
val FINISHED = "finished" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
426 |
val FAILED = "failed" |
68871
f5c76072db55
more explicit status for "canceled" command within theory node;
wenzelm
parents:
68822
diff
changeset
|
427 |
val CANCELED = "canceled" |
68323 | 428 |
val INITIALIZED = "initialized" |
66379
6392766f3c25
maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
wenzelm
parents:
66044
diff
changeset
|
429 |
val CONSOLIDATED = "consolidated" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
430 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
431 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
432 |
/* interactive documents */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
433 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
434 |
val VERSION = "version" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
435 |
val ASSIGN = "assign" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
436 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
437 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
438 |
/* prover process */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
439 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
440 |
val PROVER_COMMAND = "prover_command" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
441 |
val PROVER_ARG = "prover_arg" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
442 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
443 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
444 |
/* messages */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
445 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
446 |
val INIT = "init" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
447 |
val STATUS = "status" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
448 |
val REPORT = "report" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
449 |
val RESULT = "result" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
450 |
val WRITELN = "writeln" |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
451 |
val STATE = "state" |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
452 |
val INFORMATION = "information" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
453 |
val TRACING = "tracing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
454 |
val WARNING = "warning" |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
455 |
val LEGACY = "legacy" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
456 |
val ERROR = "error" |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68323
diff
changeset
|
457 |
val NODES_STATUS = "nodes_status" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
458 |
val PROTOCOL = "protocol" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
459 |
val SYSTEM = "system" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
460 |
val STDOUT = "stdout" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
461 |
val STDERR = "stderr" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
462 |
val EXIT = "exit" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
463 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
464 |
val WRITELN_MESSAGE = "writeln_message" |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
465 |
val STATE_MESSAGE = "state_message" |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
466 |
val INFORMATION_MESSAGE = "information_message" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
467 |
val TRACING_MESSAGE = "tracing_message" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
468 |
val WARNING_MESSAGE = "warning_message" |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
469 |
val LEGACY_MESSAGE = "legacy_message" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
470 |
val ERROR_MESSAGE = "error_message" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
471 |
|
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
472 |
val messages = Map( |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
473 |
WRITELN -> WRITELN_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
474 |
STATE -> STATE_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
475 |
INFORMATION -> INFORMATION_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
476 |
TRACING -> TRACING_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
477 |
WARNING -> WARNING_MESSAGE, |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
478 |
LEGACY -> LEGACY_MESSAGE, |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
479 |
ERROR -> ERROR_MESSAGE) |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
480 |
|
52876 | 481 |
val message: String => String = messages.withDefault((s: String) => s) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
482 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
483 |
val NO_REPORT = "no_report" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
484 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
485 |
val BAD = "bad" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
486 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
487 |
val INTENSIFY = "intensify" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
488 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
489 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
490 |
/* active areas */ |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
491 |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50545
diff
changeset
|
492 |
val BROWSER = "browser" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
493 |
val GRAPHVIEW = "graphview" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
494 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
495 |
val SENDBACK = "sendback" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
496 |
val PADDING = "padding" |
52697
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52643
diff
changeset
|
497 |
val PADDING_LINE = (PADDING, "line") |
6fb98a20c349
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm
parents:
52643
diff
changeset
|
498 |
val PADDING_COMMAND = (PADDING, "command") |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
499 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
500 |
val DIALOG = "dialog" |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50501
diff
changeset
|
501 |
val Result = new Properties.String(RESULT) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
502 |
|
63681 | 503 |
val JEDIT_ACTION = "jedit_action" |
504 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
505 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
506 |
/* protocol message functions */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
507 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
508 |
val FUNCTION = "function" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
509 |
val Function = new Properties.String(FUNCTION) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
510 |
|
66942
91a21a5631ae
proper order of initialization (amending 9953ae603a23);
wenzelm
parents:
66873
diff
changeset
|
511 |
val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing") |
91a21a5631ae
proper order of initialization (amending 9953ae603a23);
wenzelm
parents:
66873
diff
changeset
|
512 |
val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing") |
91a21a5631ae
proper order of initialization (amending 9953ae603a23);
wenzelm
parents:
66873
diff
changeset
|
513 |
|
52563 | 514 |
val Assign_Update: Properties.T = List((FUNCTION, "assign_update")) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
515 |
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions")) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
516 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
517 |
object Protocol_Handler |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
518 |
{ |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
519 |
def unapply(props: Properties.T): Option[(String)] = |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
520 |
props match { |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
521 |
case List((FUNCTION, "protocol_handler"), (NAME, name)) => Some(name) |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
522 |
case _ => None |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
523 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
524 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
525 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
526 |
val INVOKE_SCALA = "invoke_scala" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
527 |
object Invoke_Scala |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
528 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
529 |
def unapply(props: Properties.T): Option[(String, String)] = |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
530 |
props match { |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
531 |
case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id)) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
532 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
533 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
534 |
} |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
535 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
536 |
val CANCEL_SCALA = "cancel_scala" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
537 |
object Cancel_Scala |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
538 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
539 |
def unapply(props: Properties.T): Option[String] = |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
540 |
props match { |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
541 |
case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
542 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
543 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
544 |
} |
50255 | 545 |
|
546 |
object ML_Statistics |
|
547 |
{ |
|
548 |
def unapply(props: Properties.T): Option[Properties.T] = |
|
549 |
props match { |
|
66872 | 550 |
case (FUNCTION, "ML_statistics") :: props => Some(props) |
50255 | 551 |
case _ => None |
552 |
} |
|
553 |
} |
|
50975 | 554 |
|
555 |
object Task_Statistics |
|
556 |
{ |
|
557 |
def unapply(props: Properties.T): Option[Properties.T] = |
|
558 |
props match { |
|
66872 | 559 |
case (FUNCTION, "task_statistics") :: props => Some(props) |
50975 | 560 |
case _ => None |
561 |
} |
|
562 |
} |
|
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
563 |
|
59367 | 564 |
val LOADING_THEORY = "loading_theory" |
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
565 |
object Loading_Theory |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
566 |
{ |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
567 |
def unapply(props: Properties.T): Option[String] = |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
568 |
props match { |
59367 | 569 |
case List((FUNCTION, LOADING_THEORY), (NAME, name)) => Some(name) |
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
570 |
case _ => None |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
571 |
} |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
572 |
} |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
573 |
|
68088 | 574 |
val EXPORT = "export" |
575 |
object Export |
|
576 |
{ |
|
68101 | 577 |
sealed case class Args( |
578 |
id: Option[String], serial: Long, theory_name: String, name: String, compress: Boolean) |
|
68088 | 579 |
|
580 |
val THEORY_NAME = "theory_name" |
|
581 |
val COMPRESS = "compress" |
|
582 |
||
68148 | 583 |
def dest_inline(props: Properties.T): Option[(Args, Path)] = |
68088 | 584 |
props match { |
585 |
case |
|
68101 | 586 |
List( |
587 |
(SERIAL, Value.Long(serial)), |
|
588 |
(THEORY_NAME, theory_name), |
|
589 |
(NAME, name), |
|
590 |
(COMPRESS, Value.Boolean(compress)), |
|
68148 | 591 |
(FILE, file)) if isabelle.Path.is_valid(file) => |
592 |
Some((Args(None, serial, theory_name, name, compress), isabelle.Path.explode(file))) |
|
68088 | 593 |
case _ => None |
594 |
} |
|
595 |
||
596 |
def unapply(props: Properties.T): Option[Args] = |
|
597 |
props match { |
|
68101 | 598 |
case List( |
599 |
(FUNCTION, EXPORT), |
|
600 |
(ID, id), |
|
601 |
(SERIAL, Value.Long(serial)), |
|
602 |
(THEORY_NAME, theory_name), |
|
603 |
(NAME, name), |
|
604 |
(COMPRESS, Value.Boolean(compress))) => |
|
605 |
Some(Args(proper_string(id), serial, theory_name, name, compress)) |
|
68088 | 606 |
case _ => None |
607 |
} |
|
608 |
} |
|
609 |
||
65313 | 610 |
val BUILD_SESSION_FINISHED = "build_session_finished" |
611 |
val Build_Session_Finished: Properties.T = List((FUNCTION, BUILD_SESSION_FINISHED)) |
|
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
612 |
|
56864 | 613 |
val PRINT_OPERATIONS = "print_operations" |
614 |
||
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
615 |
|
60830 | 616 |
/* debugger output */ |
617 |
||
60842 | 618 |
val DEBUGGER_STATE = "debugger_state" |
619 |
object Debugger_State |
|
620 |
{ |
|
621 |
def unapply(props: Properties.T): Option[String] = |
|
622 |
props match { |
|
623 |
case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name) |
|
624 |
case _ => None |
|
625 |
} |
|
626 |
} |
|
627 |
||
60830 | 628 |
val DEBUGGER_OUTPUT = "debugger_output" |
629 |
object Debugger_Output |
|
630 |
{ |
|
60834 | 631 |
def unapply(props: Properties.T): Option[String] = |
60830 | 632 |
props match { |
60834 | 633 |
case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name) |
60830 | 634 |
case _ => None |
635 |
} |
|
636 |
} |
|
637 |
||
638 |
||
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
639 |
/* simplifier trace */ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
640 |
|
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
641 |
val SIMP_TRACE_PANEL = "simp_trace_panel" |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
642 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
643 |
val SIMP_TRACE_LOG = "simp_trace_log" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
644 |
val SIMP_TRACE_STEP = "simp_trace_step" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
645 |
val SIMP_TRACE_RECURSE = "simp_trace_recurse" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
646 |
val SIMP_TRACE_HINT = "simp_trace_hint" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
647 |
val SIMP_TRACE_IGNORE = "simp_trace_ignore" |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
648 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
649 |
val SIMP_TRACE_CANCEL = "simp_trace_cancel" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
650 |
object Simp_Trace_Cancel |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
651 |
{ |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
652 |
def unapply(props: Properties.T): Option[Long] = |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
653 |
props match { |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
654 |
case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i) |
55316
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
655 |
case _ => None |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
656 |
} |
885500f4aa6a
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents:
55033
diff
changeset
|
657 |
} |
65335 | 658 |
|
659 |
||
660 |
/* XML data representation */ |
|
661 |
||
662 |
def encode: XML.Encode.T[Markup] = (markup: Markup) => |
|
663 |
{ |
|
664 |
import XML.Encode._ |
|
665 |
pair(string, properties)((markup.name, markup.properties)) |
|
666 |
} |
|
667 |
||
668 |
def decode: XML.Decode.T[Markup] = (body: XML.Body) => |
|
669 |
{ |
|
670 |
import XML.Decode._ |
|
671 |
val (name, props) = pair(string, properties)(body) |
|
672 |
Markup(name, props) |
|
673 |
} |
|
45666 | 674 |
} |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
675 |
|
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
676 |
|
45666 | 677 |
sealed case class Markup(name: String, properties: Properties.T) |
59707 | 678 |
{ |
679 |
def markup(s: String): String = |
|
680 |
YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) |
|
64358 | 681 |
|
682 |
def update_properties(more_props: Properties.T): Markup = |
|
683 |
if (more_props.isEmpty) this |
|
684 |
else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) }) |
|
65753 | 685 |
|
686 |
def + (entry: Properties.Entry): Markup = |
|
687 |
Markup(name, Properties.put(properties, entry)) |
|
59707 | 688 |
} |