author | wenzelm |
Fri, 13 Nov 2015 19:59:28 +0100 | |
changeset 61660 | 78b371644654 |
parent 61598 | ed4dad8823a4 |
child 61862 | e2a9e46ac0fb |
permissions | -rw-r--r-- |
45670 | 1 |
/* Title: Pure/PIDE/markup.scala |
45673
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents:
45670
diff
changeset
|
2 |
Module: PIDE |
27958 | 3 |
Author: Makarius |
4 |
||
56743 | 5 |
Quasi-abstract markup elements. |
27958 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
27970 | 10 |
|
32450 | 11 |
object Markup |
12 |
{ |
|
56743 | 13 |
/* elements */ |
14 |
||
15 |
object Elements |
|
16 |
{ |
|
17 |
def apply(elems: Set[String]): Elements = new Elements(elems) |
|
18 |
def apply(elems: String*): Elements = apply(Set(elems: _*)) |
|
19 |
val empty: Elements = apply() |
|
20 |
val full: Elements = |
|
21 |
new Elements(Set.empty) |
|
22 |
{ |
|
23 |
override def apply(elem: String): Boolean = true |
|
24 |
override def toString: String = "Elements.full" |
|
25 |
} |
|
26 |
} |
|
27 |
||
28 |
sealed class Elements private[Markup](private val rep: Set[String]) |
|
29 |
{ |
|
30 |
def apply(elem: String): Boolean = rep.contains(elem) |
|
31 |
def + (elem: String): Elements = new Elements(rep + elem) |
|
32 |
def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep) |
|
33 |
override def toString: String = rep.mkString("Elements(", ",", ")") |
|
34 |
} |
|
35 |
||
36 |
||
45666 | 37 |
/* properties */ |
29184 | 38 |
|
39 |
val NAME = "name" |
|
43780 | 40 |
val Name = new Properties.String(NAME) |
42136 | 41 |
|
29184 | 42 |
val KIND = "kind" |
43780 | 43 |
val Kind = new Properties.String(KIND) |
29184 | 44 |
|
60744 | 45 |
val SERIAL = "serial" |
46 |
val Serial = new Properties.Long(SERIAL) |
|
47 |
||
52854
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
48 |
val INSTANCE = "instance" |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
49 |
val Instance = new Properties.String(INSTANCE) |
92932931bd82
more general Output.result: allow to update arbitrary properties;
wenzelm
parents:
52800
diff
changeset
|
50 |
|
29184 | 51 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
52 |
/* basic markup */ |
29184 | 53 |
|
45666 | 54 |
val Empty = Markup("", Nil) |
55 |
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
|
56 |
|
55551 | 57 |
class Markup_String(val name: String, prop: String) |
58 |
{ |
|
59 |
private val Prop = new Properties.String(prop) |
|
60 |
||
61 |
def apply(s: String): Markup = Markup(name, Prop(s)) |
|
62 |
def unapply(markup: Markup): Option[String] = |
|
63 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
64 |
} |
|
65 |
||
66 |
class Markup_Int(val name: String, prop: String) |
|
67 |
{ |
|
68 |
private val Prop = new Properties.Int(prop) |
|
69 |
||
70 |
def apply(i: Int): Markup = Markup(name, Prop(i)) |
|
71 |
def unapply(markup: Markup): Option[Int] = |
|
72 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
73 |
} |
|
74 |
||
60744 | 75 |
class Markup_Long(val name: String, prop: String) |
76 |
{ |
|
77 |
private val Prop = new Properties.Long(prop) |
|
78 |
||
79 |
def apply(i: Long): Markup = Markup(name, Prop(i)) |
|
80 |
def unapply(markup: Markup): Option[Long] = |
|
81 |
if (markup.name == name) Prop.unapply(markup.properties) else None |
|
82 |
} |
|
83 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
84 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
85 |
/* formal entities */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
86 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
87 |
val BINDING = "binding" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
88 |
val ENTITY = "entity" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
89 |
val DEF = "def" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
90 |
val REF = "ref" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
91 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
92 |
object Entity |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
93 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
94 |
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
|
95 |
markup match { |
55551 | 96 |
case Markup(ENTITY, props) => |
97 |
(props, props) match { |
|
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
98 |
case (Kind(kind), Name(name)) => Some((kind, name)) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
99 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
100 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
101 |
case _ => None |
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 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
104 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
105 |
|
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
106 |
/* completion */ |
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
107 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
108 |
val COMPLETION = "completion" |
55914
c5b752d549e3
clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents:
55837
diff
changeset
|
109 |
val NO_COMPLETION = "no_completion" |
55672
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
diff
changeset
|
110 |
|
5e25cc741ab9
support for completion within the formal context;
wenzelm
parents:
55666
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 |
/* position */ |
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 LINE = "line" |
58978
e42da880c61e
more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents:
58853
diff
changeset
|
115 |
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
|
116 |
val OFFSET = "offset" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
117 |
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
|
118 |
val FILE = "file" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
119 |
val ID = "id" |
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 |
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
|
122 |
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
|
123 |
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
|
124 |
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
|
125 |
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
|
126 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
127 |
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
|
128 |
val POSITION = "position" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
129 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
130 |
|
58464 | 131 |
/* expression */ |
132 |
||
133 |
val EXPRESSION = "expression" |
|
134 |
||
135 |
||
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
136 |
/* citation */ |
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
137 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
138 |
val CITATION = "citation" |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
58544
diff
changeset
|
139 |
val Citation = new Markup_String(CITATION, NAME) |
58544
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
140 |
|
340f130b3d38
bibtex support in ML: document antiquotation @{cite} with markup;
wenzelm
parents:
58464
diff
changeset
|
141 |
|
55550 | 142 |
/* embedded languages */ |
143 |
||
55666 | 144 |
val Symbols = new Properties.Boolean("symbols") |
145 |
val Antiquotes = new Properties.Boolean("antiquotes") |
|
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
146 |
val Delimited = new Properties.Boolean("delimited") |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
147 |
|
55550 | 148 |
val LANGUAGE = "language" |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
149 |
object Language |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
150 |
{ |
55616 | 151 |
val ML = "ML" |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
152 |
val SML = "SML" |
56843
b2bfcd8cda80
support for path completion based on file-system content;
wenzelm
parents:
56743
diff
changeset
|
153 |
val PATH = "path" |
55616 | 154 |
val UNKNOWN = "unknown" |
155 |
||
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
156 |
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
|
157 |
markup match { |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
158 |
case Markup(LANGUAGE, props) => |
55828
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
159 |
(props, props, props, props) match { |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
160 |
case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) => |
42ac3cfb89f6
clarified language markup: added "delimited" property;
wenzelm
parents:
55765
diff
changeset
|
161 |
Some((name, symbols, antiquotes, delimited)) |
55615
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
162 |
case _ => None |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
163 |
} |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
164 |
case _ => None |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
165 |
} |
bf4bbe72f740
completion of keywords and symbols based on language context;
wenzelm
parents:
55553
diff
changeset
|
166 |
} |
55550 | 167 |
|
168 |
||
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
169 |
/* external resources */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
170 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
171 |
val PATH = "path" |
55551 | 172 |
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
|
173 |
|
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
53378
diff
changeset
|
174 |
val URL = "url" |
55551 | 175 |
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
|
176 |
|
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
177 |
val DOC = "doc" |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
178 |
val Doc = new Markup_String(DOC, NAME) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61598
diff
changeset
|
179 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
180 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
181 |
/* pretty printing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
182 |
|
55551 | 183 |
val Block = new Markup_Int("block", "indent") |
184 |
val Break = new Markup_Int("break", "width") |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
185 |
|
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
|
186 |
val ITEM = "item" |
51574
2b58d7b139d6
ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents:
51570
diff
changeset
|
187 |
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
|
188 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
189 |
val SEPARATOR = "separator" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
190 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
191 |
|
56548 | 192 |
/* text properties */ |
193 |
||
194 |
val WORDS = "words" |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
195 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
196 |
val HIDDEN = "hidden" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
197 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
198 |
|
58048
aa6296d09e0e
more explicit Method.modifier with reported position;
wenzelm
parents:
57595
diff
changeset
|
199 |
/* misc entities */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
200 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
201 |
val CLASS = "class" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
202 |
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
|
203 |
val FIXED = "fixed" |
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53055
diff
changeset
|
204 |
val CASE = "case" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
205 |
val CONSTANT = "constant" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
206 |
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
|
207 |
|
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 |
/* inner syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
210 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
211 |
val TFREE = "tfree" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
212 |
val TVAR = "tvar" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
213 |
val FREE = "free" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
214 |
val SKOLEM = "skolem" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
215 |
val BOUND = "bound" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
216 |
val VAR = "var" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
217 |
val NUMERAL = "numeral" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
218 |
val LITERAL = "literal" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
219 |
val DELIMITER = "delimiter" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
220 |
val INNER_STRING = "inner_string" |
55033 | 221 |
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
|
222 |
val INNER_COMMENT = "inner_comment" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
223 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
224 |
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
|
225 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
226 |
val SORTING = "sorting" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
227 |
val TYPING = "typing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
228 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
229 |
val ATTRIBUTE = "attribute" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
230 |
val METHOD = "method" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
231 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
232 |
|
55550 | 233 |
/* antiquotations */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
234 |
|
55526 | 235 |
val ANTIQUOTED = "antiquoted" |
236 |
val ANTIQUOTE = "antiquote" |
|
237 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
238 |
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
|
239 |
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
|
240 |
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
|
241 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
242 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
243 |
/* text structure */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
244 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
245 |
val PARAGRAPH = "paragraph" |
50545
00bdc48c5f71
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents:
50543
diff
changeset
|
246 |
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
|
247 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
248 |
|
61449 | 249 |
/* Markdown document structure */ |
250 |
||
251 |
val MARKDOWN_PARAGRAPH = "markdown_paragraph" |
|
252 |
val Markdown_List = new Markup_String("markdown_list", "kind") |
|
253 |
val Markdown_Item = new Markup_Int("markdown_item", "depth") |
|
254 |
||
255 |
||
60744 | 256 |
/* ML */ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
257 |
|
55505 | 258 |
val ML_KEYWORD1 = "ML_keyword1" |
259 |
val ML_KEYWORD2 = "ML_keyword2" |
|
260 |
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
|
261 |
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
|
262 |
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
|
263 |
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
|
264 |
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
|
265 |
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
|
266 |
val ML_COMMENT = "ML_comment" |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
267 |
val SML_STRING = "SML_string" |
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56202
diff
changeset
|
268 |
val SML_COMMENT = "SML_comment" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
269 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
270 |
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
|
271 |
val ML_OPEN = "ML_open" |
55837 | 272 |
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
|
273 |
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
|
274 |
|
60744 | 275 |
val ML_BREAKPOINT = "ML_breakpoint" |
276 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
277 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
278 |
/* outer syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
279 |
|
55744
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
280 |
val COMMAND = "command" |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
281 |
val KEYWORD1 = "keyword1" |
4a4e5686e091
clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind;
wenzelm
parents:
55694
diff
changeset
|
282 |
val KEYWORD2 = "keyword2" |
55765 | 283 |
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
|
284 |
val QUASI_KEYWORD = "quasi_keyword" |
56202 | 285 |
val IMPROPER = "improper" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
286 |
val OPERATOR = "operator" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
287 |
val STRING = "string" |
59081 | 288 |
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
|
289 |
val VERBATIM = "verbatim" |
55033 | 290 |
val CARTOUCHE = "cartouche" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
291 |
val COMMENT = "comment" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
292 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
293 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
294 |
/* timing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
295 |
|
50781 | 296 |
val Elapsed = new Properties.Double("elapsed") |
297 |
val CPU = new Properties.Double("cpu") |
|
298 |
val GC = new Properties.Double("gc") |
|
299 |
||
300 |
object Timing_Properties |
|
301 |
{ |
|
302 |
def apply(timing: isabelle.Timing): Properties.T = |
|
303 |
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
|
304 |
|
50781 | 305 |
def unapply(props: Properties.T): Option[isabelle.Timing] = |
306 |
(props, props, props) match { |
|
307 |
case (Elapsed(elapsed), CPU(cpu), GC(gc)) => |
|
308 |
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) |
|
309 |
case _ => None |
|
310 |
} |
|
311 |
} |
|
312 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
313 |
val TIMING = "timing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
314 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
315 |
object Timing |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
316 |
{ |
50781 | 317 |
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
|
318 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
319 |
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
|
320 |
markup match { |
50781 | 321 |
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
|
322 |
case _ => None |
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 |
} |
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 |
|
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
327 |
/* command timing */ |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
328 |
|
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51662
diff
changeset
|
329 |
val COMMAND_TIMING = "command_timing" |
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
330 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
331 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
332 |
/* toplevel */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
333 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
334 |
val SUBGOALS = "subgoals" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
335 |
val PROOF_STATE = "proof_state" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
336 |
|
50543 | 337 |
val GOAL = "goal" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
338 |
val SUBGOAL = "subgoal" |
50215 | 339 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset
|
340 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
341 |
/* command status */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
342 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
343 |
val TASK = "task" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
344 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
345 |
val ACCEPTED = "accepted" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
346 |
val FORKED = "forked" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
347 |
val JOINED = "joined" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
348 |
val RUNNING = "running" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
349 |
val FINISHED = "finished" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
350 |
val FAILED = "failed" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
351 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
352 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
353 |
/* interactive documents */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
354 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
355 |
val VERSION = "version" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
356 |
val ASSIGN = "assign" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
357 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
358 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
359 |
/* prover process */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
360 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
361 |
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
|
362 |
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
|
363 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
364 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
365 |
/* messages */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
366 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
367 |
val INIT = "init" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
368 |
val STATUS = "status" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
369 |
val REPORT = "report" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
370 |
val RESULT = "result" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
371 |
val WRITELN = "writeln" |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
372 |
val STATE = "state" |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
373 |
val INFORMATION = "information" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
374 |
val TRACING = "tracing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
375 |
val WARNING = "warning" |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
376 |
val LEGACY = "legacy" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
377 |
val ERROR = "error" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
378 |
val PROTOCOL = "protocol" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
379 |
val SYSTEM = "system" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
380 |
val STDOUT = "stdout" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
381 |
val STDERR = "stderr" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
382 |
val EXIT = "exit" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
383 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
384 |
val WRITELN_MESSAGE = "writeln_message" |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
385 |
val STATE_MESSAGE = "state_message" |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
386 |
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
|
387 |
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
|
388 |
val WARNING_MESSAGE = "warning_message" |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
389 |
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
|
390 |
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
|
391 |
|
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
392 |
val messages = Map( |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
393 |
WRITELN -> WRITELN_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
394 |
STATE -> STATE_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
395 |
INFORMATION -> INFORMATION_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
396 |
TRACING -> TRACING_MESSAGE, |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
397 |
WARNING -> WARNING_MESSAGE, |
59203
5f0bd5afc16d
explicit message channel for "legacy", which is nonetheless a variant of "warning";
wenzelm
parents:
59186
diff
changeset
|
398 |
LEGACY -> LEGACY_MESSAGE, |
59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
399 |
ERROR -> ERROR_MESSAGE) |
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59112
diff
changeset
|
400 |
|
52876 | 401 |
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
|
402 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
403 |
val Return_Code = new Properties.Int("return_code") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
404 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
405 |
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
|
406 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
407 |
val BAD = "bad" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
408 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
409 |
val INTENSIFY = "intensify" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
410 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
411 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
412 |
/* active areas */ |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
413 |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50545
diff
changeset
|
414 |
val BROWSER = "browser" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
415 |
val GRAPHVIEW = "graphview" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
416 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
417 |
val SENDBACK = "sendback" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
418 |
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
|
419 |
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
|
420 |
val PADDING_COMMAND = (PADDING, "command") |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
421 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
422 |
val DIALOG = "dialog" |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50501
diff
changeset
|
423 |
val Result = new Properties.String(RESULT) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
424 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
425 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
426 |
/* protocol message functions */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
427 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
428 |
val FUNCTION = "function" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
429 |
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
|
430 |
|
52563 | 431 |
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
|
432 |
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
|
433 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
434 |
object Protocol_Handler |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
435 |
{ |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
436 |
def unapply(props: Properties.T): Option[(String)] = |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
437 |
props match { |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
438 |
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
|
439 |
case _ => None |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
440 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
441 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
442 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
443 |
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
|
444 |
object Invoke_Scala |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
445 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
446 |
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
|
447 |
props match { |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
448 |
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
|
449 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
450 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
451 |
} |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
452 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
453 |
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
|
454 |
object Cancel_Scala |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
455 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
456 |
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
|
457 |
props match { |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
458 |
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
|
459 |
case _ => None |
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 |
} |
50255 | 462 |
|
463 |
object ML_Statistics |
|
464 |
{ |
|
465 |
def unapply(props: Properties.T): Option[Properties.T] = |
|
466 |
props match { |
|
467 |
case (FUNCTION, "ML_statistics") :: stats => Some(stats) |
|
468 |
case _ => None |
|
469 |
} |
|
470 |
} |
|
50975 | 471 |
|
472 |
object Task_Statistics |
|
473 |
{ |
|
474 |
def unapply(props: Properties.T): Option[Properties.T] = |
|
475 |
props match { |
|
476 |
case (FUNCTION, "task_statistics") :: stats => Some(stats) |
|
477 |
case _ => None |
|
478 |
} |
|
479 |
} |
|
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
|
480 |
|
59367 | 481 |
val LOADING_THEORY = "loading_theory" |
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
482 |
object Loading_Theory |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
483 |
{ |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
484 |
def unapply(props: Properties.T): Option[String] = |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
485 |
props match { |
59367 | 486 |
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
|
487 |
case _ => None |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
488 |
} |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
489 |
} |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
490 |
|
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset
|
491 |
val BUILD_THEORIES_RESULT = "build_theories_result" |
59364 | 492 |
object Build_Theories_Result |
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
493 |
{ |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59367
diff
changeset
|
494 |
def unapply(props: Properties.T): Option[String] = |
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
495 |
props match { |
60831 | 496 |
case List((FUNCTION, BUILD_THEORIES_RESULT), (ID, id)) => Some(id) |
56616
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
497 |
case _ => None |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
498 |
} |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
499 |
} |
abc2da18d08d
added protocol command "use_theories", with core functionality of batch build;
wenzelm
parents:
56548
diff
changeset
|
500 |
|
56864 | 501 |
val PRINT_OPERATIONS = "print_operations" |
502 |
||
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
503 |
|
60830 | 504 |
/* debugger output */ |
505 |
||
60842 | 506 |
val DEBUGGER_STATE = "debugger_state" |
507 |
object Debugger_State |
|
508 |
{ |
|
509 |
def unapply(props: Properties.T): Option[String] = |
|
510 |
props match { |
|
511 |
case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name) |
|
512 |
case _ => None |
|
513 |
} |
|
514 |
} |
|
515 |
||
60830 | 516 |
val DEBUGGER_OUTPUT = "debugger_output" |
517 |
object Debugger_Output |
|
518 |
{ |
|
60834 | 519 |
def unapply(props: Properties.T): Option[String] = |
60830 | 520 |
props match { |
60834 | 521 |
case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name) |
60830 | 522 |
case _ => None |
523 |
} |
|
524 |
} |
|
525 |
||
526 |
||
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
|
527 |
/* 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
|
528 |
|
57594
037f3b251df5
regular message to refer to Simplifier Trace panel (unused);
wenzelm
parents:
56864
diff
changeset
|
529 |
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
|
530 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
531 |
val SIMP_TRACE_LOG = "simp_trace_log" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
532 |
val SIMP_TRACE_STEP = "simp_trace_step" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
533 |
val SIMP_TRACE_RECURSE = "simp_trace_recurse" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
534 |
val SIMP_TRACE_HINT = "simp_trace_hint" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
535 |
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
|
536 |
|
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
537 |
val SIMP_TRACE_CANCEL = "simp_trace_cancel" |
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
538 |
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
|
539 |
{ |
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
|
540 |
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
|
541 |
props match { |
55553
99409ccbe04a
more standard names for protocol and markup elements;
wenzelm
parents:
55551
diff
changeset
|
542 |
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
|
543 |
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
|
544 |
} |
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
|
545 |
} |
45666 | 546 |
} |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
547 |
|
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
548 |
|
45666 | 549 |
sealed case class Markup(name: String, properties: Properties.T) |
59707 | 550 |
{ |
551 |
def markup(s: String): String = |
|
552 |
YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) |
|
553 |
} |