--- a/src/Pure/General/markup.scala Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/General/markup.scala Tue Jul 12 19:36:46 2011 +0200
@@ -9,73 +9,6 @@
object Markup
{
- /* plain values */
-
- object Int
- {
- def apply(x: scala.Int): String = x.toString
- def unapply(s: String): Option[scala.Int] =
- try { Some(Integer.parseInt(s)) }
- catch { case _: NumberFormatException => None }
- }
-
- object Long
- {
- def apply(x: scala.Long): String = x.toString
- def unapply(s: String): Option[scala.Long] =
- try { Some(java.lang.Long.parseLong(s)) }
- catch { case _: NumberFormatException => None }
- }
-
- object Double
- {
- def apply(x: scala.Double): String = x.toString
- def unapply(s: String): Option[scala.Double] =
- try { Some(java.lang.Double.parseDouble(s)) }
- catch { case _: NumberFormatException => None }
- }
-
-
- /* named properties */
-
- class Property(val name: String)
- {
- def apply(value: String): List[(String, String)] = List((name, value))
- def unapply(props: List[(String, String)]): Option[String] =
- props.find(_._1 == name).map(_._2)
- }
-
- class Int_Property(name: String)
- {
- def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
- def unapply(props: List[(String, String)]): Option[Int] =
- props.find(_._1 == name) match {
- case None => None
- case Some((_, value)) => Int.unapply(value)
- }
- }
-
- class Long_Property(name: String)
- {
- def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
- def unapply(props: List[(String, String)]): Option[Long] =
- props.find(_._1 == name) match {
- case None => None
- case Some((_, value)) => Long.unapply(value)
- }
- }
-
- class Double_Property(name: String)
- {
- def apply(value: scala.Double): List[(String, String)] = List((name, Double(value)))
- def unapply(props: List[(String, String)]): Option[Double] =
- props.find(_._1 == name) match {
- case None => None
- case Some((_, value)) => Double.unapply(value)
- }
- }
-
-
/* empty */
val Empty = Markup("", Nil)
@@ -84,10 +17,10 @@
/* misc properties */
val NAME = "name"
- val Name = new Property(NAME)
+ val Name = new Properties.String(NAME)
val KIND = "kind"
- val Kind = new Property(KIND)
+ val Kind = new Properties.String(KIND)
/* formal entities */
@@ -145,9 +78,9 @@
/* pretty printing */
- val Indent = new Int_Property("indent")
+ val Indent = new Properties.Int("indent")
val BLOCK = "block"
- val Width = new Int_Property("width")
+ val Width = new Properties.Int("width")
val BREAK = "break"
@@ -260,13 +193,15 @@
{
def apply(timing: isabelle.Timing): Markup =
Markup(TIMING, List(
- (ELAPSED, Double(timing.elapsed.seconds)),
- (CPU, Double(timing.cpu.seconds)),
- (GC, Double(timing.gc.seconds))))
+ (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, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
+ (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
}
@@ -310,7 +245,7 @@
/* messages */
- val Serial = new Long_Property("serial")
+ val Serial = new Properties.Long("serial")
val MESSAGE = "message"
@@ -336,12 +271,12 @@
/* raw message functions */
val FUNCTION = "function"
- val Function = new Property(FUNCTION)
+ val Function = new Properties.String(FUNCTION)
val INVOKE_SCALA = "invoke_scala"
object Invoke_Scala
{
- def unapply(props: List[(String, String)]): Option[(String, String)] =
+ def unapply(props: Properties.T): Option[(String, String)] =
props match {
case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
case _ => None
@@ -354,4 +289,4 @@
val Data = Markup("data", Nil)
}
-sealed case class Markup(name: String, properties: List[(String, String)])
+sealed case class Markup(name: String, properties: Properties.T)
--- a/src/Pure/General/position.scala Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/General/position.scala Tue Jul 12 19:36:46 2011 +0200
@@ -9,13 +9,13 @@
object Position
{
- type T = List[(String, String)]
+ type T = Properties.T
- val Line = new Markup.Int_Property(Markup.LINE)
- val Offset = new Markup.Int_Property(Markup.OFFSET)
- val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
- val File = new Markup.Property(Markup.FILE)
- val Id = new Markup.Long_Property(Markup.ID)
+ val Line = new Properties.Int(Markup.LINE)
+ val Offset = new Properties.Int(Markup.OFFSET)
+ val End_Offset = new Properties.Int(Markup.END_OFFSET)
+ val File = new Properties.String(Markup.FILE)
+ val Id = new Properties.Long(Markup.ID)
object Range
{
--- a/src/Pure/General/properties.ML Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/General/properties.ML Tue Jul 12 19:36:46 2011 +0200
@@ -6,27 +6,30 @@
signature PROPERTIES =
sig
- type property = string * string
- type T = property list
+ type entry = string * string
+ type T = entry list
val defined: T -> string -> bool
val get: T -> string -> string option
val get_int: T -> string -> int option
- val put: string * string -> T -> T
+ val put: entry -> T -> T
+ val put_int: string * int -> T -> T
val remove: string -> T -> T
end;
structure Properties: PROPERTIES =
struct
-type property = string * string;
-type T = property list;
+type entry = string * string;
+type T = entry list;
fun defined (props: T) name = AList.defined (op =) props name;
fun get (props: T) name = AList.lookup (op =) props name;
fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
-fun put prop (props: T) = AList.update (op =) prop props;
+fun put entry (props: T) = AList.update (op =) entry props;
+fun put_int (name, i) = put (name, signed_string_of_int i);
+
fun remove name (props: T) = AList.delete (op =) name props;
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/properties.scala Tue Jul 12 19:36:46 2011 +0200
@@ -0,0 +1,84 @@
+/* Title: Pure/General/properties.scala
+ Author: Makarius
+
+Property lists.
+*/
+
+package isabelle
+
+
+object Properties
+{
+ /* plain values */
+
+ object Value
+ {
+ object Int
+ {
+ def apply(x: scala.Int): java.lang.String = x.toString
+ def unapply(s: java.lang.String): Option[scala.Int] =
+ try { Some(Integer.parseInt(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+
+ object Long
+ {
+ def apply(x: scala.Long): java.lang.String = x.toString
+ def unapply(s: java.lang.String): Option[scala.Long] =
+ try { Some(java.lang.Long.parseLong(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+
+ object Double
+ {
+ def apply(x: scala.Double): java.lang.String = x.toString
+ def unapply(s: java.lang.String): Option[scala.Double] =
+ try { Some(java.lang.Double.parseDouble(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+ }
+
+
+ /* named entries */
+
+ type Entry = (java.lang.String, java.lang.String)
+ type T = List[Entry]
+
+ class String(val name: java.lang.String)
+ {
+ def apply(value: java.lang.String): T = List((name, value))
+ def unapply(props: T): Option[java.lang.String] =
+ props.find(_._1 == name).map(_._2)
+ }
+
+ class Int(name: java.lang.String)
+ {
+ def apply(value: scala.Int): T = List((name, Value.Int(value)))
+ def unapply(props: T): Option[scala.Int] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Value.Int.unapply(value)
+ }
+ }
+
+ class Long(name: java.lang.String)
+ {
+ def apply(value: scala.Long): T = List((name, Value.Long(value)))
+ def unapply(props: T): Option[scala.Long] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Value.Long.unapply(value)
+ }
+ }
+
+ class Double(name: java.lang.String)
+ {
+ def apply(value: scala.Double): T = List((name, Value.Double(value)))
+ def unapply(props: T): Option[scala.Double] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Value.Double.unapply(value)
+ }
+ }
+}
+
--- a/src/Pure/General/xml.scala Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/General/xml.scala Tue Jul 12 19:36:46 2011 +0200
@@ -21,7 +21,7 @@
/* datatype representation */
- type Attributes = List[(String, String)]
+ type Attributes = Properties.T
sealed abstract class Tree { override def toString = string_of_tree(this) }
case class Elem(markup: Markup, body: List[Tree]) extends Tree
@@ -118,7 +118,7 @@
val z = trim_bytes(x)
if (z.length > max_string) z else store(z)
}
- def cache_props(x: List[(String, String)]): List[(String, String)] =
+ def cache_props(x: Properties.T): Properties.T =
if (x.isEmpty) x
else
lookup(x) match {
@@ -232,7 +232,7 @@
private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
- private def vector(xs: List[String]): List[(String, String)] =
+ private def vector(xs: List[String]): Properties.T =
xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
@@ -241,7 +241,7 @@
/* representation of standard types */
- val properties: T[List[(String, String)]] =
+ val properties: T[Properties.T] =
(props => List(XML.Elem(Markup(":", props), Nil)))
val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
@@ -310,7 +310,7 @@
case _ => throw new XML_Body(List(t))
}
- private def vector(props: List[(String, String)]): List[String] =
+ private def vector(props: Properties.T): List[String] =
{
val xs = new mutable.ListBuffer[String]
var i = 0
@@ -330,7 +330,7 @@
/* representation of standard types */
- val properties: T[List[(String, String)]] =
+ val properties: T[Properties.T] =
{
case List(XML.Elem(Markup(":", props), Nil)) => props
case ts => throw new XML_Body(ts)
--- a/src/Pure/PIDE/document.scala Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/PIDE/document.scala Tue Jul 12 19:36:46 2011 +0200
@@ -16,12 +16,7 @@
/* formal identifiers */
type ID = Long
-
- object ID
- {
- def apply(id: ID): String = Markup.Long.apply(id)
- def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
- }
+ val ID = Properties.Value.Long
type Version_ID = ID
type Command_ID = ID
--- a/src/Pure/System/isabelle_process.scala Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala Tue Jul 12 19:36:46 2011 +0200
@@ -46,7 +46,7 @@
class Result(val message: XML.Elem) extends Message
{
def kind: String = message.markup.name
- def properties: XML.Attributes = message.markup.properties
+ def properties: Properties.T = message.markup.properties
def body: XML.Body = message.body
def is_init = kind == Markup.INIT
@@ -95,7 +95,7 @@
private val xml_cache = new XML.Cache()
- private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
+ private def put_result(kind: String, props: Properties.T, body: XML.Body)
{
if (kind == Markup.INIT) rm_fifos()
if (kind == Markup.RAW)
--- a/src/Pure/build-jars Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/build-jars Tue Jul 12 19:36:46 2011 +0200
@@ -20,6 +20,7 @@
General/path.scala
General/position.scala
General/pretty.scala
+ General/properties.scala
General/scan.scala
General/sha1.scala
General/symbol.scala
--- a/src/Pure/more_thm.ML Tue Jul 12 18:00:05 2011 +0200
+++ b/src/Pure/more_thm.ML Tue Jul 12 19:36:46 2011 +0200
@@ -76,9 +76,9 @@
val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
val no_attributes: 'a -> 'a * 'b list
val simple_fact: 'a -> ('a * 'b list) list
- val tag_rule: Properties.property -> thm -> thm
+ val tag_rule: Properties.entry -> thm -> thm
val untag_rule: string -> thm -> thm
- val tag: Properties.property -> attribute
+ val tag: Properties.entry -> attribute
val untag: string -> attribute
val def_name: string -> string
val def_name_optional: string -> string -> string