author  wenzelm 
Mon, 11 Jul 2011 11:13:33 +0200  
changeset 43746  a41f618c641d 
parent 43721  fad8634cee62 
child 43748  c70bd78ec83c 
permissions  rwrr 
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 
{ 

38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

12 
/* plain values */ 
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

13 

40392  14 
object Int 
15 
{ 

16 
def apply(x: scala.Int): String = x.toString 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

17 
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

18 
try { Some(Integer.parseInt(s)) } 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

19 
catch { case _: NumberFormatException => None } 
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 

40392  22 
object Long 
23 
{ 

24 
def apply(x: scala.Long): String = x.toString 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

25 
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

26 
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

27 
catch { case _: NumberFormatException => None } 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

28 
} 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

29 

40392  30 
object Double 
31 
{ 

32 
def apply(x: scala.Double): String = x.toString 

33 
def unapply(s: String): Option[scala.Double] = 

34 
try { Some(java.lang.Double.parseDouble(s)) } 

35 
catch { case _: NumberFormatException => None } 

36 
} 

37 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

38 

38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

39 
/* named properties */ 
36683  40 

38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

41 
class Property(val name: String) 
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

42 
{ 
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

43 
def apply(value: String): List[(String, String)] = List((name, value)) 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

44 
def unapply(props: List[(String, String)]): Option[String] = 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

45 
props.find(_._1 == name).map(_._2) 
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

46 
} 
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

47 

38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

48 
class Int_Property(name: String) 
36683  49 
{ 
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

50 
def apply(value: scala.Int): List[(String, String)] = List((name, Int(value))) 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

51 
def unapply(props: List[(String, String)]): Option[Int] = 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

52 
props.find(_._1 == name) match { 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

53 
case None => None 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

54 
case Some((_, value)) => Int.unapply(value) 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

55 
} 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

56 
} 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

57 

ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

58 
class Long_Property(name: String) 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

59 
{ 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

60 
def apply(value: scala.Long): List[(String, String)] = List((name, Long(value))) 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

61 
def unapply(props: List[(String, String)]): Option[Long] = 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

62 
props.find(_._1 == name) match { 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

63 
case None => None 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

64 
case Some((_, value)) => Long.unapply(value) 
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset

65 
} 
36683  66 
} 
67 

40392  68 
class Double_Property(name: String) 
69 
{ 

70 
def apply(value: scala.Double): List[(String, String)] = List((name, Double(value))) 

71 
def unapply(props: List[(String, String)]): Option[Double] = 

72 
props.find(_._1 == name) match { 

73 
case None => None 

74 
case Some((_, value)) => Double.unapply(value) 

75 
} 

76 
} 

77 

36683  78 

38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

79 
/* empty */ 
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

80 

e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

81 
val Empty = Markup("", Nil) 
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

82 

e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset

83 

38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

84 
/* misc properties */ 
29184  85 

86 
val NAME = "name" 

42136  87 
val Name = new Property(NAME) 
88 

29184  89 
val KIND = "kind" 
42136  90 
val Kind = new Property(KIND) 
29184  91 

92 

33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

93 
/* formal entities */ 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

94 

38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset

95 
val BINDING = "binding" 
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

96 
val ENTITY = "entity" 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

97 
val DEF = "def" 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

98 
val REF = "ref" 
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

99 

42202  100 
object Entity 
101 
{ 

102 
def unapply(markup: Markup): Option[(String, String)] = 

103 
markup match { 

104 
case Markup(ENTITY, props @ Kind(kind)) => 

105 
props match { 

106 
case Name(name) => Some(kind, name) 

107 
case _ => None 

108 
} 

109 
case _ => None 

110 
} 

111 
} 

112 

33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset

113 

27970  114 
/* position */ 
115 

116 
val LINE = "line" 

117 
val OFFSET = "offset" 

118 
val END_OFFSET = "end_offset" 

119 
val FILE = "file" 

120 
val ID = "id" 

121 

42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset

122 
val DEF_LINE = "def_line" 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset

123 
val DEF_OFFSET = "def_offset" 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset

124 
val DEF_END_OFFSET = "def_end_offset" 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset

125 
val DEF_FILE = "def_file" 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset

126 
val DEF_ID = "def_id" 
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset

127 

43710
7270ae921cf2
discontinued odd Position.column  leftover from attempts at PGIP implementation;
wenzelm
parents:
43673
diff
changeset

128 
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) 
43593  129 
val POSITION = "position" 
29205  130 

43593  131 

132 
/* path */ 

133 

134 
val PATH = "path" 

135 

136 
object Path 

137 
{ 

138 
def unapply(markup: Markup): Option[String] = 

139 
markup match { 

140 
case Markup(PATH, Name(name)) => Some(name) 

141 
case _ => None 

142 
} 

143 
} 

29184  144 

145 

36683  146 
/* pretty printing */ 
147 

38724  148 
val Indent = new Int_Property("indent") 
36683  149 
val BLOCK = "block" 
38724  150 
val Width = new Int_Property("width") 
36683  151 
val BREAK = "break" 
152 

153 

33985  154 
/* hidden text */ 
155 

156 
val HIDDEN = "hidden" 

157 

158 

29184  159 
/* logical entities */ 
160 

43551  161 
val CLASS = "class" 
43552  162 
val TYPE = "type" 
29184  163 
val FIXED = "fixed" 
43552  164 
val CONSTANT = "constant" 
165 

29184  166 
val DYNAMIC_FACT = "dynamic_fact" 
167 

168 

169 
/* inner syntax */ 

170 

171 
val TFREE = "tfree" 

172 
val TVAR = "tvar" 

173 
val FREE = "free" 

174 
val SKOLEM = "skolem" 

175 
val BOUND = "bound" 

176 
val VAR = "var" 

177 
val NUM = "num" 

178 
val FLOAT = "float" 

179 
val XNUM = "xnum" 

180 
val XSTR = "xstr" 

181 
val LITERAL = "literal" 

43432
224006e5ac46
inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents:
43386
diff
changeset

182 
val DELIMITER = "delimiter" 
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
42492
diff
changeset

183 
val INNER_STRING = "inner_string" 
29184  184 
val INNER_COMMENT = "inner_comment" 
185 

39168
e3ac771235f7
report token range after inner parse error  often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset

186 
val TOKEN_RANGE = "token_range" 
e3ac771235f7
report token range after inner parse error  often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset

187 

29184  188 
val SORT = "sort" 
189 
val TYP = "typ" 

190 
val TERM = "term" 

191 
val PROP = "prop" 

192 

193 
val ATTRIBUTE = "attribute" 

194 
val METHOD = "method" 

195 

196 

197 
/* embedded source text */ 

198 

199 
val ML_SOURCE = "ML_source" 

200 
val DOC_SOURCE = "doc_source" 

201 

202 
val ANTIQ = "antiq" 

43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43552
diff
changeset

203 
val ML_ANTIQUOTATION = "ML antiquotation" 
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

204 
val DOCUMENT_ANTIQUOTATION = "document antiquotation" 
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset

205 
val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option" 
29184  206 

207 

30615  208 
/* ML syntax */ 
209 

210 
val ML_KEYWORD = "ML_keyword" 

37195  211 
val ML_DELIMITER = "ML_delimiter" 
30615  212 
val ML_IDENT = "ML_ident" 
213 
val ML_TVAR = "ML_tvar" 

214 
val ML_NUMERAL = "ML_numeral" 

215 
val ML_CHAR = "ML_char" 

216 
val ML_STRING = "ML_string" 

217 
val ML_COMMENT = "ML_comment" 

218 
val ML_MALFORMED = "ML_malformed" 

219 

30702  220 
val ML_DEF = "ML_def" 
31472  221 
val ML_OPEN = "ML_open" 
222 
val ML_STRUCT = "ML_struct" 

30702  223 
val ML_TYPING = "ML_typing" 
224 

30615  225 

29184  226 
/* outer syntax */ 
227 

228 
val KEYWORD_DECL = "keyword_decl" 

229 
val COMMAND_DECL = "command_decl" 

230 

231 
val KEYWORD = "keyword" 

37194  232 
val OPERATOR = "operator" 
29184  233 
val COMMAND = "command" 
234 
val IDENT = "ident" 

235 
val STRING = "string" 

236 
val ALTSTRING = "altstring" 

237 
val VERBATIM = "verbatim" 

238 
val COMMENT = "comment" 

239 
val CONTROL = "control" 

240 
val MALFORMED = "malformed" 

241 

29185  242 
val COMMAND_SPAN = "command_span" 
243 
val IGNORED_SPAN = "ignored_span" 

244 
val MALFORMED_SPAN = "malformed_span" 

245 

29184  246 

43673
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset

247 
/* theory loader */ 
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset

248 

29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset

249 
val LOADED_THEORY = "loaded_theory" 
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset

250 

29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset

251 

40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

252 
/* timing */ 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

253 

6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

254 
val TIMING = "timing" 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

255 
val ELAPSED = "elapsed" 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

256 
val CPU = "cpu" 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

257 
val GC = "gc" 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

258 

6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

259 
object Timing 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

260 
{ 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

261 
def apply(timing: isabelle.Timing): Markup = 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

262 
Markup(TIMING, List( 
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset

263 
(ELAPSED, Double(timing.elapsed.seconds)), 
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset

264 
(CPU, Double(timing.cpu.seconds)), 
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset

265 
(GC, Double(timing.gc.seconds)))) 
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

266 
def unapply(markup: Markup): Option[isabelle.Timing] = 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

267 
markup match { 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

268 
case Markup(TIMING, List( 
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset

269 
(ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) => 
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset

270 
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) 
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

271 
case _ => None 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

272 
} 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

273 
} 
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

274 

6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset

275 

29184  276 
/* toplevel */ 
277 

38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

278 
val SUBGOALS = "subgoals" 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

279 
val PROOF_STATE = "proof_state" 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset

280 

29184  281 
val STATE = "state" 
282 
val SUBGOAL = "subgoal" 

283 
val SENDBACK = "sendback" 

284 
val HILITE = "hilite" 

285 

286 

287 
/* command status */ 

288 

29417  289 
val TASK = "task" 
290 

37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset

291 
val FORKED = "forked" 
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset

292 
val JOINED = "joined" 
29184  293 
val FAILED = "failed" 
294 
val FINISHED = "finished" 

29488  295 

296 

297 
/* interactive documents */ 

298 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

299 
val VERSION = "version" 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

300 
val EXEC = "exec" 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset

301 
val ASSIGN = "assign" 
29488  302 
val EDIT = "edit" 
29184  303 

27970  304 

43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset

305 
/* prover process */ 
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset

306 

fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset

307 
val PROVER_COMMAND = "prover_command" 
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset

308 
val PROVER_ARG = "prover_arg" 
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset

309 

fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset

310 

27970  311 
/* messages */ 
312 

38872  313 
val Serial = new Long_Property("serial") 
27970  314 

29195  315 
val MESSAGE = "message" 
29522
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

316 

793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

317 
val INIT = "init" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

318 
val STATUS = "status" 
39525  319 
val REPORT = "report" 
29522
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

320 
val WRITELN = "writeln" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

321 
val TRACING = "tracing" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

322 
val WARNING = "warning" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

323 
val ERROR = "error" 
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43721
diff
changeset

324 
val RAW = "raw" 
29522
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

325 
val SYSTEM = "system" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

326 
val STDOUT = "stdout" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

327 
val EXIT = "exit" 
29195  328 

39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39171
diff
changeset

329 
val NO_REPORT = "no_report" 
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39171
diff
changeset

330 

39171
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset

331 
val BAD = "bad" 
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset

332 

39591  333 
val READY = "ready" 
31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30702
diff
changeset

334 

27970  335 

34119  336 
/* system data */ 
27970  337 

38231  338 
val Data = Markup("data", Nil) 
27958  339 
} 
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset

340 

ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset

341 
sealed case class Markup(name: String, properties: List[(String, String)]) 