author  wenzelm 
Sun, 09 Jan 2011 16:03:56 +0100  
changeset 41483  4a8431c73cf2 
parent 40848  8662b9b1f123 
child 42136  826168ae0213 
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" 

87 
val KIND = "kind" 

88 

89 

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

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

91 

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

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

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

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

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

96 

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

97 

27970  98 
/* position */ 
99 

100 
val LINE = "line" 

101 
val COLUMN = "column" 

102 
val OFFSET = "offset" 

103 
val END_OFFSET = "end_offset" 

104 
val FILE = "file" 

105 
val ID = "id" 

106 

41483  107 
val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID) 
29205  108 

29184  109 
val POSITION = "position" 
110 

111 

36683  112 
/* pretty printing */ 
113 

38724  114 
val Indent = new Int_Property("indent") 
36683  115 
val BLOCK = "block" 
38724  116 
val Width = new Int_Property("width") 
36683  117 
val BREAK = "break" 
118 

119 

33985  120 
/* hidden text */ 
121 

122 
val HIDDEN = "hidden" 

123 

124 

29184  125 
/* logical entities */ 
126 

127 
val TCLASS = "tclass" 

128 
val TYCON = "tycon" 

129 
val FIXED_DECL = "fixed_decl" 

130 
val FIXED = "fixed" 

131 
val CONST_DECL = "const_decl" 

132 
val CONST = "const" 

133 
val FACT_DECL = "fact_decl" 

134 
val FACT = "fact" 

135 
val DYNAMIC_FACT = "dynamic_fact" 

136 
val LOCAL_FACT_DECL = "local_fact_decl" 

137 
val LOCAL_FACT = "local_fact" 

138 

139 

140 
/* inner syntax */ 

141 

142 
val TFREE = "tfree" 

143 
val TVAR = "tvar" 

144 
val FREE = "free" 

145 
val SKOLEM = "skolem" 

146 
val BOUND = "bound" 

147 
val VAR = "var" 

148 
val NUM = "num" 

149 
val FLOAT = "float" 

150 
val XNUM = "xnum" 

151 
val XSTR = "xstr" 

152 
val LITERAL = "literal" 

153 
val INNER_COMMENT = "inner_comment" 

154 

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

155 
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

156 

29184  157 
val SORT = "sort" 
158 
val TYP = "typ" 

159 
val TERM = "term" 

160 
val PROP = "prop" 

161 

162 
val ATTRIBUTE = "attribute" 

163 
val METHOD = "method" 

164 

165 

166 
/* embedded source text */ 

167 

168 
val ML_SOURCE = "ML_source" 

169 
val DOC_SOURCE = "doc_source" 

170 

171 
val ANTIQ = "antiq" 

172 
val ML_ANTIQ = "ML_antiq" 

173 
val DOC_ANTIQ = "doc_antiq" 

174 

175 

30615  176 
/* ML syntax */ 
177 

178 
val ML_KEYWORD = "ML_keyword" 

37195  179 
val ML_DELIMITER = "ML_delimiter" 
30615  180 
val ML_IDENT = "ML_ident" 
181 
val ML_TVAR = "ML_tvar" 

182 
val ML_NUMERAL = "ML_numeral" 

183 
val ML_CHAR = "ML_char" 

184 
val ML_STRING = "ML_string" 

185 
val ML_COMMENT = "ML_comment" 

186 
val ML_MALFORMED = "ML_malformed" 

187 

30702  188 
val ML_DEF = "ML_def" 
31472  189 
val ML_OPEN = "ML_open" 
190 
val ML_STRUCT = "ML_struct" 

30702  191 
val ML_REF = "ML_ref" 
192 
val ML_TYPING = "ML_typing" 

193 

30615  194 

29184  195 
/* outer syntax */ 
196 

197 
val KEYWORD_DECL = "keyword_decl" 

198 
val COMMAND_DECL = "command_decl" 

199 

200 
val KEYWORD = "keyword" 

37194  201 
val OPERATOR = "operator" 
29184  202 
val COMMAND = "command" 
203 
val IDENT = "ident" 

204 
val STRING = "string" 

205 
val ALTSTRING = "altstring" 

206 
val VERBATIM = "verbatim" 

207 
val COMMENT = "comment" 

208 
val CONTROL = "control" 

209 
val MALFORMED = "malformed" 

210 

29185  211 
val COMMAND_SPAN = "command_span" 
212 
val IGNORED_SPAN = "ignored_span" 

213 
val MALFORMED_SPAN = "malformed_span" 

214 

29184  215 

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

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

217 

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

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

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

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

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

222 

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

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

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

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

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

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

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

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

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

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

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

233 
(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

234 
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

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

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

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

238 

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

239 

29184  240 
/* toplevel */ 
241 

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

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

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

244 

29184  245 
val STATE = "state" 
246 
val SUBGOAL = "subgoal" 

247 
val SENDBACK = "sendback" 

248 
val HILITE = "hilite" 

249 

250 

251 
/* command status */ 

252 

29417  253 
val TASK = "task" 
254 

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

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

256 
val JOINED = "joined" 
29184  257 
val FAILED = "failed" 
258 
val FINISHED = "finished" 

29488  259 

260 

261 
/* interactive documents */ 

262 

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

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

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

265 
val ASSIGN = "assign" 
29488  266 
val EDIT = "edit" 
29184  267 

27970  268 

269 
/* messages */ 

270 

38872  271 
val Serial = new Long_Property("serial") 
27970  272 

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

274 
val CLASS = "class" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

275 

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

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

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

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

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

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

282 
val ERROR = "error" 
793766d4c1b5
moved message markup into Scala layer  reduced redundancy;
wenzelm
parents:
29488
diff
changeset

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

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

285 
val EXIT = "exit" 
29195  286 

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

287 
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

288 

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

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

290 

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

292 

27970  293 

34119  294 
/* system data */ 
27970  295 

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

298 

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

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