author | wenzelm |
Wed, 18 Aug 2010 11:02:47 +0200 | |
changeset 38474 | e498dc2eb576 |
parent 38429 | 9951852fae91 |
child 38721 | ca8b14fa0d0d |
permissions | -rw-r--r-- |
27958 | 1 |
/* Title: Pure/General/markup.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Common markup elements. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
27970 | 9 |
|
32450 | 10 |
object Markup |
11 |
{ |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
12 |
/* integers */ |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
13 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
14 |
object Int { |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
15 |
def apply(i: scala.Int): String = i.toString |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
16 |
def unapply(s: String): Option[scala.Int] = |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
17 |
try { Some(Integer.parseInt(s)) } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
18 |
catch { case _: NumberFormatException => None } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
19 |
} |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
20 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
21 |
object Long { |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
22 |
def apply(i: scala.Long): String = i.toString |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
23 |
def unapply(s: String): Option[scala.Long] = |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
24 |
try { Some(java.lang.Long.parseLong(s)) } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
25 |
catch { case _: NumberFormatException => None } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
26 |
} |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
27 |
|
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
28 |
|
36683 | 29 |
/* property values */ |
30 |
||
31 |
def get_string(name: String, props: List[(String, String)]): Option[String] = |
|
32 |
props.find(p => p._1 == name).map(_._2) |
|
33 |
||
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
34 |
def get_long(name: String, props: List[(String, String)]): Option[scala.Long] = |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
35 |
{ |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
36 |
get_string(name, props) match { |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
37 |
case None => None |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
38 |
case Some(Long(i)) => Some(i) |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
39 |
} |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
40 |
} |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
41 |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
42 |
def get_int(name: String, props: List[(String, String)]): Option[scala.Int] = |
36683 | 43 |
{ |
44 |
get_string(name, props) match { |
|
45 |
case None => None |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
46 |
case Some(Int(i)) => Some(i) |
36683 | 47 |
} |
48 |
} |
|
49 |
||
50 |
||
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
51 |
/* empty */ |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
52 |
|
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
53 |
val Empty = Markup("", Nil) |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
54 |
|
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
55 |
|
29184 | 56 |
/* name */ |
57 |
||
58 |
val NAME = "name" |
|
59 |
val KIND = "kind" |
|
60 |
||
61 |
||
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
62 |
/* formal entities */ |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
63 |
|
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
64 |
val ENTITY = "entity" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
65 |
val DEF = "def" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
66 |
val REF = "ref" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
67 |
|
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
68 |
|
27970 | 69 |
/* position */ |
70 |
||
71 |
val LINE = "line" |
|
72 |
val COLUMN = "column" |
|
73 |
val OFFSET = "offset" |
|
74 |
val END_LINE = "end_line" |
|
75 |
val END_COLUMN = "end_column" |
|
76 |
val END_OFFSET = "end_offset" |
|
77 |
val FILE = "file" |
|
78 |
val ID = "id" |
|
79 |
||
32450 | 80 |
val POSITION_PROPERTIES = |
81 |
Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID) |
|
29205 | 82 |
|
29184 | 83 |
val POSITION = "position" |
84 |
val LOCATION = "location" |
|
85 |
||
86 |
||
36683 | 87 |
/* pretty printing */ |
88 |
||
89 |
val INDENT = "indent" |
|
90 |
val BLOCK = "block" |
|
91 |
val WIDTH = "width" |
|
92 |
val BREAK = "break" |
|
93 |
||
94 |
||
33985 | 95 |
/* hidden text */ |
96 |
||
97 |
val HIDDEN = "hidden" |
|
98 |
||
99 |
||
29184 | 100 |
/* logical entities */ |
101 |
||
102 |
val TCLASS = "tclass" |
|
103 |
val TYCON = "tycon" |
|
104 |
val FIXED_DECL = "fixed_decl" |
|
105 |
val FIXED = "fixed" |
|
106 |
val CONST_DECL = "const_decl" |
|
107 |
val CONST = "const" |
|
108 |
val FACT_DECL = "fact_decl" |
|
109 |
val FACT = "fact" |
|
110 |
val DYNAMIC_FACT = "dynamic_fact" |
|
111 |
val LOCAL_FACT_DECL = "local_fact_decl" |
|
112 |
val LOCAL_FACT = "local_fact" |
|
113 |
||
114 |
||
115 |
/* inner syntax */ |
|
116 |
||
117 |
val TFREE = "tfree" |
|
118 |
val TVAR = "tvar" |
|
119 |
val FREE = "free" |
|
120 |
val SKOLEM = "skolem" |
|
121 |
val BOUND = "bound" |
|
122 |
val VAR = "var" |
|
123 |
val NUM = "num" |
|
124 |
val FLOAT = "float" |
|
125 |
val XNUM = "xnum" |
|
126 |
val XSTR = "xstr" |
|
127 |
val LITERAL = "literal" |
|
128 |
val INNER_COMMENT = "inner_comment" |
|
129 |
||
130 |
val SORT = "sort" |
|
131 |
val TYP = "typ" |
|
132 |
val TERM = "term" |
|
133 |
val PROP = "prop" |
|
134 |
||
135 |
val ATTRIBUTE = "attribute" |
|
136 |
val METHOD = "method" |
|
137 |
||
138 |
||
139 |
/* embedded source text */ |
|
140 |
||
141 |
val ML_SOURCE = "ML_source" |
|
142 |
val DOC_SOURCE = "doc_source" |
|
143 |
||
144 |
val ANTIQ = "antiq" |
|
145 |
val ML_ANTIQ = "ML_antiq" |
|
146 |
val DOC_ANTIQ = "doc_antiq" |
|
147 |
||
148 |
||
30615 | 149 |
/* ML syntax */ |
150 |
||
151 |
val ML_KEYWORD = "ML_keyword" |
|
37195 | 152 |
val ML_DELIMITER = "ML_delimiter" |
30615 | 153 |
val ML_IDENT = "ML_ident" |
154 |
val ML_TVAR = "ML_tvar" |
|
155 |
val ML_NUMERAL = "ML_numeral" |
|
156 |
val ML_CHAR = "ML_char" |
|
157 |
val ML_STRING = "ML_string" |
|
158 |
val ML_COMMENT = "ML_comment" |
|
159 |
val ML_MALFORMED = "ML_malformed" |
|
160 |
||
30702 | 161 |
val ML_DEF = "ML_def" |
31472 | 162 |
val ML_OPEN = "ML_open" |
163 |
val ML_STRUCT = "ML_struct" |
|
30702 | 164 |
val ML_REF = "ML_ref" |
165 |
val ML_TYPING = "ML_typing" |
|
166 |
||
30615 | 167 |
|
29184 | 168 |
/* outer syntax */ |
169 |
||
170 |
val KEYWORD_DECL = "keyword_decl" |
|
171 |
val COMMAND_DECL = "command_decl" |
|
172 |
||
173 |
val KEYWORD = "keyword" |
|
37194 | 174 |
val OPERATOR = "operator" |
29184 | 175 |
val COMMAND = "command" |
176 |
val IDENT = "ident" |
|
177 |
val STRING = "string" |
|
178 |
val ALTSTRING = "altstring" |
|
179 |
val VERBATIM = "verbatim" |
|
180 |
val COMMENT = "comment" |
|
181 |
val CONTROL = "control" |
|
182 |
val MALFORMED = "malformed" |
|
183 |
||
29185 | 184 |
val COMMAND_SPAN = "command_span" |
185 |
val IGNORED_SPAN = "ignored_span" |
|
186 |
val MALFORMED_SPAN = "malformed_span" |
|
187 |
||
29184 | 188 |
|
189 |
/* toplevel */ |
|
190 |
||
191 |
val STATE = "state" |
|
192 |
val SUBGOAL = "subgoal" |
|
193 |
val SENDBACK = "sendback" |
|
194 |
val HILITE = "hilite" |
|
195 |
||
196 |
||
197 |
/* command status */ |
|
198 |
||
29417 | 199 |
val TASK = "task" |
200 |
||
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset
|
201 |
val FORKED = "forked" |
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset
|
202 |
val JOINED = "joined" |
29184 | 203 |
val FAILED = "failed" |
204 |
val FINISHED = "finished" |
|
29488 | 205 |
|
206 |
||
207 |
/* interactive documents */ |
|
208 |
||
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
209 |
val VERSION = "version" |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
210 |
val EXEC = "exec" |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
211 |
val ASSIGN = "assign" |
29488 | 212 |
val EDIT = "edit" |
29184 | 213 |
|
27970 | 214 |
|
215 |
/* messages */ |
|
216 |
||
217 |
val PID = "pid" |
|
218 |
||
29195 | 219 |
val MESSAGE = "message" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
220 |
val CLASS = "class" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
221 |
|
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
222 |
val INIT = "init" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
223 |
val STATUS = "status" |
38236
d8c7be27e01d
explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents:
38231
diff
changeset
|
224 |
val REPORT = "report" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
225 |
val WRITELN = "writeln" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
226 |
val TRACING = "tracing" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
227 |
val WARNING = "warning" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
228 |
val ERROR = "error" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
229 |
val DEBUG = "debug" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
230 |
val SYSTEM = "system" |
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38236
diff
changeset
|
231 |
val INPUT = "input" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
232 |
val STDIN = "stdin" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
233 |
val STDOUT = "stdout" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
234 |
val SIGNAL = "signal" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
235 |
val EXIT = "exit" |
29195 | 236 |
|
38231 | 237 |
val Ready = Markup("ready", Nil) |
31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30702
diff
changeset
|
238 |
|
27970 | 239 |
|
34119 | 240 |
/* system data */ |
27970 | 241 |
|
38231 | 242 |
val Data = Markup("data", Nil) |
27958 | 243 |
} |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset
|
244 |
|
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset
|
245 |
sealed case class Markup(name: String, properties: List[(String, String)]) |