src/Pure/General/markup.scala
author wenzelm
Mon, 28 Nov 2011 22:05:32 +0100
changeset 45666 d83797ef0d2d
parent 45633 2cb7e34f6096
child 45667 546d78f0d81f
permissions -rw-r--r--
separate module for concrete Isabelle markup;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/markup.scala
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     3
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
     4
Generic markup elements.
27958
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     5
*/
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     6
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     7
package isabelle
292d78c906b1 Common markup elements.
wenzelm
parents:
diff changeset
     8
27970
3dd5fbdf61c4 added position, messages;
wenzelm
parents: 27958
diff changeset
     9
32450
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    10
object Markup
375db037f4d2 misc tuning;
wenzelm
parents: 31472
diff changeset
    11
{
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    12
  /* properties */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    13
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    14
  val NAME = "name"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    15
  val Name = new Properties.String(NAME)
42136
826168ae0213 added Markup.Name and Markup.Kind convenience;
wenzelm
parents: 41483
diff changeset
    16
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    17
  val KIND = "kind"
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    18
  val Kind = new Properties.String(KIND)
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    19
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    20
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    21
  /* elements */
29184
85889d58b5da more markup elements;
wenzelm
parents: 29140
diff changeset
    22
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    23
  val Empty = Markup("", Nil)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    24
  val Data = Markup("data", Nil)
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    25
  val Broken = Markup("broken", Nil)
43673
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43593
diff changeset
    26
29eb1cd29961 Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents: 43593
diff changeset
    27
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    28
  /* timing */
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    29
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    30
  val TIMING = "timing"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    31
  val ELAPSED = "elapsed"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    32
  val CPU = "cpu"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    33
  val GC = "gc"
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    34
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    35
  object Timing
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    36
  {
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    37
    def apply(timing: isabelle.Timing): Markup =
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    38
      Markup(TIMING, List(
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    39
        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    40
        (CPU, Properties.Value.Double(timing.cpu.seconds)),
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    41
        (GC, Properties.Value.Double(timing.gc.seconds))))
40394
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    42
    def unapply(markup: Markup): Option[isabelle.Timing] =
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    43
      markup match {
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    44
        case Markup(TIMING, List(
43780
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    45
          (ELAPSED, Properties.Value.Double(elapsed)),
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    46
          (CPU, Properties.Value.Double(cpu)),
2cb2310d68b6 more uniform Properties in ML and Scala;
wenzelm
parents: 43748
diff changeset
    47
          (GC, Properties.Value.Double(gc)))) =>
40848
8662b9b1f123 more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents: 40394
diff changeset
    48
            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
    49
        case _ => None
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    50
      }
6dcb6cbf0719 somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents: 40392
diff changeset
    51
  }
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    52
}
43721
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
    53
fad8634cee62 echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents: 43710
diff changeset
    54
45666
d83797ef0d2d separate module for concrete Isabelle markup;
wenzelm
parents: 45633
diff changeset
    55
sealed case class Markup(name: String, properties: Properties.T)
43748
c70bd78ec83c JVM method invocation service via Scala layer;
wenzelm
parents: 43746
diff changeset
    56