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