author | wenzelm |
Sat, 20 Nov 2021 20:42:41 +0100 | |
changeset 74826 | 0e4d8aa61ad7 |
parent 74823 | d6ce4ce20422 |
child 74829 | f31229171b3b |
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 |
|
71601 | 61 |
val Empty: Markup = Markup("", Nil) |
62 |
val Broken: Markup = 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 |
|
74783 | 64 |
class Markup_Elem(val name: String) |
65 |
{ |
|
66 |
def apply(props: Properties.T = Nil): Markup = Markup(name, props) |
|
67 |
def unapply(markup: Markup): Option[Properties.T] = |
|
68 |
if (markup.name == name) Some(markup.properties) else None |
|
69 |
} |
|
70 |
||
55551 | 71 |
class Markup_String(val name: String, prop: String) |
72 |
{ |
|
74782 | 73 |
val Prop: Properties.String = new Properties.String(prop) |
55551 | 74 |
|
75 |
def apply(s: String): Markup = Markup(name, Prop(s)) |
|
76 |
def unapply(markup: Markup): Option[String] = |
|
77 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
74782 | 78 |
def get(markup: Markup): String = unapply(markup).getOrElse("") |
55551 | 79 |
} |
80 |
||
81 |
class Markup_Int(val name: String, prop: String) |
|
82 |
{ |
|
74782 | 83 |
val Prop: Properties.Int = new Properties.Int(prop) |
55551 | 84 |
|
85 |
def apply(i: Int): Markup = Markup(name, Prop(i)) |
|
86 |
def unapply(markup: Markup): Option[Int] = |
|
87 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
74782 | 88 |
def get(markup: Markup): Int = unapply(markup).getOrElse(0) |
55551 | 89 |
} |
90 |
||
60744 | 91 |
class Markup_Long(val name: String, prop: String) |
92 |
{ |
|
74782 | 93 |
val Prop: Properties.Long = new Properties.Long(prop) |
60744 | 94 |
|
95 |
def apply(i: Long): Markup = Markup(name, Prop(i)) |
|
96 |
def unapply(markup: Markup): Option[Long] = |
|
97 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
74782 | 98 |
def get(markup: Markup): Long = unapply(markup).getOrElse(0) |
60744 | 99 |
} |
100 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
101 |
|
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69788
diff
changeset
|
102 |
/* meta data */ |
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69788
diff
changeset
|
103 |
|
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69788
diff
changeset
|
104 |
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
|
105 |
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
|
106 |
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
|
107 |
val META_DATE = "meta_date" |
69962
82e945d472d5
documentation of document markers and re-interpreted command tags;
wenzelm
parents:
69916
diff
changeset
|
108 |
val META_LICENSE = "meta_license" |
69889
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69788
diff
changeset
|
109 |
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
|
110 |
|
be04e9a053a7
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm
parents:
69788
diff
changeset
|
111 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
112 |
/* formal entities */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
113 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
114 |
val BINDING = "binding" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
115 |
val ENTITY = "entity" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
116 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
117 |
object Entity |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
118 |
{ |
74782 | 119 |
val Def = new Markup_Long(ENTITY, "def") |
120 |
val Ref = new Markup_Long(ENTITY, "ref") |
|
121 |
||
72929 | 122 |
object Occ |
72903 | 123 |
{ |
124 |
def unapply(markup: Markup): Option[Long] = |
|
125 |
Def.unapply(markup) orElse Ref.unapply(markup) |
|
126 |
} |
|
127 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
128 |
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
|
129 |
markup match { |
74782 | 130 |
case Markup(ENTITY, props) => Some((Kind.get(props), Name.get(props))) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
131 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
132 |
} |
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 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
135 |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
136 |
/* completion */ |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
137 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
138 |
val COMPLETION = "completion" |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55837
diff
changeset
|
139 |
val NO_COMPLETION = "no_completion" |
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
140 |
|
69557 | 141 |
val UPDATE = "update" |
142 |
||
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
143 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
144 |
/* position */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
145 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
146 |
val LINE = "line" |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58853
diff
changeset
|
147 |
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
|
148 |
val OFFSET = "offset" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
149 |
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
|
150 |
val FILE = "file" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
151 |
val ID = "id" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
152 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
153 |
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
|
154 |
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
|
155 |
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
|
156 |
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
|
157 |
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
|
158 |
|
74263
be49c660ebbf
more markup, e.g. to locate defining theory node in formal document output;
wenzelm
parents:
74261
diff
changeset
|
159 |
val DEF_THEORY = "def_theory" |
be49c660ebbf
more markup, e.g. to locate defining theory node in formal document output;
wenzelm
parents:
74261
diff
changeset
|
160 |
|
74182 | 161 |
val POSITION = "position" |
162 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
163 |
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) |
72708 | 164 |
def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1) |
165 |
||
74182 | 166 |
|
167 |
/* position "def" name */ |
|
168 |
||
169 |
private val def_names: Map[String, String] = |
|
170 |
Map(LINE -> DEF_LINE, OFFSET -> DEF_OFFSET, END_OFFSET -> DEF_END_OFFSET, |
|
171 |
FILE -> DEF_FILE, ID -> DEF_ID) |
|
172 |
||
173 |
def def_name(a: String): String = def_names.getOrElse(a, a + "def_") |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
174 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
175 |
|
58464 | 176 |
/* expression */ |
177 |
||
178 |
val EXPRESSION = "expression" |
|
62806 | 179 |
object Expression |
180 |
{ |
|
181 |
def unapply(markup: Markup): Option[String] = |
|
182 |
markup match { |
|
74782 | 183 |
case Markup(EXPRESSION, props) => Some(Kind.get(props)) |
62806 | 184 |
case _ => None |
185 |
} |
|
186 |
} |
|
58464 | 187 |
|
188 |
||
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
189 |
/* citation */ |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
190 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
191 |
val CITATION = "citation" |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
192 |
val Citation = new Markup_String(CITATION, NAME) |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
193 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
194 |
|
55550 | 195 |
/* embedded languages */ |
196 |
||
55666 | 197 |
val Symbols = new Properties.Boolean("symbols") |
198 |
val Antiquotes = new Properties.Boolean("antiquotes") |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
199 |
val Delimited = new Properties.Boolean("delimited") |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
200 |
|
55550 | 201 |
val LANGUAGE = "language" |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
202 |
object Language |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
203 |
{ |
67336 | 204 |
val DOCUMENT = "document" |
55616 | 205 |
val ML = "ML" |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
206 |
val SML = "SML" |
56843
b2bfcd8cda80
support for path completion based on file-system content;
wenzelm
parents:
56743
diff
changeset
|
207 |
val PATH = "path" |
55616 | 208 |
val UNKNOWN = "unknown" |
209 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
210 |
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
|
211 |
markup match { |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
212 |
case Markup(LANGUAGE, props) => |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
213 |
(props, props, props, props) match { |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
214 |
case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) => |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
215 |
Some((name, symbols, antiquotes, delimited)) |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
216 |
case _ => None |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
217 |
} |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
218 |
case _ => None |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
219 |
} |
72842
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
220 |
|
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
221 |
object Path |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
222 |
{ |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
223 |
def unapply(markup: Markup): Option[Boolean] = |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
224 |
markup match { |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
225 |
case Language(PATH, _, _, delimited) => Some(delimited) |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
226 |
case _ => None |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
227 |
} |
6aae62f55c2b
clarified markup: support more completion, e.g. within ROOTS;
wenzelm
parents:
72782
diff
changeset
|
228 |
} |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
229 |
} |
55550 | 230 |
|
231 |
||
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
232 |
/* external resources */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
233 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
234 |
val PATH = "path" |
55551 | 235 |
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
|
236 |
|
70016 | 237 |
val EXPORT_PATH = "export_path" |
238 |
val Export_Path = new Markup_String(EXPORT_PATH, NAME) |
|
239 |
||
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
240 |
val URL = "url" |
55551 | 241 |
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
|
242 |
|
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
243 |
val DOC = "doc" |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
244 |
val Doc = new Markup_String(DOC, NAME) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
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 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
247 |
/* pretty printing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
248 |
|
61864 | 249 |
val Consistent = new Properties.Boolean("consistent") |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
250 |
val Indent = new Properties.Int("indent") |
61864 | 251 |
val Width = new Properties.Int("width") |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
252 |
|
61864 | 253 |
object Block |
254 |
{ |
|
255 |
val name = "block" |
|
256 |
def apply(c: Boolean, i: Int): Markup = |
|
257 |
Markup(name, |
|
258 |
(if (c) Consistent(c) else Nil) ::: |
|
259 |
(if (i != 0) Indent(i) else Nil)) |
|
260 |
def unapply(markup: Markup): Option[(Boolean, Int)] = |
|
261 |
if (markup.name == name) { |
|
74782 | 262 |
val c = Consistent.get(markup.properties) |
263 |
val i = Indent.get(markup.properties) |
|
61864 | 264 |
Some((c, i)) |
265 |
} |
|
266 |
else None |
|
267 |
} |
|
268 |
||
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
269 |
object Break |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
270 |
{ |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
271 |
val name = "break" |
61864 | 272 |
def apply(w: Int, i: Int): Markup = |
273 |
Markup(name, |
|
274 |
(if (w != 0) Width(w) else Nil) ::: |
|
275 |
(if (i != 0) Indent(i) else Nil)) |
|
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
276 |
def unapply(markup: Markup): Option[(Int, Int)] = |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
277 |
if (markup.name == name) { |
74782 | 278 |
val w = Width.get(markup.properties) |
279 |
val i = Indent.get(markup.properties) |
|
61864 | 280 |
Some((w, i)) |
61862
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
281 |
} |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
282 |
else None |
e2a9e46ac0fb
support pretty break indent, like underlying ML systems;
wenzelm
parents:
61660
diff
changeset
|
283 |
} |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
284 |
|
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
|
285 |
val ITEM = "item" |
51574
2b58d7b139d6
ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents:
51570
diff
changeset
|
286 |
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
|
287 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
288 |
val SEPARATOR = "separator" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
289 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
290 |
|
56548 | 291 |
/* text properties */ |
292 |
||
293 |
val WORDS = "words" |
|
50201
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 HIDDEN = "hidden" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
296 |
|
68298
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68148
diff
changeset
|
297 |
val DELETE = "delete" |
2c3ce27cf4a8
markup for deleted fragments of token source (NB: quoted tokens transform "\123" implicitly);
wenzelm
parents:
68148
diff
changeset
|
298 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
299 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57595
diff
changeset
|
300 |
/* misc entities */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
301 |
|
74112 | 302 |
val SESSION = "session" |
303 |
||
72781 | 304 |
val THEORY = "theory" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
305 |
val CLASS = "class" |
74112 | 306 |
val LOCALE = "locale" |
74261
d28a51dd9da6
export other entities, e.g. relevant for formal document output;
wenzelm
parents:
74182
diff
changeset
|
307 |
val BUNDLE = "bundle" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
308 |
val TYPE_NAME = "type_name" |
74112 | 309 |
val CONSTANT = "constant" |
310 |
val AXIOM = "axiom" |
|
311 |
val FACT = "fact" |
|
312 |
val ORACLE = "oracle" |
|
313 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
314 |
val FIXED = "fixed" |
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53055
diff
changeset
|
315 |
val CASE = "case" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
316 |
val DYNAMIC_FACT = "dynamic_fact" |
74112 | 317 |
val LITERAL_FACT = "literal_fact" |
318 |
||
319 |
val ATTRIBUTE = "attribute" |
|
320 |
val METHOD = "method" |
|
321 |
val METHOD_MODIFIER = "method_modifier" |
|
50201
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 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
324 |
/* inner syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
325 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
326 |
val TFREE = "tfree" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
327 |
val TVAR = "tvar" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
328 |
val FREE = "free" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
329 |
val SKOLEM = "skolem" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
330 |
val BOUND = "bound" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
331 |
val VAR = "var" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
332 |
val NUMERAL = "numeral" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
333 |
val LITERAL = "literal" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
334 |
val DELIMITER = "delimiter" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
335 |
val INNER_STRING = "inner_string" |
55033 | 336 |
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
|
337 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
338 |
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
|
339 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
340 |
val SORTING = "sorting" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
341 |
val TYPING = "typing" |
63347 | 342 |
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
|
343 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
344 |
|
55550 | 345 |
/* antiquotations */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
346 |
|
55526 | 347 |
val ANTIQUOTED = "antiquoted" |
348 |
val ANTIQUOTE = "antiquote" |
|
349 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
350 |
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
|
351 |
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
|
352 |
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
|
353 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
354 |
|
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
355 |
/* document text */ |
69965
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
356 |
|
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
357 |
val RAW_TEXT = "raw_text" |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
358 |
val PLAIN_TEXT = "plain_text" |
da5e7278286b
more markup for various text kinds, notably for nested formal comments;
wenzelm
parents:
69962
diff
changeset
|
359 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
360 |
val PARAGRAPH = "paragraph" |
50545
00bdc48c5f71
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents:
50543
diff
changeset
|
361 |
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
|
362 |
|
74782 | 363 |
object Document_Tag extends Markup_String("document_tag", NAME) |
70135
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
364 |
{ |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
365 |
val IMPORTANT = "important" |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
366 |
val UNIMPORTANT = "unimportant" |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
367 |
} |
ad6d4a14adb5
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
wenzelm
parents:
70016
diff
changeset
|
368 |
|
74784
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74783
diff
changeset
|
369 |
|
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74783
diff
changeset
|
370 |
/* LaTeX */ |
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74783
diff
changeset
|
371 |
|
74783 | 372 |
val Document_Latex = new Markup_Elem("document_latex") |
73780
466fae6bf22e
compose Latex text as XML, output exported YXML in Isabelle/Scala;
wenzelm
parents:
73556
diff
changeset
|
373 |
|
74784
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74783
diff
changeset
|
374 |
val Latex_Output = new Markup_Elem("latex_output") |
74790 | 375 |
val Latex_Macro0 = new Markup_String("latex_macro0", NAME) |
376 |
val Latex_Macro = new Markup_String("latex_macro", NAME) |
|
377 |
val Latex_Environment = new Markup_String("latex_environment", NAME) |
|
74823 | 378 |
val Latex_Heading = new Markup_String("latex_heading", KIND) |
379 |
val Latex_Body = new Markup_String("latex_body", KIND) |
|
74826
0e4d8aa61ad7
more symbolic latex_output via XML (using YXML within text);
wenzelm
parents:
74823
diff
changeset
|
380 |
val Latex_Delim = new Markup_String("latex_delim", NAME) |
0e4d8aa61ad7
more symbolic latex_output via XML (using YXML within text);
wenzelm
parents:
74823
diff
changeset
|
381 |
val Latex_Tag = new Markup_String("latex_tag", NAME) |
0e4d8aa61ad7
more symbolic latex_output via XML (using YXML within text);
wenzelm
parents:
74823
diff
changeset
|
382 |
|
74786 | 383 |
val Latex_Index_Item = new Markup_Elem("latex_index_item") |
384 |
val Latex_Index_Entry = new Markup_String("latex_index_entry", KIND) |
|
74784
d2522bb4db1b
symbolic latex_output via XML, interpreted in Isabelle/Scala;
wenzelm
parents:
74783
diff
changeset
|
385 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
386 |
|
61449 | 387 |
/* Markdown document structure */ |
388 |
||
389 |
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
|
390 |
val MARKDOWN_ITEM = "markdown_item" |
67336 | 391 |
val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth") |
61449 | 392 |
val Markdown_List = new Markup_String("markdown_list", "kind") |
67336 | 393 |
|
394 |
val ITEMIZE = "itemize" |
|
395 |
val ENUMERATE = "enumerate" |
|
396 |
val DESCRIPTION = "description" |
|
61449 | 397 |
|
398 |
||
60744 | 399 |
/* ML */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
400 |
|
55505 | 401 |
val ML_KEYWORD1 = "ML_keyword1" |
402 |
val ML_KEYWORD2 = "ML_keyword2" |
|
403 |
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
|
404 |
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
|
405 |
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
|
406 |
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
|
407 |
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
|
408 |
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
|
409 |
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
|
410 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
411 |
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
|
412 |
val ML_OPEN = "ML_open" |
55837 | 413 |
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
|
414 |
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
|
415 |
|
60744 | 416 |
val ML_BREAKPOINT = "ML_breakpoint" |
417 |
||
50201
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 |
/* outer syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
420 |
|
74673 | 421 |
val COMMAND_SPAN = "command_span" |
422 |
val Command_Span = new Markup_String(COMMAND_SPAN, NAME) |
|
423 |
||
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
424 |
val COMMAND = "command" |
66044 | 425 |
val KEYWORD = "keyword" |
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
426 |
val KEYWORD1 = "keyword1" |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
427 |
val KEYWORD2 = "keyword2" |
55765 | 428 |
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
|
429 |
val QUASI_KEYWORD = "quasi_keyword" |
56202 | 430 |
val IMPROPER = "improper" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
431 |
val OPERATOR = "operator" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
432 |
val STRING = "string" |
59081 | 433 |
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
|
434 |
val VERBATIM = "verbatim" |
55033 | 435 |
val CARTOUCHE = "cartouche" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
436 |
val COMMENT = "comment" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
437 |
|
72782 | 438 |
val LOAD_COMMAND = "load_command" |
439 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
440 |
|
69320 | 441 |
/* comments */ |
442 |
||
443 |
val COMMENT1 = "comment1" |
|
444 |
val COMMENT2 = "comment2" |
|
445 |
val COMMENT3 = "comment3" |
|
446 |
||
447 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
448 |
/* timing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
449 |
|
50781 | 450 |
val Elapsed = new Properties.Double("elapsed") |
451 |
val CPU = new Properties.Double("cpu") |
|
452 |
val GC = new Properties.Double("gc") |
|
453 |
||
454 |
object Timing_Properties |
|
455 |
{ |
|
456 |
def apply(timing: isabelle.Timing): Properties.T = |
|
457 |
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
|
458 |
|
50781 | 459 |
def unapply(props: Properties.T): Option[isabelle.Timing] = |
460 |
(props, props, props) match { |
|
461 |
case (Elapsed(elapsed), CPU(cpu), GC(gc)) => |
|
462 |
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) |
|
463 |
case _ => None |
|
464 |
} |
|
72013 | 465 |
|
74782 | 466 |
def get(props: Properties.T): isabelle.Timing = |
467 |
unapply(props).getOrElse(isabelle.Timing.zero) |
|
50781 | 468 |
} |
469 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
470 |
val TIMING = "timing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
471 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
472 |
object Timing |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
473 |
{ |
50781 | 474 |
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
|
475 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
476 |
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
|
477 |
markup match { |
50781 | 478 |
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
|
479 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
480 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
481 |
} |
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 |
|
65317 | 484 |
/* process result */ |
485 |
||
486 |
val Return_Code = new Properties.Int("return_code") |
|
487 |
||
488 |
object Process_Result |
|
489 |
{ |
|
490 |
def apply(result: Process_Result): Properties.T = |
|
491 |
Return_Code(result.rc) ::: |
|
492 |
(if (result.timing.is_zero) Nil else Timing_Properties(result.timing)) |
|
493 |
||
494 |
def unapply(props: Properties.T): Option[Process_Result] = |
|
495 |
props match { |
|
496 |
case Return_Code(rc) => |
|
497 |
val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero) |
|
498 |
Some(isabelle.Process_Result(rc, timing = timing)) |
|
499 |
case _ => None |
|
500 |
} |
|
501 |
} |
|
502 |
||
503 |
||
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
504 |
/* command indentation */ |
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
505 |
|
74782 | 506 |
val Command_Indent = new Markup_Int("command_indent", Indent.name) |
63474
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
507 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
508 |
|
f66e3c3b0fb1
semantic indentation for unstructured proof scripts;
wenzelm
parents:
63347
diff
changeset
|
509 |
/* goals */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
510 |
|
50543 | 511 |
val GOAL = "goal" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
512 |
val SUBGOAL = "subgoal" |
50215 | 513 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset
|
514 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
515 |
/* command status */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
516 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
517 |
val TASK = "task" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
518 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
519 |
val ACCEPTED = "accepted" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
520 |
val FORKED = "forked" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
521 |
val JOINED = "joined" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
522 |
val RUNNING = "running" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
523 |
val FINISHED = "finished" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
524 |
val FAILED = "failed" |
68871
f5c76072db55
more explicit status for "canceled" command within theory node;
wenzelm
parents:
68822
diff
changeset
|
525 |
val CANCELED = "canceled" |
68323 | 526 |
val INITIALIZED = "initialized" |
68884
9b97d0b20d95
clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents:
68871
diff
changeset
|
527 |
val FINALIZED = "finalized" |
70780
034742453594
more robust: avoid update/interrupt of long-running print_consolidation;
wenzelm
parents:
70665
diff
changeset
|
528 |
val CONSOLIDATING = "consolidating" |
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
|
529 |
val CONSOLIDATED = "consolidated" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
530 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
531 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
532 |
/* interactive documents */ |
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 |
val VERSION = "version" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
535 |
val ASSIGN = "assign" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
536 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
537 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
538 |
/* prover process */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
539 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
540 |
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
|
541 |
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
|
542 |
|
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 |
/* messages */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
545 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
546 |
val INIT = "init" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
547 |
val STATUS = "status" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
548 |
val REPORT = "report" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
549 |
val RESULT = "result" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
550 |
val WRITELN = "writeln" |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
551 |
val STATE = "state" |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
552 |
val INFORMATION = "information" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
553 |
val TRACING = "tracing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
554 |
val WARNING = "warning" |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
555 |
val LEGACY = "legacy" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
556 |
val ERROR = "error" |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68323
diff
changeset
|
557 |
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
|
558 |
val PROTOCOL = "protocol" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
559 |
val SYSTEM = "system" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
560 |
val STDOUT = "stdout" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
561 |
val STDERR = "stderr" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
562 |
val EXIT = "exit" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
563 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
564 |
val WRITELN_MESSAGE = "writeln_message" |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
565 |
val STATE_MESSAGE = "state_message" |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
566 |
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
|
567 |
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
|
568 |
val WARNING_MESSAGE = "warning_message" |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
569 |
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
|
570 |
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
|
571 |
|
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
572 |
val messages = Map( |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
573 |
WRITELN -> WRITELN_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
574 |
STATE -> STATE_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
575 |
INFORMATION -> INFORMATION_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
576 |
TRACING -> TRACING_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
577 |
WARNING -> WARNING_MESSAGE, |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
578 |
LEGACY -> LEGACY_MESSAGE, |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
579 |
ERROR -> ERROR_MESSAGE) |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
580 |
|
52876 | 581 |
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
|
582 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
583 |
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
|
584 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
585 |
val BAD = "bad" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
586 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
587 |
val INTENSIFY = "intensify" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
588 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
589 |
|
73835 | 590 |
/* ML profiling */ |
591 |
||
592 |
val COUNT = "count" |
|
593 |
val ML_PROFILING_ENTRY = "ML_profiling_entry" |
|
594 |
val ML_PROFILING = "ML_profiling" |
|
595 |
||
596 |
object ML_Profiling |
|
597 |
{ |
|
598 |
def unapply_entry(tree: XML.Tree): Option[isabelle.ML_Profiling.Entry] = |
|
599 |
tree match { |
|
600 |
case XML.Elem(Markup(ML_PROFILING_ENTRY, List((NAME, name), (COUNT, Value.Long(count)))), _) => |
|
601 |
Some(isabelle.ML_Profiling.Entry(name, count)) |
|
602 |
case _ => None |
|
603 |
} |
|
604 |
||
605 |
def unapply_report(tree: XML.Tree): Option[isabelle.ML_Profiling.Report] = |
|
606 |
tree match { |
|
607 |
case XML.Elem(Markup(ML_PROFILING, List((KIND, kind))), body) => |
|
608 |
Some(isabelle.ML_Profiling.Report(kind, body.flatMap(unapply_entry))) |
|
609 |
case _ => None |
|
610 |
} |
|
611 |
} |
|
612 |
||
613 |
||
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
614 |
/* active areas */ |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
615 |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50545
diff
changeset
|
616 |
val BROWSER = "browser" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
617 |
val GRAPHVIEW = "graphview" |
69650 | 618 |
val THEORY_EXPORTS = "theory_exports" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
619 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
620 |
val SENDBACK = "sendback" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
621 |
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
|
622 |
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
|
623 |
val PADDING_COMMAND = (PADDING, "command") |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
624 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
625 |
val DIALOG = "dialog" |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50501
diff
changeset
|
626 |
val Result = new Properties.String(RESULT) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
627 |
|
63681 | 628 |
val JEDIT_ACTION = "jedit_action" |
629 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
630 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
631 |
/* protocol message functions */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
632 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
633 |
val FUNCTION = "function" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
634 |
|
71673 | 635 |
class Function(val name: String) |
636 |
{ |
|
637 |
val PROPERTY: Properties.Entry = (FUNCTION, name) |
|
638 |
} |
|
66942
91a21a5631ae
proper order of initialization (amending 9953ae603a23);
wenzelm
parents:
66873
diff
changeset
|
639 |
|
71673 | 640 |
class Properties_Function(name: String) extends Function(name) |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
641 |
{ |
71673 | 642 |
def unapply(props: Properties.T): Option[Properties.T] = |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
643 |
props match { |
71673 | 644 |
case PROPERTY :: args => Some(args) |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
645 |
case _ => None |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
646 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
647 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
648 |
|
71673 | 649 |
class Name_Function(name: String) extends Function(name) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
650 |
{ |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72107
diff
changeset
|
651 |
def unapply(props: Properties.T): Option[String] = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
652 |
props match { |
71673 | 653 |
case List(PROPERTY, (NAME, a)) => Some(a) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
654 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
655 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
656 |
} |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
657 |
|
72116 | 658 |
object ML_Statistics extends Function("ML_statistics") |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72107
diff
changeset
|
659 |
{ |
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72116
diff
changeset
|
660 |
def unapply(props: Properties.T): Option[(Long, String)] = |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72107
diff
changeset
|
661 |
props match { |
72119
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72116
diff
changeset
|
662 |
case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) => |
d115d50a19c0
provide POLYSTATSDIR to keep $HOME/.polyml clean (requires Poly/ML 52881757b127, otherwise ignored);
wenzelm
parents:
72116
diff
changeset
|
663 |
Some((pid, stats_dir)) |
72112
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72107
diff
changeset
|
664 |
case _ => None |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72107
diff
changeset
|
665 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72107
diff
changeset
|
666 |
} |
3546dd4ade74
ML statistics via external process: allows monitoring RTS while ML program sleeps;
wenzelm
parents:
72107
diff
changeset
|
667 |
|
72107
1b06ed254943
more compact command_timings, as in former batch-build;
wenzelm
parents:
72013
diff
changeset
|
668 |
val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name) |
72711 | 669 |
def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1) |
72107
1b06ed254943
more compact command_timings, as in former batch-build;
wenzelm
parents:
72013
diff
changeset
|
670 |
|
71673 | 671 |
object Command_Timing extends Properties_Function("command_timing") |
672 |
object Theory_Timing extends Properties_Function("theory_timing") |
|
72002
5c4800f6b25a
more robust protocol for "Timing ..." messages, notably for pide_session=true;
wenzelm
parents:
71673
diff
changeset
|
673 |
object Session_Timing extends Properties_Function("session_timing") |
72008
7a53fc156c2b
proper session Timing for build_history log file (see 5c4800f6b25a);
wenzelm
parents:
72002
diff
changeset
|
674 |
{ |
72013 | 675 |
val Threads = new Properties.Int("threads") |
72008
7a53fc156c2b
proper session Timing for build_history log file (see 5c4800f6b25a);
wenzelm
parents:
72002
diff
changeset
|
676 |
} |
71673 | 677 |
object Task_Statistics extends Properties_Function("task_statistics") |
678 |
||
72692
22aeec526ffd
support for PIDE markup in batch build (inactive due to pide_reports=false);
wenzelm
parents:
72332
diff
changeset
|
679 |
object Loading_Theory extends Properties_Function("loading_theory") |
71673 | 680 |
object Build_Session_Finished extends Function("build_session_finished") |
681 |
||
682 |
object Commands_Accepted extends Function("commands_accepted") |
|
683 |
object Assign_Update extends Function("assign_update") |
|
684 |
object Removed_Versions extends Function("removed_versions") |
|
685 |
||
686 |
object Invoke_Scala extends Function("invoke_scala") |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
687 |
{ |
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
73360
diff
changeset
|
688 |
def unapply(props: Properties.T): Option[(String, String)] = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
689 |
props match { |
73419
22f3f2117ed7
clarified signature: function_thread is determined in Isabelle/Scala, not Isabelle/ML;
wenzelm
parents:
73360
diff
changeset
|
690 |
case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id)) |
50255 | 691 |
case _ => None |
692 |
} |
|
693 |
} |
|
50975 | 694 |
|
71673 | 695 |
object Cancel_Scala extends Function("cancel_scala") |
50975 | 696 |
{ |
71673 | 697 |
def unapply(props: Properties.T): Option[String] = |
50975 | 698 |
props match { |
71673 | 699 |
case List(PROPERTY, (ID, id)) => Some(id) |
50975 | 700 |
case _ => None |
701 |
} |
|
702 |
} |
|
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
|
703 |
|
69788 | 704 |
val PRINT_OPERATIONS = "print_operations" |
705 |
||
706 |
||
707 |
/* export */ |
|
708 |
||
68088 | 709 |
val EXPORT = "export" |
71624 | 710 |
val THEORY_NAME = "theory_name" |
711 |
val EXECUTABLE = "executable" |
|
712 |
val COMPRESS = "compress" |
|
713 |
val STRICT = "strict" |
|
68088 | 714 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
715 |
|
60830 | 716 |
/* debugger output */ |
717 |
||
60842 | 718 |
val DEBUGGER_STATE = "debugger_state" |
719 |
object Debugger_State |
|
720 |
{ |
|
721 |
def unapply(props: Properties.T): Option[String] = |
|
722 |
props match { |
|
723 |
case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name) |
|
724 |
case _ => None |
|
725 |
} |
|
726 |
} |
|
727 |
||
60830 | 728 |
val DEBUGGER_OUTPUT = "debugger_output" |
729 |
object Debugger_Output |
|
730 |
{ |
|
60834 | 731 |
def unapply(props: Properties.T): Option[String] = |
60830 | 732 |
props match { |
60834 | 733 |
case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name) |
60830 | 734 |
case _ => None |
735 |
} |
|
736 |
} |
|
737 |
||
738 |
||
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
|
739 |
/* 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
|
740 |
|
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
741 |
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
|
742 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
743 |
val SIMP_TRACE_LOG = "simp_trace_log" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
744 |
val SIMP_TRACE_STEP = "simp_trace_step" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
745 |
val SIMP_TRACE_RECURSE = "simp_trace_recurse" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
746 |
val SIMP_TRACE_HINT = "simp_trace_hint" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
747 |
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
|
748 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
749 |
val SIMP_TRACE_CANCEL = "simp_trace_cancel" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
750 |
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
|
751 |
{ |
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
|
752 |
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
|
753 |
props match { |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
754 |
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
|
755 |
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
|
756 |
} |
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
|
757 |
} |
65335 | 758 |
|
759 |
||
760 |
/* XML data representation */ |
|
761 |
||
762 |
def encode: XML.Encode.T[Markup] = (markup: Markup) => |
|
763 |
{ |
|
764 |
import XML.Encode._ |
|
765 |
pair(string, properties)((markup.name, markup.properties)) |
|
766 |
} |
|
767 |
||
768 |
def decode: XML.Decode.T[Markup] = (body: XML.Body) => |
|
769 |
{ |
|
770 |
import XML.Decode._ |
|
771 |
val (name, props) = pair(string, properties)(body) |
|
772 |
Markup(name, props) |
|
773 |
} |
|
45666 | 774 |
} |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
775 |
|
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
776 |
|
45666 | 777 |
sealed case class Markup(name: String, properties: Properties.T) |
59707 | 778 |
{ |
73556
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73419
diff
changeset
|
779 |
def is_empty: Boolean = name.isEmpty |
192bcee4f8b8
more robust treatment of empty markup: it allows to produce formal chunks;
wenzelm
parents:
73419
diff
changeset
|
780 |
|
59707 | 781 |
def markup(s: String): String = |
782 |
YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) |
|
64358 | 783 |
|
784 |
def update_properties(more_props: Properties.T): Markup = |
|
785 |
if (more_props.isEmpty) this |
|
73360 | 786 |
else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) }) |
65753 | 787 |
|
788 |
def + (entry: Properties.Entry): Markup = |
|
789 |
Markup(name, Properties.put(properties, entry)) |
|
59707 | 790 |
} |