more uniform Properties in ML and Scala;
authorwenzelm
Tue Jul 12 19:36:46 2011 +0200 (2011-07-12)
changeset 437802cb2310d68b6
parent 43779 47bec02c6762
child 43781 d43e5f79bdc2
more uniform Properties in ML and Scala;
src/Pure/General/markup.scala
src/Pure/General/position.scala
src/Pure/General/properties.ML
src/Pure/General/properties.scala
src/Pure/General/xml.scala
src/Pure/PIDE/document.scala
src/Pure/System/isabelle_process.scala
src/Pure/build-jars
src/Pure/more_thm.ML
     1.1 --- a/src/Pure/General/markup.scala	Tue Jul 12 18:00:05 2011 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Tue Jul 12 19:36:46 2011 +0200
     1.3 @@ -9,73 +9,6 @@
     1.4  
     1.5  object Markup
     1.6  {
     1.7 -  /* plain values */
     1.8 -
     1.9 -  object Int
    1.10 -  {
    1.11 -    def apply(x: scala.Int): String = x.toString
    1.12 -    def unapply(s: String): Option[scala.Int] =
    1.13 -      try { Some(Integer.parseInt(s)) }
    1.14 -      catch { case _: NumberFormatException => None }
    1.15 -  }
    1.16 -
    1.17 -  object Long
    1.18 -  {
    1.19 -    def apply(x: scala.Long): String = x.toString
    1.20 -    def unapply(s: String): Option[scala.Long] =
    1.21 -      try { Some(java.lang.Long.parseLong(s)) }
    1.22 -      catch { case _: NumberFormatException => None }
    1.23 -  }
    1.24 -
    1.25 -  object Double
    1.26 -  {
    1.27 -    def apply(x: scala.Double): String = x.toString
    1.28 -    def unapply(s: String): Option[scala.Double] =
    1.29 -      try { Some(java.lang.Double.parseDouble(s)) }
    1.30 -      catch { case _: NumberFormatException => None }
    1.31 -  }
    1.32 -
    1.33 -
    1.34 -  /* named properties */
    1.35 -
    1.36 -  class Property(val name: String)
    1.37 -  {
    1.38 -    def apply(value: String): List[(String, String)] = List((name, value))
    1.39 -    def unapply(props: List[(String, String)]): Option[String] =
    1.40 -      props.find(_._1 == name).map(_._2)
    1.41 -  }
    1.42 -
    1.43 -  class Int_Property(name: String)
    1.44 -  {
    1.45 -    def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
    1.46 -    def unapply(props: List[(String, String)]): Option[Int] =
    1.47 -      props.find(_._1 == name) match {
    1.48 -        case None => None
    1.49 -        case Some((_, value)) => Int.unapply(value)
    1.50 -      }
    1.51 -  }
    1.52 -
    1.53 -  class Long_Property(name: String)
    1.54 -  {
    1.55 -    def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
    1.56 -    def unapply(props: List[(String, String)]): Option[Long] =
    1.57 -      props.find(_._1 == name) match {
    1.58 -        case None => None
    1.59 -        case Some((_, value)) => Long.unapply(value)
    1.60 -      }
    1.61 -  }
    1.62 -
    1.63 -  class Double_Property(name: String)
    1.64 -  {
    1.65 -    def apply(value: scala.Double): List[(String, String)] = List((name, Double(value)))
    1.66 -    def unapply(props: List[(String, String)]): Option[Double] =
    1.67 -      props.find(_._1 == name) match {
    1.68 -        case None => None
    1.69 -        case Some((_, value)) => Double.unapply(value)
    1.70 -      }
    1.71 -  }
    1.72 -
    1.73 -
    1.74    /* empty */
    1.75  
    1.76    val Empty = Markup("", Nil)
    1.77 @@ -84,10 +17,10 @@
    1.78    /* misc properties */
    1.79  
    1.80    val NAME = "name"
    1.81 -  val Name = new Property(NAME)
    1.82 +  val Name = new Properties.String(NAME)
    1.83  
    1.84    val KIND = "kind"
    1.85 -  val Kind = new Property(KIND)
    1.86 +  val Kind = new Properties.String(KIND)
    1.87  
    1.88  
    1.89    /* formal entities */
    1.90 @@ -145,9 +78,9 @@
    1.91  
    1.92    /* pretty printing */
    1.93  
    1.94 -  val Indent = new Int_Property("indent")
    1.95 +  val Indent = new Properties.Int("indent")
    1.96    val BLOCK = "block"
    1.97 -  val Width = new Int_Property("width")
    1.98 +  val Width = new Properties.Int("width")
    1.99    val BREAK = "break"
   1.100  
   1.101  
   1.102 @@ -260,13 +193,15 @@
   1.103    {
   1.104      def apply(timing: isabelle.Timing): Markup =
   1.105        Markup(TIMING, List(
   1.106 -        (ELAPSED, Double(timing.elapsed.seconds)),
   1.107 -        (CPU, Double(timing.cpu.seconds)),
   1.108 -        (GC, Double(timing.gc.seconds))))
   1.109 +        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
   1.110 +        (CPU, Properties.Value.Double(timing.cpu.seconds)),
   1.111 +        (GC, Properties.Value.Double(timing.gc.seconds))))
   1.112      def unapply(markup: Markup): Option[isabelle.Timing] =
   1.113        markup match {
   1.114          case Markup(TIMING, List(
   1.115 -          (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
   1.116 +          (ELAPSED, Properties.Value.Double(elapsed)),
   1.117 +          (CPU, Properties.Value.Double(cpu)),
   1.118 +          (GC, Properties.Value.Double(gc)))) =>
   1.119              Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
   1.120          case _ => None
   1.121        }
   1.122 @@ -310,7 +245,7 @@
   1.123  
   1.124    /* messages */
   1.125  
   1.126 -  val Serial = new Long_Property("serial")
   1.127 +  val Serial = new Properties.Long("serial")
   1.128  
   1.129    val MESSAGE = "message"
   1.130  
   1.131 @@ -336,12 +271,12 @@
   1.132    /* raw message functions */
   1.133  
   1.134    val FUNCTION = "function"
   1.135 -  val Function = new Property(FUNCTION)
   1.136 +  val Function = new Properties.String(FUNCTION)
   1.137  
   1.138    val INVOKE_SCALA = "invoke_scala"
   1.139    object Invoke_Scala
   1.140    {
   1.141 -    def unapply(props: List[(String, String)]): Option[(String, String)] =
   1.142 +    def unapply(props: Properties.T): Option[(String, String)] =
   1.143        props match {
   1.144          case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
   1.145          case _ => None
   1.146 @@ -354,4 +289,4 @@
   1.147    val Data = Markup("data", Nil)
   1.148  }
   1.149  
   1.150 -sealed case class Markup(name: String, properties: List[(String, String)])
   1.151 +sealed case class Markup(name: String, properties: Properties.T)
     2.1 --- a/src/Pure/General/position.scala	Tue Jul 12 18:00:05 2011 +0200
     2.2 +++ b/src/Pure/General/position.scala	Tue Jul 12 19:36:46 2011 +0200
     2.3 @@ -9,13 +9,13 @@
     2.4  
     2.5  object Position
     2.6  {
     2.7 -  type T = List[(String, String)]
     2.8 +  type T = Properties.T
     2.9  
    2.10 -  val Line = new Markup.Int_Property(Markup.LINE)
    2.11 -  val Offset = new Markup.Int_Property(Markup.OFFSET)
    2.12 -  val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
    2.13 -  val File = new Markup.Property(Markup.FILE)
    2.14 -  val Id = new Markup.Long_Property(Markup.ID)
    2.15 +  val Line = new Properties.Int(Markup.LINE)
    2.16 +  val Offset = new Properties.Int(Markup.OFFSET)
    2.17 +  val End_Offset = new Properties.Int(Markup.END_OFFSET)
    2.18 +  val File = new Properties.String(Markup.FILE)
    2.19 +  val Id = new Properties.Long(Markup.ID)
    2.20  
    2.21    object Range
    2.22    {
     3.1 --- a/src/Pure/General/properties.ML	Tue Jul 12 18:00:05 2011 +0200
     3.2 +++ b/src/Pure/General/properties.ML	Tue Jul 12 19:36:46 2011 +0200
     3.3 @@ -6,27 +6,30 @@
     3.4  
     3.5  signature PROPERTIES =
     3.6  sig
     3.7 -  type property = string * string
     3.8 -  type T = property list
     3.9 +  type entry = string * string
    3.10 +  type T = entry list
    3.11    val defined: T -> string -> bool
    3.12    val get: T -> string -> string option
    3.13    val get_int: T -> string -> int option
    3.14 -  val put: string * string -> T -> T
    3.15 +  val put: entry -> T -> T
    3.16 +  val put_int: string * int -> T -> T
    3.17    val remove: string -> T -> T
    3.18  end;
    3.19  
    3.20  structure Properties: PROPERTIES =
    3.21  struct
    3.22  
    3.23 -type property = string * string;
    3.24 -type T = property list;
    3.25 +type entry = string * string;
    3.26 +type T = entry list;
    3.27  
    3.28  fun defined (props: T) name = AList.defined (op =) props name;
    3.29  
    3.30  fun get (props: T) name = AList.lookup (op =) props name;
    3.31  fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
    3.32  
    3.33 -fun put prop (props: T) = AList.update (op =) prop props;
    3.34 +fun put entry (props: T) = AList.update (op =) entry props;
    3.35 +fun put_int (name, i) = put (name, signed_string_of_int i);
    3.36 +
    3.37  fun remove name (props: T) = AList.delete (op =) name props;
    3.38  
    3.39  end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/General/properties.scala	Tue Jul 12 19:36:46 2011 +0200
     4.3 @@ -0,0 +1,84 @@
     4.4 +/*  Title:      Pure/General/properties.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Property lists.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +object Properties
    4.14 +{
    4.15 +  /* plain values */
    4.16 +
    4.17 +  object Value
    4.18 +  {
    4.19 +    object Int
    4.20 +    {
    4.21 +      def apply(x: scala.Int): java.lang.String = x.toString
    4.22 +      def unapply(s: java.lang.String): Option[scala.Int] =
    4.23 +        try { Some(Integer.parseInt(s)) }
    4.24 +        catch { case _: NumberFormatException => None }
    4.25 +    }
    4.26 +
    4.27 +    object Long
    4.28 +    {
    4.29 +      def apply(x: scala.Long): java.lang.String = x.toString
    4.30 +      def unapply(s: java.lang.String): Option[scala.Long] =
    4.31 +        try { Some(java.lang.Long.parseLong(s)) }
    4.32 +        catch { case _: NumberFormatException => None }
    4.33 +    }
    4.34 +
    4.35 +    object Double
    4.36 +    {
    4.37 +      def apply(x: scala.Double): java.lang.String = x.toString
    4.38 +      def unapply(s: java.lang.String): Option[scala.Double] =
    4.39 +        try { Some(java.lang.Double.parseDouble(s)) }
    4.40 +        catch { case _: NumberFormatException => None }
    4.41 +    }
    4.42 +  }
    4.43 +
    4.44 +
    4.45 +  /* named entries */
    4.46 +
    4.47 +  type Entry = (java.lang.String, java.lang.String)
    4.48 +  type T = List[Entry]
    4.49 +
    4.50 +  class String(val name: java.lang.String)
    4.51 +  {
    4.52 +    def apply(value: java.lang.String): T = List((name, value))
    4.53 +    def unapply(props: T): Option[java.lang.String] =
    4.54 +      props.find(_._1 == name).map(_._2)
    4.55 +  }
    4.56 +
    4.57 +  class Int(name: java.lang.String)
    4.58 +  {
    4.59 +    def apply(value: scala.Int): T = List((name, Value.Int(value)))
    4.60 +    def unapply(props: T): Option[scala.Int] =
    4.61 +      props.find(_._1 == name) match {
    4.62 +        case None => None
    4.63 +        case Some((_, value)) => Value.Int.unapply(value)
    4.64 +      }
    4.65 +  }
    4.66 +
    4.67 +  class Long(name: java.lang.String)
    4.68 +  {
    4.69 +    def apply(value: scala.Long): T = List((name, Value.Long(value)))
    4.70 +    def unapply(props: T): Option[scala.Long] =
    4.71 +      props.find(_._1 == name) match {
    4.72 +        case None => None
    4.73 +        case Some((_, value)) => Value.Long.unapply(value)
    4.74 +      }
    4.75 +  }
    4.76 +
    4.77 +  class Double(name: java.lang.String)
    4.78 +  {
    4.79 +    def apply(value: scala.Double): T = List((name, Value.Double(value)))
    4.80 +    def unapply(props: T): Option[scala.Double] =
    4.81 +      props.find(_._1 == name) match {
    4.82 +        case None => None
    4.83 +        case Some((_, value)) => Value.Double.unapply(value)
    4.84 +      }
    4.85 +  }
    4.86 +}
    4.87 +
     5.1 --- a/src/Pure/General/xml.scala	Tue Jul 12 18:00:05 2011 +0200
     5.2 +++ b/src/Pure/General/xml.scala	Tue Jul 12 19:36:46 2011 +0200
     5.3 @@ -21,7 +21,7 @@
     5.4  
     5.5    /* datatype representation */
     5.6  
     5.7 -  type Attributes = List[(String, String)]
     5.8 +  type Attributes = Properties.T
     5.9  
    5.10    sealed abstract class Tree { override def toString = string_of_tree(this) }
    5.11    case class Elem(markup: Markup, body: List[Tree]) extends Tree
    5.12 @@ -118,7 +118,7 @@
    5.13              val z = trim_bytes(x)
    5.14              if (z.length > max_string) z else store(z)
    5.15          }
    5.16 -      def cache_props(x: List[(String, String)]): List[(String, String)] =
    5.17 +      def cache_props(x: Properties.T): Properties.T =
    5.18          if (x.isEmpty) x
    5.19          else
    5.20            lookup(x) match {
    5.21 @@ -232,7 +232,7 @@
    5.22  
    5.23      private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
    5.24  
    5.25 -    private def vector(xs: List[String]): List[(String, String)] =
    5.26 +    private def vector(xs: List[String]): Properties.T =
    5.27        xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
    5.28  
    5.29      private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
    5.30 @@ -241,7 +241,7 @@
    5.31  
    5.32      /* representation of standard types */
    5.33  
    5.34 -    val properties: T[List[(String, String)]] =
    5.35 +    val properties: T[Properties.T] =
    5.36        (props => List(XML.Elem(Markup(":", props), Nil)))
    5.37  
    5.38      val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
    5.39 @@ -310,7 +310,7 @@
    5.40          case _ => throw new XML_Body(List(t))
    5.41        }
    5.42  
    5.43 -    private def vector(props: List[(String, String)]): List[String] =
    5.44 +    private def vector(props: Properties.T): List[String] =
    5.45      {
    5.46        val xs = new mutable.ListBuffer[String]
    5.47        var i = 0
    5.48 @@ -330,7 +330,7 @@
    5.49  
    5.50      /* representation of standard types */
    5.51  
    5.52 -    val properties: T[List[(String, String)]] =
    5.53 +    val properties: T[Properties.T] =
    5.54      {
    5.55        case List(XML.Elem(Markup(":", props), Nil)) => props
    5.56        case ts => throw new XML_Body(ts)
     6.1 --- a/src/Pure/PIDE/document.scala	Tue Jul 12 18:00:05 2011 +0200
     6.2 +++ b/src/Pure/PIDE/document.scala	Tue Jul 12 19:36:46 2011 +0200
     6.3 @@ -16,12 +16,7 @@
     6.4    /* formal identifiers */
     6.5  
     6.6    type ID = Long
     6.7 -
     6.8 -  object ID
     6.9 -  {
    6.10 -    def apply(id: ID): String = Markup.Long.apply(id)
    6.11 -    def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
    6.12 -  }
    6.13 +  val ID = Properties.Value.Long
    6.14  
    6.15    type Version_ID = ID
    6.16    type Command_ID = ID
     7.1 --- a/src/Pure/System/isabelle_process.scala	Tue Jul 12 18:00:05 2011 +0200
     7.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Jul 12 19:36:46 2011 +0200
     7.3 @@ -46,7 +46,7 @@
     7.4    class Result(val message: XML.Elem) extends Message
     7.5    {
     7.6      def kind: String = message.markup.name
     7.7 -    def properties: XML.Attributes = message.markup.properties
     7.8 +    def properties: Properties.T = message.markup.properties
     7.9      def body: XML.Body = message.body
    7.10  
    7.11      def is_init = kind == Markup.INIT
    7.12 @@ -95,7 +95,7 @@
    7.13  
    7.14    private val xml_cache = new XML.Cache()
    7.15  
    7.16 -  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
    7.17 +  private def put_result(kind: String, props: Properties.T, body: XML.Body)
    7.18    {
    7.19      if (kind == Markup.INIT) rm_fifos()
    7.20      if (kind == Markup.RAW)
     8.1 --- a/src/Pure/build-jars	Tue Jul 12 18:00:05 2011 +0200
     8.2 +++ b/src/Pure/build-jars	Tue Jul 12 19:36:46 2011 +0200
     8.3 @@ -20,6 +20,7 @@
     8.4    General/path.scala
     8.5    General/position.scala
     8.6    General/pretty.scala
     8.7 +  General/properties.scala
     8.8    General/scan.scala
     8.9    General/sha1.scala
    8.10    General/symbol.scala
     9.1 --- a/src/Pure/more_thm.ML	Tue Jul 12 18:00:05 2011 +0200
     9.2 +++ b/src/Pure/more_thm.ML	Tue Jul 12 19:36:46 2011 +0200
     9.3 @@ -76,9 +76,9 @@
     9.4    val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
     9.5    val no_attributes: 'a -> 'a * 'b list
     9.6    val simple_fact: 'a -> ('a * 'b list) list
     9.7 -  val tag_rule: Properties.property -> thm -> thm
     9.8 +  val tag_rule: Properties.entry -> thm -> thm
     9.9    val untag_rule: string -> thm -> thm
    9.10 -  val tag: Properties.property -> attribute
    9.11 +  val tag: Properties.entry -> attribute
    9.12    val untag: string -> attribute
    9.13    val def_name: string -> string
    9.14    val def_name_optional: string -> string -> string