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