--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/markup.scala Tue Nov 29 19:49:36 2011 +0100
@@ -0,0 +1,57 @@
+/* Title: Pure/PIDE/markup.scala
+ Module: Library
+ Author: Makarius
+
+Generic markup elements.
+*/
+
+package isabelle
+
+
+object Markup
+{
+ /* properties */
+
+ val NAME = "name"
+ val Name = new Properties.String(NAME)
+
+ val KIND = "kind"
+ val Kind = new Properties.String(KIND)
+
+
+ /* elements */
+
+ val Empty = Markup("", Nil)
+ val Data = Markup("data", Nil)
+ val Broken = Markup("broken", Nil)
+
+
+ /* timing */
+
+ val TIMING = "timing"
+ val ELAPSED = "elapsed"
+ val CPU = "cpu"
+ val GC = "gc"
+
+ object Timing
+ {
+ def apply(timing: isabelle.Timing): Markup =
+ Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
+ (CPU, Properties.Value.Double(timing.cpu.seconds)),
+ (GC, Properties.Value.Double(timing.gc.seconds))))
+ def unapply(markup: Markup): Option[isabelle.Timing] =
+ markup match {
+ case Markup(TIMING, List(
+ (ELAPSED, Properties.Value.Double(elapsed)),
+ (CPU, Properties.Value.Double(cpu)),
+ (GC, Properties.Value.Double(gc)))) =>
+ Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
+ case _ => None
+ }
+ }
+}
+
+
+sealed case class Markup(name: String, properties: Properties.T)
+