1 /* Title: Pure/General/markup.scala
4 Common markup elements.
16 def apply(x: scala.Int): String = x.toString
17 def unapply(s: String): Option[scala.Int] =
18 try { Some(Integer.parseInt(s)) }
19 catch { case _: NumberFormatException => None }
24 def apply(x: scala.Long): String = x.toString
25 def unapply(s: String): Option[scala.Long] =
26 try { Some(java.lang.Long.parseLong(s)) }
27 catch { case _: NumberFormatException => None }
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 }
39 /* named properties */
41 class Property(val name: String)
43 def apply(value: String): List[(String, String)] = List((name, value))
44 def unapply(props: List[(String, String)]): Option[String] =
45 props.find(_._1 == name).map(_._2)
48 class Int_Property(name: String)
50 def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
51 def unapply(props: List[(String, String)]): Option[Int] =
52 props.find(_._1 == name) match {
54 case Some((_, value)) => Int.unapply(value)
58 class Long_Property(name: String)
60 def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
61 def unapply(props: List[(String, String)]): Option[Long] =
62 props.find(_._1 == name) match {
64 case Some((_, value)) => Long.unapply(value)
68 class Double_Property(name: String)
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 {
74 case Some((_, value)) => Double.unapply(value)
81 val Empty = Markup("", Nil)
87 val Name = new Property(NAME)
90 val Kind = new Property(KIND)
95 val BINDING = "binding"
102 def unapply(markup: Markup): Option[(String, String)] =
104 case Markup(ENTITY, props @ Kind(kind)) =>
106 case Name(name) => Some(kind, name)
117 val COLUMN = "column"
118 val OFFSET = "offset"
119 val END_OFFSET = "end_offset"
123 val DEF_LINE = "def_line"
124 val DEF_COLUMN = "def_column"
125 val DEF_OFFSET = "def_offset"
126 val DEF_END_OFFSET = "def_end_offset"
127 val DEF_FILE = "def_file"
128 val DEF_ID = "def_id"
130 val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID)
131 val POSITION = "position"
140 def unapply(markup: Markup): Option[String] =
142 case Markup(PATH, Name(name)) => Some(name)
148 /* pretty printing */
150 val Indent = new Int_Property("indent")
152 val Width = new Int_Property("width")
158 val HIDDEN = "hidden"
161 /* logical entities */
166 val CONSTANT = "constant"
168 val DYNAMIC_FACT = "dynamic_fact"
176 val SKOLEM = "skolem"
183 val LITERAL = "literal"
184 val DELIMITER = "delimiter"
185 val INNER_STRING = "inner_string"
186 val INNER_COMMENT = "inner_comment"
188 val TOKEN_RANGE = "token_range"
195 val ATTRIBUTE = "attribute"
196 val METHOD = "method"
199 /* embedded source text */
201 val ML_SOURCE = "ML_source"
202 val DOC_SOURCE = "doc_source"
205 val ML_ANTIQUOTATION = "ML antiquotation"
206 val DOCUMENT_ANTIQUOTATION = "document antiquotation"
207 val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
212 val ML_KEYWORD = "ML_keyword"
213 val ML_DELIMITER = "ML_delimiter"
214 val ML_IDENT = "ML_ident"
215 val ML_TVAR = "ML_tvar"
216 val ML_NUMERAL = "ML_numeral"
217 val ML_CHAR = "ML_char"
218 val ML_STRING = "ML_string"
219 val ML_COMMENT = "ML_comment"
220 val ML_MALFORMED = "ML_malformed"
222 val ML_DEF = "ML_def"
223 val ML_OPEN = "ML_open"
224 val ML_STRUCT = "ML_struct"
225 val ML_TYPING = "ML_typing"
230 val KEYWORD_DECL = "keyword_decl"
231 val COMMAND_DECL = "command_decl"
233 val KEYWORD = "keyword"
234 val OPERATOR = "operator"
235 val COMMAND = "command"
237 val STRING = "string"
238 val ALTSTRING = "altstring"
239 val VERBATIM = "verbatim"
240 val COMMENT = "comment"
241 val CONTROL = "control"
242 val MALFORMED = "malformed"
244 val COMMAND_SPAN = "command_span"
245 val IGNORED_SPAN = "ignored_span"
246 val MALFORMED_SPAN = "malformed_span"
251 val TIMING = "timing"
252 val ELAPSED = "elapsed"
258 def apply(timing: isabelle.Timing): Markup =
260 (ELAPSED, Double(timing.elapsed.seconds)),
261 (CPU, Double(timing.cpu.seconds)),
262 (GC, Double(timing.gc.seconds))))
263 def unapply(markup: Markup): Option[isabelle.Timing] =
265 case Markup(TIMING, List(
266 (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
267 Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
275 val SUBGOALS = "subgoals"
276 val PROOF_STATE = "proof_state"
279 val SUBGOAL = "subgoal"
280 val SENDBACK = "sendback"
281 val HILITE = "hilite"
288 val FORKED = "forked"
289 val JOINED = "joined"
290 val FAILED = "failed"
291 val FINISHED = "finished"
294 /* interactive documents */
296 val VERSION = "version"
298 val ASSIGN = "assign"
304 val Serial = new Long_Property("serial")
306 val MESSAGE = "message"
309 val STATUS = "status"
310 val REPORT = "report"
311 val WRITELN = "writeln"
312 val TRACING = "tracing"
313 val WARNING = "warning"
315 val SYSTEM = "system"
316 val STDOUT = "stdout"
319 val NO_REPORT = "no_report"
328 val Data = Markup("data", Nil)
331 sealed case class Markup(name: String, properties: List[(String, String)])