author | wenzelm |
Mon, 28 Nov 2011 22:18:19 +0100 | |
changeset 45667 | 546d78f0d81f |
parent 45666 | d83797ef0d2d |
permissions | -rw-r--r-- |
27958 | 1 |
/* Title: Pure/General/markup.scala |
45667
546d78f0d81f
explicit indication of modules for independent Scala library;
wenzelm
parents:
45666
diff
changeset
|
2 |
Module: Library |
27958 | 3 |
Author: Makarius |
4 |
||
45666 | 5 |
Generic markup elements. |
27958 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
27970 | 10 |
|
32450 | 11 |
object Markup |
12 |
{ |
|
45666 | 13 |
/* properties */ |
29184 | 14 |
|
15 |
val NAME = "name" |
|
43780 | 16 |
val Name = new Properties.String(NAME) |
42136 | 17 |
|
29184 | 18 |
val KIND = "kind" |
43780 | 19 |
val Kind = new Properties.String(KIND) |
29184 | 20 |
|
21 |
||
45666 | 22 |
/* elements */ |
29184 | 23 |
|
45666 | 24 |
val Empty = Markup("", Nil) |
25 |
val Data = Markup("data", Nil) |
|
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 | 40 |
(ELAPSED, Properties.Value.Double(timing.elapsed.seconds)), |
41 |
(CPU, Properties.Value.Double(timing.cpu.seconds)), |
|
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 | 46 |
(ELAPSED, Properties.Value.Double(elapsed)), |
47 |
(CPU, Properties.Value.Double(cpu)), |
|
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 | 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 | 56 |
sealed case class Markup(name: String, properties: Properties.T) |
43748 | 57 |