author | nipkow |
Fri, 21 Jun 2013 09:00:26 +0200 | |
changeset 52402 | c2f30ba4bb98 |
parent 52111 | 1fd184eaa310 |
child 52563 | f9a20c2c3b70 |
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 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
5 |
Isabelle-specific implementation of quasi-abstract markup elements. |
27958 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
27970 | 10 |
|
32450 | 11 |
object Markup |
12 |
{ |
|
45666 | 13 |
/* properties */ |
29184 | 14 |
|
15 |
val NAME = "name" |
|
43780 | 16 |
val Name = new Properties.String(NAME) |
42136 | 17 |
|
29184 | 18 |
val KIND = "kind" |
43780 | 19 |
val Kind = new Properties.String(KIND) |
29184 | 20 |
|
21 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
22 |
/* basic markup */ |
29184 | 23 |
|
45666 | 24 |
val Empty = Markup("", Nil) |
25 |
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
|
26 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
27 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
28 |
/* formal entities */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
29 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
30 |
val BINDING = "binding" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
31 |
val ENTITY = "entity" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
32 |
val DEF = "def" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
33 |
val REF = "ref" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
34 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
35 |
object Entity |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
36 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
37 |
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
|
38 |
markup match { |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
39 |
case Markup(ENTITY, props @ Kind(kind)) => |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
40 |
props match { |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
41 |
case Name(name) => Some(kind, name) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
42 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
43 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
44 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
45 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
46 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
47 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
48 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
49 |
/* position */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
50 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
51 |
val LINE = "line" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
52 |
val OFFSET = "offset" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
53 |
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
|
54 |
val FILE = "file" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
55 |
val ID = "id" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
56 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
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
|
61 |
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
|
62 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
63 |
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
|
64 |
val POSITION = "position" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
65 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
66 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
67 |
/* path */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
68 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
69 |
val PATH = "path" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
70 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
71 |
object Path |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
72 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
73 |
def unapply(markup: Markup): Option[String] = |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
74 |
markup match { |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
75 |
case Markup(PATH, Name(name)) => Some(name) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
76 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
77 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
78 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
79 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
80 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
81 |
/* pretty printing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
82 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
83 |
val Indent = new Properties.Int("indent") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
84 |
val BLOCK = "block" |
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
|
85 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
86 |
val Width = new Properties.Int("width") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
87 |
val BREAK = "break" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
88 |
|
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
|
89 |
val ITEM = "item" |
51574
2b58d7b139d6
ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents:
51570
diff
changeset
|
90 |
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
|
91 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
92 |
val SEPARATOR = "separator" |
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 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
95 |
/* hidden text */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
96 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
97 |
val HIDDEN = "hidden" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
98 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
99 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
100 |
/* logical entities */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
101 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
102 |
val CLASS = "class" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
103 |
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
|
104 |
val FIXED = "fixed" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
105 |
val CONSTANT = "constant" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
106 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
107 |
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
|
108 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
109 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
110 |
/* inner syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
111 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
112 |
val TFREE = "tfree" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
113 |
val TVAR = "tvar" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
114 |
val FREE = "free" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
115 |
val SKOLEM = "skolem" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
116 |
val BOUND = "bound" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
117 |
val VAR = "var" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
118 |
val NUMERAL = "numeral" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
119 |
val LITERAL = "literal" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
120 |
val DELIMITER = "delimiter" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
121 |
val INNER_STRING = "inner_string" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
122 |
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
|
123 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
124 |
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
|
125 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
126 |
val SORT = "sort" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
127 |
val TYP = "typ" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
128 |
val TERM = "term" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
129 |
val PROP = "prop" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
130 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
131 |
val SORTING = "sorting" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
132 |
val TYPING = "typing" |
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 |
val ATTRIBUTE = "attribute" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
135 |
val METHOD = "method" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
136 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
137 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
138 |
/* embedded source text */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
139 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
140 |
val ML_SOURCE = "ML_source" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
141 |
val DOCUMENT_SOURCE = "document_source" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
142 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
143 |
val ANTIQ = "antiq" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
144 |
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
|
145 |
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
|
146 |
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
|
147 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
148 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
149 |
/* text structure */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
150 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
151 |
val PARAGRAPH = "paragraph" |
50545
00bdc48c5f71
explicit text_fold markup, which is used by default in Pretty.chunks/chunks2;
wenzelm
parents:
50543
diff
changeset
|
152 |
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
|
153 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
154 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
155 |
/* ML syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
156 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
157 |
val ML_KEYWORD = "ML_keyword" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
158 |
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
|
159 |
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
|
160 |
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
|
161 |
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
|
162 |
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
|
163 |
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
|
164 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
165 |
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
|
166 |
val ML_OPEN = "ML_open" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
167 |
val ML_STRUCT = "ML_struct" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
168 |
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
|
169 |
|
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 |
/* outer syntax */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
172 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
173 |
val KEYWORD = "keyword" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
174 |
val OPERATOR = "operator" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
175 |
val COMMAND = "command" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
176 |
val STRING = "string" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
177 |
val ALTSTRING = "altstring" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
178 |
val VERBATIM = "verbatim" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
179 |
val COMMENT = "comment" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
180 |
val CONTROL = "control" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
181 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
182 |
val KEYWORD1 = "keyword1" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
183 |
val KEYWORD2 = "keyword2" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
184 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
185 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
186 |
/* timing */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
187 |
|
50781 | 188 |
val Elapsed = new Properties.Double("elapsed") |
189 |
val CPU = new Properties.Double("cpu") |
|
190 |
val GC = new Properties.Double("gc") |
|
191 |
||
192 |
object Timing_Properties |
|
193 |
{ |
|
194 |
def apply(timing: isabelle.Timing): Properties.T = |
|
195 |
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
|
196 |
|
50781 | 197 |
def unapply(props: Properties.T): Option[isabelle.Timing] = |
198 |
(props, props, props) match { |
|
199 |
case (Elapsed(elapsed), CPU(cpu), GC(gc)) => |
|
200 |
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) |
|
201 |
case _ => None |
|
202 |
} |
|
203 |
} |
|
204 |
||
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
205 |
val TIMING = "timing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
206 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
207 |
object Timing |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
208 |
{ |
50781 | 209 |
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
|
210 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
211 |
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
|
212 |
markup match { |
50781 | 213 |
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
|
214 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
215 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
216 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
217 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
218 |
|
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
219 |
/* command timing */ |
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
220 |
|
51818
517f232e867d
clarified module dependencies: avoid Properties and Document introding minimal "PIDE";
wenzelm
parents:
51662
diff
changeset
|
221 |
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
|
222 |
|
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51574
diff
changeset
|
223 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
224 |
/* toplevel */ |
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 SUBGOALS = "subgoals" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
227 |
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
|
228 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
229 |
val STATE = "state" |
50543 | 230 |
val GOAL = "goal" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
231 |
val SUBGOAL = "subgoal" |
50215 | 232 |
|
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50255
diff
changeset
|
233 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
234 |
/* command status */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
235 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
236 |
val TASK = "task" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
237 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
238 |
val ACCEPTED = "accepted" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
239 |
val FORKED = "forked" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
240 |
val JOINED = "joined" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
241 |
val RUNNING = "running" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
242 |
val FINISHED = "finished" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
243 |
val FAILED = "failed" |
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 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
246 |
/* interactive documents */ |
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 |
val VERSION = "version" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
249 |
val ASSIGN = "assign" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
250 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
251 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
252 |
/* prover process */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
253 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
254 |
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
|
255 |
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
|
256 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
257 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
258 |
/* messages */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
259 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
260 |
val Serial = new Properties.Long("serial") |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
261 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
262 |
val MESSAGE = "message" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
263 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
264 |
val INIT = "init" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
265 |
val STATUS = "status" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
266 |
val REPORT = "report" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
267 |
val RESULT = "result" |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
268 |
val WRITELN = "writeln" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
269 |
val TRACING = "tracing" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
270 |
val WARNING = "warning" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
271 |
val ERROR = "error" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
272 |
val PROTOCOL = "protocol" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
273 |
val SYSTEM = "system" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
274 |
val STDOUT = "stdout" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
275 |
val STDERR = "stderr" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
276 |
val EXIT = "exit" |
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 |
val WRITELN_MESSAGE = "writeln_message" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
279 |
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
|
280 |
val WARNING_MESSAGE = "warning_message" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
281 |
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
|
282 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
283 |
val message: String => String = |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
284 |
Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE, |
50501
6f41f1646617
more careful handling of Dialog_Result, with active area and color feedback;
wenzelm
parents:
50500
diff
changeset
|
285 |
WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).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
|
286 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
287 |
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
|
288 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
289 |
val LEGACY = "legacy" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
290 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
291 |
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
|
292 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
293 |
val BAD = "bad" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
294 |
|
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
295 |
val INTENSIFY = "intensify" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
296 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
297 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
298 |
/* active areas */ |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
299 |
|
50715
8cfd585b9162
prefer old graph browser in Isabelle/jEdit, which still produces better layout;
wenzelm
parents:
50545
diff
changeset
|
300 |
val BROWSER = "browser" |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
301 |
val GRAPHVIEW = "graphview" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
302 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
303 |
val SENDBACK = "sendback" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
304 |
val PADDING = "padding" |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
305 |
val PADDING_LINE = (PADDING, LINE) |
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
306 |
|
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
307 |
val DIALOG = "dialog" |
50503
50f141b34bb7
enable Isabelle/ML to produce uninterpreted result messages as well;
wenzelm
parents:
50501
diff
changeset
|
308 |
val Result = new Properties.String(RESULT) |
50500
c94bba7906d2
identify dialogs via official serial and maintain as result message;
wenzelm
parents:
50499
diff
changeset
|
309 |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
310 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
311 |
/* protocol message functions */ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
312 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
313 |
val FUNCTION = "function" |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
314 |
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
|
315 |
|
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
316 |
val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs")) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
317 |
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
|
318 |
|
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
319 |
object Protocol_Handler |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
320 |
{ |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
321 |
def unapply(props: Properties.T): Option[(String)] = |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
322 |
props match { |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
323 |
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
|
324 |
case _ => None |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
325 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
326 |
} |
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
327 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
328 |
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
|
329 |
object Invoke_Scala |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
330 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
331 |
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
|
332 |
props match { |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
333 |
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
|
334 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
335 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
336 |
} |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
337 |
|
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
338 |
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
|
339 |
object Cancel_Scala |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
340 |
{ |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
341 |
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
|
342 |
props match { |
52111
1fd184eaa310
explicit management of Session.Protocol_Handlers, with protocol state and functions;
wenzelm
parents:
51818
diff
changeset
|
343 |
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
|
344 |
case _ => None |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
345 |
} |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49613
diff
changeset
|
346 |
} |
50255 | 347 |
|
348 |
object ML_Statistics |
|
349 |
{ |
|
350 |
def unapply(props: Properties.T): Option[Properties.T] = |
|
351 |
props match { |
|
352 |
case (FUNCTION, "ML_statistics") :: stats => Some(stats) |
|
353 |
case _ => None |
|
354 |
} |
|
355 |
} |
|
50975 | 356 |
|
357 |
object Task_Statistics |
|
358 |
{ |
|
359 |
def unapply(props: Properties.T): Option[Properties.T] = |
|
360 |
props match { |
|
361 |
case (FUNCTION, "task_statistics") :: stats => Some(stats) |
|
362 |
case _ => None |
|
363 |
} |
|
364 |
} |
|
45666 | 365 |
} |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
366 |
|
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
367 |
|
45666 | 368 |
sealed case class Markup(name: String, properties: Properties.T) |
43748 | 369 |