merged
authorwenzelm
Tue Jul 12 20:53:14 2011 +0200 (2011-07-12)
changeset 43788e84239a47f32
parent 43787 5be84619e4d4
parent 43784 c3b6374278fa
child 43789 321ebd051897
merged
src/Pure/General/xml_data.ML
src/Pure/General/xml_data.scala
src/Pure/Isar/parse_value.ML
src/Pure/System/isabelle_syntax.scala
     1.1 --- a/lib/fonts/IsabelleText.sfd	Wed Jul 13 00:43:07 2011 +0900
     1.2 +++ b/lib/fonts/IsabelleText.sfd	Tue Jul 12 20:53:14 2011 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  OS2_WeightWidthSlopeOnly: 0
     1.5  OS2_UseTypoMetrics: 1
     1.6  CreationTime: 1050361371
     1.7 -ModificationTime: 1308688123
     1.8 +ModificationTime: 1310461984
     1.9  PfmFamily: 17
    1.10  TTFWeight: 400
    1.11  TTFWidth: 5
    1.12 @@ -2241,9 +2241,9 @@
    1.13  DisplaySize: -48
    1.14  AntiAlias: 1
    1.15  FitToEm: 1
    1.16 -WinInfo: 8608 16 10
    1.17 +WinInfo: 0 16 10
    1.18  TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
    1.19 -BeginChars: 1114189 1090
    1.20 +BeginChars: 1114189 1094
    1.21  
    1.22  StartChar: u10000
    1.23  Encoding: 65536 65536 0
    1.24 @@ -55412,7 +55412,7 @@
    1.25  StartChar: uni21D6
    1.26  Encoding: 8662 8662 1086
    1.27  Width: 1233
    1.28 -Flags: HW
    1.29 +Flags: W
    1.30  LayerCount: 2
    1.31  Fore
    1.32  SplineSet
    1.33 @@ -55438,7 +55438,7 @@
    1.34  StartChar: uni21D7
    1.35  Encoding: 8663 8663 1087
    1.36  Width: 1233
    1.37 -Flags: HW
    1.38 +Flags: W
    1.39  LayerCount: 2
    1.40  Fore
    1.41  SplineSet
    1.42 @@ -55464,7 +55464,7 @@
    1.43  StartChar: uni21D8
    1.44  Encoding: 8664 8664 1088
    1.45  Width: 1233
    1.46 -Flags: HW
    1.47 +Flags: W
    1.48  LayerCount: 2
    1.49  Fore
    1.50  SplineSet
    1.51 @@ -55490,7 +55490,7 @@
    1.52  StartChar: uni21D9
    1.53  Encoding: 8665 8665 1089
    1.54  Width: 1233
    1.55 -Flags: HW
    1.56 +Flags: W
    1.57  LayerCount: 2
    1.58  Fore
    1.59  SplineSet
    1.60 @@ -55512,5 +55512,103 @@
    1.61   398 127 l 1,0,-1
    1.62  EndSplineSet
    1.63  EndChar
    1.64 +
    1.65 +StartChar: uni0005
    1.66 +Encoding: 5 5 1090
    1.67 +Width: 1233
    1.68 +Flags: W
    1.69 +LayerCount: 2
    1.70 +Fore
    1.71 +SplineSet
    1.72 +1071 0 m 1,0,-1
    1.73 + 780 0 l 1,1,-1
    1.74 + 580 512 l 1,2,-1
    1.75 + 180 0 l 1,3,-1
    1.76 + -143 0 l 1,4,-1
    1.77 + 471 782 l 1,5,-1
    1.78 + 184 1493 l 1,6,-1
    1.79 + 475 1493 l 1,7,-1
    1.80 + 662 1030 l 1,8,-1
    1.81 + 1022 1493 l 1,9,-1
    1.82 + 1343 1493 l 1,10,-1
    1.83 + 770 756 l 1,11,-1
    1.84 + 1071 0 l 1,0,-1
    1.85 +EndSplineSet
    1.86 +EndChar
    1.87 +
    1.88 +StartChar: uni0006
    1.89 +Encoding: 6 6 1091
    1.90 +Width: 1233
    1.91 +Flags: W
    1.92 +LayerCount: 2
    1.93 +Fore
    1.94 +SplineSet
    1.95 +145 1493 m 1,0,-1
    1.96 + 438 1493 l 1,1,-1
    1.97 + 625 844 l 1,2,-1
    1.98 + 1036 1493 l 1,3,-1
    1.99 + 1358 1493 l 1,4,-1
   1.100 + 725 588 l 1,5,-1
   1.101 + 610 0 l 1,6,-1
   1.102 + 317 0 l 1,7,-1
   1.103 + 432 588 l 1,8,-1
   1.104 + 145 1493 l 1,0,-1
   1.105 +EndSplineSet
   1.106 +EndChar
   1.107 +
   1.108 +StartChar: uni007F
   1.109 +Encoding: 127 127 1092
   1.110 +Width: 1233
   1.111 +Flags: W
   1.112 +LayerCount: 2
   1.113 +Fore
   1.114 +SplineSet
   1.115 +994 410 m 1,0,-1
   1.116 + 994 983 l 1,1,-1
   1.117 + 886.193 983 l 1,2,-1
   1.118 + 685.584 696.5 l 1,3,-1
   1.119 + 886.193 410 l 1,4,-1
   1.120 + 994 410 l 1,0,-1
   1.121 +1108 296 m 1,5,-1
   1.122 + 125 296 l 1,6,-1
   1.123 + 125 1097 l 1,7,-1
   1.124 + 1108 1097 l 1,8,-1
   1.125 + 1108 296 l 1,5,-1
   1.126 +484.976 983 m 1,9,-1
   1.127 + 616 795.877 l 1,10,-1
   1.128 + 747.024 983 l 1,11,-1
   1.129 + 484.976 983 l 1,9,-1
   1.130 +345.807 983 m 1,12,-1
   1.131 + 239 983 l 1,13,-1
   1.132 + 239 410 l 1,14,-1
   1.133 + 345.807 410 l 1,15,-1
   1.134 + 546.416 696.5 l 1,16,-1
   1.135 + 345.807 983 l 1,12,-1
   1.136 +747.024 410 m 1,17,-1
   1.137 + 616 597.123 l 1,18,-1
   1.138 + 484.976 410 l 1,19,-1
   1.139 + 747.024 410 l 1,17,-1
   1.140 +EndSplineSet
   1.141 +EndChar
   1.142 +
   1.143 +StartChar: uni0007
   1.144 +Encoding: 7 7 1093
   1.145 +Width: 1233
   1.146 +Flags: HW
   1.147 +LayerCount: 2
   1.148 +Fore
   1.149 +SplineSet
   1.150 +104 -362 m 1,0,-1
   1.151 + 104 1444 l 1,1,-1
   1.152 + 1128 1444 l 1,2,-1
   1.153 + 1128 -362 l 1,3,-1
   1.154 + 104 -362 l 1,0,-1
   1.155 +219 -248 m 1,4,-1
   1.156 + 1014 -248 l 1,5,-1
   1.157 + 1014 1329 l 1,6,-1
   1.158 + 219 1329 l 1,7,-1
   1.159 + 219 -248 l 1,4,-1
   1.160 +EndSplineSet
   1.161 +EndChar
   1.162  EndChars
   1.163  EndSplineFont
     2.1 Binary file lib/fonts/IsabelleText.ttf has changed
     3.1 --- a/lib/fonts/IsabelleTextBold.sfd	Wed Jul 13 00:43:07 2011 +0900
     3.2 +++ b/lib/fonts/IsabelleTextBold.sfd	Tue Jul 12 20:53:14 2011 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4  OS2_WeightWidthSlopeOnly: 0
     3.5  OS2_UseTypoMetrics: 1
     3.6  CreationTime: 1050374980
     3.7 -ModificationTime: 1308688237
     3.8 +ModificationTime: 1310462018
     3.9  PfmFamily: 17
    3.10  TTFWeight: 700
    3.11  TTFWidth: 5
    3.12 @@ -1675,8 +1675,8 @@
    3.13  DisplaySize: -48
    3.14  AntiAlias: 1
    3.15  FitToEm: 1
    3.16 -WinInfo: 8576 16 10
    3.17 -BeginChars: 1114112 1079
    3.18 +WinInfo: 0 16 10
    3.19 +BeginChars: 1114112 1083
    3.20  
    3.21  StartChar: u10000
    3.22  Encoding: 65536 65536 0
    3.23 @@ -58428,7 +58428,7 @@
    3.24  StartChar: uni21D6
    3.25  Encoding: 8662 8662 1075
    3.26  Width: 1233
    3.27 -Flags: HW
    3.28 +Flags: W
    3.29  LayerCount: 2
    3.30  Fore
    3.31  SplineSet
    3.32 @@ -58454,7 +58454,7 @@
    3.33  StartChar: uni21D7
    3.34  Encoding: 8663 8663 1076
    3.35  Width: 1233
    3.36 -Flags: HW
    3.37 +Flags: W
    3.38  LayerCount: 2
    3.39  Fore
    3.40  SplineSet
    3.41 @@ -58480,7 +58480,7 @@
    3.42  StartChar: uni21D8
    3.43  Encoding: 8664 8664 1077
    3.44  Width: 1233
    3.45 -Flags: HW
    3.46 +Flags: W
    3.47  LayerCount: 2
    3.48  Fore
    3.49  SplineSet
    3.50 @@ -58506,7 +58506,7 @@
    3.51  StartChar: uni21D9
    3.52  Encoding: 8665 8665 1078
    3.53  Width: 1233
    3.54 -Flags: HW
    3.55 +Flags: W
    3.56  LayerCount: 2
    3.57  Fore
    3.58  SplineSet
    3.59 @@ -58528,5 +58528,103 @@
    3.60   312 243 l 1,0,-1
    3.61  EndSplineSet
    3.62  EndChar
    3.63 +
    3.64 +StartChar: uni0005
    3.65 +Encoding: 5 5 1079
    3.66 +Width: 1233
    3.67 +Flags: W
    3.68 +LayerCount: 2
    3.69 +Fore
    3.70 +SplineSet
    3.71 +1071 0 m 1,0,-1
    3.72 + 780 0 l 1,1,-1
    3.73 + 580 512 l 1,2,-1
    3.74 + 180 0 l 1,3,-1
    3.75 + -143 0 l 1,4,-1
    3.76 + 471 782 l 1,5,-1
    3.77 + 184 1493 l 1,6,-1
    3.78 + 475 1493 l 1,7,-1
    3.79 + 662 1030 l 1,8,-1
    3.80 + 1022 1493 l 1,9,-1
    3.81 + 1343 1493 l 1,10,-1
    3.82 + 770 756 l 1,11,-1
    3.83 + 1071 0 l 1,0,-1
    3.84 +EndSplineSet
    3.85 +EndChar
    3.86 +
    3.87 +StartChar: uni0006
    3.88 +Encoding: 6 6 1080
    3.89 +Width: 1233
    3.90 +Flags: W
    3.91 +LayerCount: 2
    3.92 +Fore
    3.93 +SplineSet
    3.94 +145 1493 m 1,0,-1
    3.95 + 438 1493 l 1,1,-1
    3.96 + 625 844 l 1,2,-1
    3.97 + 1036 1493 l 1,3,-1
    3.98 + 1358 1493 l 1,4,-1
    3.99 + 725 588 l 1,5,-1
   3.100 + 610 0 l 1,6,-1
   3.101 + 317 0 l 1,7,-1
   3.102 + 432 588 l 1,8,-1
   3.103 + 145 1493 l 1,0,-1
   3.104 +EndSplineSet
   3.105 +EndChar
   3.106 +
   3.107 +StartChar: uni007F
   3.108 +Encoding: 127 127 1081
   3.109 +Width: 1233
   3.110 +Flags: W
   3.111 +LayerCount: 2
   3.112 +Fore
   3.113 +SplineSet
   3.114 +1138 296 m 1,0,-1
   3.115 + 95 296 l 1,1,-1
   3.116 + 95 1097 l 1,2,-1
   3.117 + 1138 1097 l 1,3,-1
   3.118 + 1138 296 l 1,0,-1
   3.119 +994 440 m 1,4,-1
   3.120 + 994 953 l 1,5,-1
   3.121 + 875.188 953 l 1,6,-1
   3.122 + 695.584 696.5 l 1,7,-1
   3.123 + 875.188 440 l 1,8,-1
   3.124 + 994 440 l 1,4,-1
   3.125 +515.981 953 m 1,9,-1
   3.126 + 616 810.158 l 1,10,-1
   3.127 + 716.019 953 l 1,11,-1
   3.128 + 515.981 953 l 1,9,-1
   3.129 +239 440 m 1,12,-1
   3.130 + 356.812 440 l 1,13,-1
   3.131 + 536.416 696.5 l 1,14,-1
   3.132 + 356.812 953 l 1,15,-1
   3.133 + 239 953 l 1,16,-1
   3.134 + 239 440 l 1,12,-1
   3.135 +716.019 440 m 1,17,-1
   3.136 + 616 582.842 l 1,18,-1
   3.137 + 515.981 440 l 1,19,-1
   3.138 + 716.019 440 l 1,17,-1
   3.139 +EndSplineSet
   3.140 +EndChar
   3.141 +
   3.142 +StartChar: uni0007
   3.143 +Encoding: 7 7 1082
   3.144 +Width: 1233
   3.145 +Flags: HW
   3.146 +LayerCount: 2
   3.147 +Fore
   3.148 +SplineSet
   3.149 +104 -362 m 1,0,-1
   3.150 + 104 1444 l 1,1,-1
   3.151 + 1128 1444 l 1,2,-1
   3.152 + 1128 -362 l 1,3,-1
   3.153 + 104 -362 l 1,0,-1
   3.154 +219 -248 m 1,4,-1
   3.155 + 1014 -248 l 1,5,-1
   3.156 + 1014 1329 l 1,6,-1
   3.157 + 219 1329 l 1,7,-1
   3.158 + 219 -248 l 1,4,-1
   3.159 +EndSplineSet
   3.160 +EndChar
   3.161  EndChars
   3.162  EndSplineFont
     4.1 Binary file lib/fonts/IsabelleTextBold.ttf has changed
     5.1 --- a/src/Pure/General/markup.scala	Wed Jul 13 00:43:07 2011 +0900
     5.2 +++ b/src/Pure/General/markup.scala	Tue Jul 12 20:53:14 2011 +0200
     5.3 @@ -9,73 +9,6 @@
     5.4  
     5.5  object Markup
     5.6  {
     5.7 -  /* plain values */
     5.8 -
     5.9 -  object Int
    5.10 -  {
    5.11 -    def apply(x: scala.Int): String = x.toString
    5.12 -    def unapply(s: String): Option[scala.Int] =
    5.13 -      try { Some(Integer.parseInt(s)) }
    5.14 -      catch { case _: NumberFormatException => None }
    5.15 -  }
    5.16 -
    5.17 -  object Long
    5.18 -  {
    5.19 -    def apply(x: scala.Long): String = x.toString
    5.20 -    def unapply(s: String): Option[scala.Long] =
    5.21 -      try { Some(java.lang.Long.parseLong(s)) }
    5.22 -      catch { case _: NumberFormatException => None }
    5.23 -  }
    5.24 -
    5.25 -  object Double
    5.26 -  {
    5.27 -    def apply(x: scala.Double): String = x.toString
    5.28 -    def unapply(s: String): Option[scala.Double] =
    5.29 -      try { Some(java.lang.Double.parseDouble(s)) }
    5.30 -      catch { case _: NumberFormatException => None }
    5.31 -  }
    5.32 -
    5.33 -
    5.34 -  /* named properties */
    5.35 -
    5.36 -  class Property(val name: String)
    5.37 -  {
    5.38 -    def apply(value: String): List[(String, String)] = List((name, value))
    5.39 -    def unapply(props: List[(String, String)]): Option[String] =
    5.40 -      props.find(_._1 == name).map(_._2)
    5.41 -  }
    5.42 -
    5.43 -  class Int_Property(name: String)
    5.44 -  {
    5.45 -    def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
    5.46 -    def unapply(props: List[(String, String)]): Option[Int] =
    5.47 -      props.find(_._1 == name) match {
    5.48 -        case None => None
    5.49 -        case Some((_, value)) => Int.unapply(value)
    5.50 -      }
    5.51 -  }
    5.52 -
    5.53 -  class Long_Property(name: String)
    5.54 -  {
    5.55 -    def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
    5.56 -    def unapply(props: List[(String, String)]): Option[Long] =
    5.57 -      props.find(_._1 == name) match {
    5.58 -        case None => None
    5.59 -        case Some((_, value)) => Long.unapply(value)
    5.60 -      }
    5.61 -  }
    5.62 -
    5.63 -  class Double_Property(name: String)
    5.64 -  {
    5.65 -    def apply(value: scala.Double): List[(String, String)] = List((name, Double(value)))
    5.66 -    def unapply(props: List[(String, String)]): Option[Double] =
    5.67 -      props.find(_._1 == name) match {
    5.68 -        case None => None
    5.69 -        case Some((_, value)) => Double.unapply(value)
    5.70 -      }
    5.71 -  }
    5.72 -
    5.73 -
    5.74    /* empty */
    5.75  
    5.76    val Empty = Markup("", Nil)
    5.77 @@ -84,10 +17,10 @@
    5.78    /* misc properties */
    5.79  
    5.80    val NAME = "name"
    5.81 -  val Name = new Property(NAME)
    5.82 +  val Name = new Properties.String(NAME)
    5.83  
    5.84    val KIND = "kind"
    5.85 -  val Kind = new Property(KIND)
    5.86 +  val Kind = new Properties.String(KIND)
    5.87  
    5.88  
    5.89    /* formal entities */
    5.90 @@ -145,9 +78,9 @@
    5.91  
    5.92    /* pretty printing */
    5.93  
    5.94 -  val Indent = new Int_Property("indent")
    5.95 +  val Indent = new Properties.Int("indent")
    5.96    val BLOCK = "block"
    5.97 -  val Width = new Int_Property("width")
    5.98 +  val Width = new Properties.Int("width")
    5.99    val BREAK = "break"
   5.100  
   5.101  
   5.102 @@ -260,13 +193,15 @@
   5.103    {
   5.104      def apply(timing: isabelle.Timing): Markup =
   5.105        Markup(TIMING, List(
   5.106 -        (ELAPSED, Double(timing.elapsed.seconds)),
   5.107 -        (CPU, Double(timing.cpu.seconds)),
   5.108 -        (GC, Double(timing.gc.seconds))))
   5.109 +        (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
   5.110 +        (CPU, Properties.Value.Double(timing.cpu.seconds)),
   5.111 +        (GC, Properties.Value.Double(timing.gc.seconds))))
   5.112      def unapply(markup: Markup): Option[isabelle.Timing] =
   5.113        markup match {
   5.114          case Markup(TIMING, List(
   5.115 -          (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
   5.116 +          (ELAPSED, Properties.Value.Double(elapsed)),
   5.117 +          (CPU, Properties.Value.Double(cpu)),
   5.118 +          (GC, Properties.Value.Double(gc)))) =>
   5.119              Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
   5.120          case _ => None
   5.121        }
   5.122 @@ -310,7 +245,7 @@
   5.123  
   5.124    /* messages */
   5.125  
   5.126 -  val Serial = new Long_Property("serial")
   5.127 +  val Serial = new Properties.Long("serial")
   5.128  
   5.129    val MESSAGE = "message"
   5.130  
   5.131 @@ -336,12 +271,12 @@
   5.132    /* raw message functions */
   5.133  
   5.134    val FUNCTION = "function"
   5.135 -  val Function = new Property(FUNCTION)
   5.136 +  val Function = new Properties.String(FUNCTION)
   5.137  
   5.138    val INVOKE_SCALA = "invoke_scala"
   5.139    object Invoke_Scala
   5.140    {
   5.141 -    def unapply(props: List[(String, String)]): Option[(String, String)] =
   5.142 +    def unapply(props: Properties.T): Option[(String, String)] =
   5.143        props match {
   5.144          case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
   5.145          case _ => None
   5.146 @@ -354,4 +289,4 @@
   5.147    val Data = Markup("data", Nil)
   5.148  }
   5.149  
   5.150 -sealed case class Markup(name: String, properties: List[(String, String)])
   5.151 +sealed case class Markup(name: String, properties: Properties.T)
     6.1 --- a/src/Pure/General/position.scala	Wed Jul 13 00:43:07 2011 +0900
     6.2 +++ b/src/Pure/General/position.scala	Tue Jul 12 20:53:14 2011 +0200
     6.3 @@ -9,13 +9,13 @@
     6.4  
     6.5  object Position
     6.6  {
     6.7 -  type T = List[(String, String)]
     6.8 +  type T = Properties.T
     6.9  
    6.10 -  val Line = new Markup.Int_Property(Markup.LINE)
    6.11 -  val Offset = new Markup.Int_Property(Markup.OFFSET)
    6.12 -  val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
    6.13 -  val File = new Markup.Property(Markup.FILE)
    6.14 -  val Id = new Markup.Long_Property(Markup.ID)
    6.15 +  val Line = new Properties.Int(Markup.LINE)
    6.16 +  val Offset = new Properties.Int(Markup.OFFSET)
    6.17 +  val End_Offset = new Properties.Int(Markup.END_OFFSET)
    6.18 +  val File = new Properties.String(Markup.FILE)
    6.19 +  val Id = new Properties.Long(Markup.ID)
    6.20  
    6.21    object Range
    6.22    {
     7.1 --- a/src/Pure/General/properties.ML	Wed Jul 13 00:43:07 2011 +0900
     7.2 +++ b/src/Pure/General/properties.ML	Tue Jul 12 20:53:14 2011 +0200
     7.3 @@ -6,27 +6,30 @@
     7.4  
     7.5  signature PROPERTIES =
     7.6  sig
     7.7 -  type property = string * string
     7.8 -  type T = property list
     7.9 +  type entry = string * string
    7.10 +  type T = entry list
    7.11    val defined: T -> string -> bool
    7.12    val get: T -> string -> string option
    7.13    val get_int: T -> string -> int option
    7.14 -  val put: string * string -> T -> T
    7.15 +  val put: entry -> T -> T
    7.16 +  val put_int: string * int -> T -> T
    7.17    val remove: string -> T -> T
    7.18  end;
    7.19  
    7.20  structure Properties: PROPERTIES =
    7.21  struct
    7.22  
    7.23 -type property = string * string;
    7.24 -type T = property list;
    7.25 +type entry = string * string;
    7.26 +type T = entry list;
    7.27  
    7.28  fun defined (props: T) name = AList.defined (op =) props name;
    7.29  
    7.30  fun get (props: T) name = AList.lookup (op =) props name;
    7.31  fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
    7.32  
    7.33 -fun put prop (props: T) = AList.update (op =) prop props;
    7.34 +fun put entry (props: T) = AList.update (op =) entry props;
    7.35 +fun put_int (name, i) = put (name, signed_string_of_int i);
    7.36 +
    7.37  fun remove name (props: T) = AList.delete (op =) name props;
    7.38  
    7.39  end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/General/properties.scala	Tue Jul 12 20:53:14 2011 +0200
     8.3 @@ -0,0 +1,84 @@
     8.4 +/*  Title:      Pure/General/properties.scala
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Property lists.
     8.8 +*/
     8.9 +
    8.10 +package isabelle
    8.11 +
    8.12 +
    8.13 +object Properties
    8.14 +{
    8.15 +  /* plain values */
    8.16 +
    8.17 +  object Value
    8.18 +  {
    8.19 +    object Int
    8.20 +    {
    8.21 +      def apply(x: scala.Int): java.lang.String = x.toString
    8.22 +      def unapply(s: java.lang.String): Option[scala.Int] =
    8.23 +        try { Some(Integer.parseInt(s)) }
    8.24 +        catch { case _: NumberFormatException => None }
    8.25 +    }
    8.26 +
    8.27 +    object Long
    8.28 +    {
    8.29 +      def apply(x: scala.Long): java.lang.String = x.toString
    8.30 +      def unapply(s: java.lang.String): Option[scala.Long] =
    8.31 +        try { Some(java.lang.Long.parseLong(s)) }
    8.32 +        catch { case _: NumberFormatException => None }
    8.33 +    }
    8.34 +
    8.35 +    object Double
    8.36 +    {
    8.37 +      def apply(x: scala.Double): java.lang.String = x.toString
    8.38 +      def unapply(s: java.lang.String): Option[scala.Double] =
    8.39 +        try { Some(java.lang.Double.parseDouble(s)) }
    8.40 +        catch { case _: NumberFormatException => None }
    8.41 +    }
    8.42 +  }
    8.43 +
    8.44 +
    8.45 +  /* named entries */
    8.46 +
    8.47 +  type Entry = (java.lang.String, java.lang.String)
    8.48 +  type T = List[Entry]
    8.49 +
    8.50 +  class String(val name: java.lang.String)
    8.51 +  {
    8.52 +    def apply(value: java.lang.String): T = List((name, value))
    8.53 +    def unapply(props: T): Option[java.lang.String] =
    8.54 +      props.find(_._1 == name).map(_._2)
    8.55 +  }
    8.56 +
    8.57 +  class Int(name: java.lang.String)
    8.58 +  {
    8.59 +    def apply(value: scala.Int): T = List((name, Value.Int(value)))
    8.60 +    def unapply(props: T): Option[scala.Int] =
    8.61 +      props.find(_._1 == name) match {
    8.62 +        case None => None
    8.63 +        case Some((_, value)) => Value.Int.unapply(value)
    8.64 +      }
    8.65 +  }
    8.66 +
    8.67 +  class Long(name: java.lang.String)
    8.68 +  {
    8.69 +    def apply(value: scala.Long): T = List((name, Value.Long(value)))
    8.70 +    def unapply(props: T): Option[scala.Long] =
    8.71 +      props.find(_._1 == name) match {
    8.72 +        case None => None
    8.73 +        case Some((_, value)) => Value.Long.unapply(value)
    8.74 +      }
    8.75 +  }
    8.76 +
    8.77 +  class Double(name: java.lang.String)
    8.78 +  {
    8.79 +    def apply(value: scala.Double): T = List((name, Value.Double(value)))
    8.80 +    def unapply(props: T): Option[scala.Double] =
    8.81 +      props.find(_._1 == name) match {
    8.82 +        case None => None
    8.83 +        case Some((_, value)) => Value.Double.unapply(value)
    8.84 +      }
    8.85 +  }
    8.86 +}
    8.87 +
     9.1 --- a/src/Pure/General/symbol.ML	Wed Jul 13 00:43:07 2011 +0900
     9.2 +++ b/src/Pure/General/symbol.ML	Tue Jul 12 20:53:14 2011 +0200
     9.3 @@ -7,10 +7,7 @@
     9.4  signature SYMBOL =
     9.5  sig
     9.6    type symbol = string
     9.7 -  val SOH: symbol
     9.8    val STX: symbol
     9.9 -  val ENQ: symbol
    9.10 -  val ACK: symbol
    9.11    val DEL: symbol
    9.12    val space: symbol
    9.13    val spaces: int -> string
    9.14 @@ -89,10 +86,7 @@
    9.15  
    9.16  type symbol = string;
    9.17  
    9.18 -val SOH = chr 1;
    9.19  val STX = chr 2;
    9.20 -val ENQ = chr 5;
    9.21 -val ACK = chr 6;
    9.22  val DEL = chr 127;
    9.23  
    9.24  val space = chr 32;
    10.1 --- a/src/Pure/General/symbol_pos.ML	Wed Jul 13 00:43:07 2011 +0900
    10.2 +++ b/src/Pure/General/symbol_pos.ML	Tue Jul 12 20:53:14 2011 +0200
    10.3 @@ -19,6 +19,9 @@
    10.4    val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
    10.5    val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
    10.6    val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
    10.7 +  val quote_string_q: string -> string
    10.8 +  val quote_string_qq: string -> string
    10.9 +  val quote_string_bq: string -> string
   10.10    val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   10.11      T list -> T list * T list
   10.12    val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
   10.13 @@ -75,7 +78,7 @@
   10.14  val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
   10.15  
   10.16  
   10.17 -(* Isabelle strings *)
   10.18 +(* scan string literals *)
   10.19  
   10.20  local
   10.21  
   10.22 @@ -104,6 +107,29 @@
   10.23  end;
   10.24  
   10.25  
   10.26 +(* quote string literals *)
   10.27 +
   10.28 +local
   10.29 +
   10.30 +fun char_code i =
   10.31 +  (if i < 10 then "00" else if i < 100 then "0" else "") ^ string_of_int i;
   10.32 +
   10.33 +fun quote_str q s =
   10.34 +  if Symbol.is_ascii_control s then "\\" ^ char_code (ord s)
   10.35 +  else if s = q orelse s = "\\" then "\\" ^ s
   10.36 +  else s;
   10.37 +
   10.38 +fun quote_string q = enclose q q o implode o map (quote_str q) o Symbol.explode;
   10.39 +
   10.40 +in
   10.41 +
   10.42 +val quote_string_q = quote_string "'";
   10.43 +val quote_string_qq = quote_string "\"";
   10.44 +val quote_string_bq = quote_string "`";
   10.45 +
   10.46 +end;
   10.47 +
   10.48 +
   10.49  (* ML-style comments *)
   10.50  
   10.51  local
    11.1 --- a/src/Pure/General/xml.ML	Wed Jul 13 00:43:07 2011 +0900
    11.2 +++ b/src/Pure/General/xml.ML	Tue Jul 12 20:53:14 2011 +0200
    11.3 @@ -1,9 +1,29 @@
    11.4  (*  Title:      Pure/General/xml.ML
    11.5      Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
    11.6  
    11.7 -Simple XML tree values.
    11.8 +Untyped XML trees.
    11.9  *)
   11.10  
   11.11 +signature XML_DATA_OPS =
   11.12 +sig
   11.13 +  type 'a A
   11.14 +  type 'a T
   11.15 +  type 'a V
   11.16 +  val int_atom: int A
   11.17 +  val bool_atom: bool A
   11.18 +  val unit_atom: unit A
   11.19 +  val properties: Properties.T T
   11.20 +  val string: string T
   11.21 +  val int: int T
   11.22 +  val bool: bool T
   11.23 +  val unit: unit T
   11.24 +  val pair: 'a T -> 'b T -> ('a * 'b) T
   11.25 +  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   11.26 +  val list: 'a T -> 'a list T
   11.27 +  val option: 'a T -> 'a option T
   11.28 +  val variant: 'a V list -> 'a T
   11.29 +end;
   11.30 +
   11.31  signature XML =
   11.32  sig
   11.33    type attributes = Properties.T
   11.34 @@ -24,6 +44,10 @@
   11.35    val parse_element: string list -> tree * string list
   11.36    val parse_document: string list -> tree * string list
   11.37    val parse: string -> tree
   11.38 +  exception XML_ATOM of string
   11.39 +  exception XML_BODY of body
   11.40 +  structure Encode: XML_DATA_OPS
   11.41 +  structure Decode: XML_DATA_OPS
   11.42  end;
   11.43  
   11.44  structure XML: XML =
   11.45 @@ -190,4 +214,137 @@
   11.46  
   11.47  end;
   11.48  
   11.49 +
   11.50 +
   11.51 +(** XML as data representation language **)
   11.52 +
   11.53 +exception XML_ATOM of string;
   11.54 +exception XML_BODY of tree list;
   11.55 +
   11.56 +
   11.57 +structure Encode =
   11.58 +struct
   11.59 +
   11.60 +type 'a A = 'a -> string;
   11.61 +type 'a T = 'a -> body;
   11.62 +type 'a V = 'a -> string list * body;
   11.63 +
   11.64 +
   11.65 +(* atomic values *)
   11.66 +
   11.67 +fun int_atom i = signed_string_of_int i;
   11.68 +
   11.69 +fun bool_atom false = "0"
   11.70 +  | bool_atom true = "1";
   11.71 +
   11.72 +fun unit_atom () = "";
   11.73 +
   11.74 +
   11.75 +(* structural nodes *)
   11.76 +
   11.77 +fun node ts = Elem ((":", []), ts);
   11.78 +
   11.79 +fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
   11.80 +
   11.81 +fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
   11.82 +
   11.83 +
   11.84 +(* representation of standard types *)
   11.85 +
   11.86 +fun properties props = [Elem ((":", props), [])];
   11.87 +
   11.88 +fun string "" = []
   11.89 +  | string s = [Text s];
   11.90 +
   11.91 +val int = string o int_atom;
   11.92 +
   11.93 +val bool = string o bool_atom;
   11.94 +
   11.95 +val unit = string o unit_atom;
   11.96 +
   11.97 +fun pair f g (x, y) = [node (f x), node (g y)];
   11.98 +
   11.99 +fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
  11.100 +
  11.101 +fun list f xs = map (node o f) xs;
  11.102 +
  11.103 +fun option _ NONE = []
  11.104 +  | option f (SOME x) = [node (f x)];
  11.105 +
  11.106 +fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
  11.107 +
  11.108  end;
  11.109 +
  11.110 +
  11.111 +structure Decode =
  11.112 +struct
  11.113 +
  11.114 +type 'a A = string -> 'a;
  11.115 +type 'a T = body -> 'a;
  11.116 +type 'a V = string list * body -> 'a;
  11.117 +
  11.118 +
  11.119 +(* atomic values *)
  11.120 +
  11.121 +fun int_atom s =
  11.122 +  (case Int.fromString s of
  11.123 +    SOME i => i
  11.124 +  | NONE => raise XML_ATOM s);
  11.125 +
  11.126 +fun bool_atom "0" = false
  11.127 +  | bool_atom "1" = true
  11.128 +  | bool_atom s = raise XML_ATOM s;
  11.129 +
  11.130 +fun unit_atom "" = ()
  11.131 +  | unit_atom s = raise XML_ATOM s;
  11.132 +
  11.133 +
  11.134 +(* structural nodes *)
  11.135 +
  11.136 +fun node (Elem ((":", []), ts)) = ts
  11.137 +  | node t = raise XML_BODY [t];
  11.138 +
  11.139 +fun vector atts =
  11.140 +  fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts;
  11.141 +
  11.142 +fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
  11.143 +  | tagged t = raise XML_BODY [t];
  11.144 +
  11.145 +
  11.146 +(* representation of standard types *)
  11.147 +
  11.148 +fun properties [Elem ((":", props), [])] = props
  11.149 +  | properties ts = raise XML_BODY ts;
  11.150 +
  11.151 +fun string [] = ""
  11.152 +  | string [Text s] = s
  11.153 +  | string ts = raise XML_BODY ts;
  11.154 +
  11.155 +val int = int_atom o string;
  11.156 +
  11.157 +val bool = bool_atom o string;
  11.158 +
  11.159 +val unit = unit_atom o string;
  11.160 +
  11.161 +fun pair f g [t1, t2] = (f (node t1), g (node t2))
  11.162 +  | pair _ _ ts = raise XML_BODY ts;
  11.163 +
  11.164 +fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
  11.165 +  | triple _ _ _ ts = raise XML_BODY ts;
  11.166 +
  11.167 +fun list f ts = map (f o node) ts;
  11.168 +
  11.169 +fun option _ [] = NONE
  11.170 +  | option f [t] = SOME (f (node t))
  11.171 +  | option _ ts = raise XML_BODY ts;
  11.172 +
  11.173 +fun variant fs [t] =
  11.174 +      let
  11.175 +        val (tag, (xs, ts)) = tagged t;
  11.176 +        val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
  11.177 +      in f (xs, ts) end
  11.178 +  | variant _ ts = raise XML_BODY ts;
  11.179 +
  11.180 +end;
  11.181 +
  11.182 +end;
    12.1 --- a/src/Pure/General/xml.scala	Wed Jul 13 00:43:07 2011 +0900
    12.2 +++ b/src/Pure/General/xml.scala	Tue Jul 12 20:53:14 2011 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  /*  Title:      Pure/General/xml.scala
    12.5      Author:     Makarius
    12.6  
    12.7 -Simple XML tree values.
    12.8 +Untyped XML trees.
    12.9  */
   12.10  
   12.11  package isabelle
   12.12 @@ -12,13 +12,16 @@
   12.13  import javax.xml.parsers.DocumentBuilderFactory
   12.14  
   12.15  import scala.actors.Actor._
   12.16 +import scala.collection.mutable
   12.17  
   12.18  
   12.19  object XML
   12.20  {
   12.21 +  /** XML trees **/
   12.22 +
   12.23    /* datatype representation */
   12.24  
   12.25 -  type Attributes = List[(String, String)]
   12.26 +  type Attributes = Properties.T
   12.27  
   12.28    sealed abstract class Tree { override def toString = string_of_tree(this) }
   12.29    case class Elem(markup: Markup, body: List[Tree]) extends Tree
   12.30 @@ -115,7 +118,7 @@
   12.31              val z = trim_bytes(x)
   12.32              if (z.length > max_string) z else store(z)
   12.33          }
   12.34 -      def cache_props(x: List[(String, String)]): List[(String, String)] =
   12.35 +      def cache_props(x: Properties.T): Properties.T =
   12.36          if (x.isEmpty) x
   12.37          else
   12.38            lookup(x) match {
   12.39 @@ -174,7 +177,8 @@
   12.40    }
   12.41  
   12.42  
   12.43 -  /* document object model (W3C DOM) */
   12.44 +
   12.45 +  /** document object model (W3C DOM) **/
   12.46  
   12.47    def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
   12.48      node.getUserData(Markup.Data.name) match {
   12.49 @@ -200,4 +204,184 @@
   12.50      }
   12.51      DOM(tree)
   12.52    }
   12.53 +
   12.54 +
   12.55 +
   12.56 +  /** XML as data representation language **/
   12.57 +
   12.58 +  class XML_Atom(s: String) extends Exception(s)
   12.59 +  class XML_Body(body: XML.Body) extends Exception
   12.60 +
   12.61 +  object Encode
   12.62 +  {
   12.63 +    type T[A] = A => XML.Body
   12.64 +
   12.65 +
   12.66 +    /* atomic values */
   12.67 +
   12.68 +    def long_atom(i: Long): String = i.toString
   12.69 +
   12.70 +    def int_atom(i: Int): String = i.toString
   12.71 +
   12.72 +    def bool_atom(b: Boolean): String = if (b) "1" else "0"
   12.73 +
   12.74 +    def unit_atom(u: Unit) = ""
   12.75 +
   12.76 +
   12.77 +    /* structural nodes */
   12.78 +
   12.79 +    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   12.80 +
   12.81 +    private def vector(xs: List[String]): XML.Attributes =
   12.82 +      xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
   12.83 +
   12.84 +    private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
   12.85 +      XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
   12.86 +
   12.87 +
   12.88 +    /* representation of standard types */
   12.89 +
   12.90 +    val properties: T[Properties.T] =
   12.91 +      (props => List(XML.Elem(Markup(":", props), Nil)))
   12.92 +
   12.93 +    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
   12.94 +
   12.95 +    val long: T[Long] = (x => string(long_atom(x)))
   12.96 +
   12.97 +    val int: T[Int] = (x => string(int_atom(x)))
   12.98 +
   12.99 +    val bool: T[Boolean] = (x => string(bool_atom(x)))
  12.100 +
  12.101 +    val unit: T[Unit] = (x => string(unit_atom(x)))
  12.102 +
  12.103 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  12.104 +      (x => List(node(f(x._1)), node(g(x._2))))
  12.105 +
  12.106 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  12.107 +      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
  12.108 +
  12.109 +    def list[A](f: T[A]): T[List[A]] =
  12.110 +      (xs => xs.map((x: A) => node(f(x))))
  12.111 +
  12.112 +    def option[A](f: T[A]): T[Option[A]] =
  12.113 +    {
  12.114 +      case None => Nil
  12.115 +      case Some(x) => List(node(f(x)))
  12.116 +    }
  12.117 +
  12.118 +    def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
  12.119 +    {
  12.120 +      case x =>
  12.121 +        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
  12.122 +        List(tagged(tag, f(x)))
  12.123 +    }
  12.124 +  }
  12.125 +
  12.126 +  object Decode
  12.127 +  {
  12.128 +    type T[A] = XML.Body => A
  12.129 +    type V[A] = (List[String], XML.Body) => A
  12.130 +
  12.131 +
  12.132 +    /* atomic values */
  12.133 +
  12.134 +    def long_atom(s: String): Long =
  12.135 +      try { java.lang.Long.parseLong(s) }
  12.136 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  12.137 +
  12.138 +    def int_atom(s: String): Int =
  12.139 +      try { Integer.parseInt(s) }
  12.140 +      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  12.141 +
  12.142 +    def bool_atom(s: String): Boolean =
  12.143 +      if (s == "1") true
  12.144 +      else if (s == "0") false
  12.145 +      else throw new XML_Atom(s)
  12.146 +
  12.147 +    def unit_atom(s: String): Unit =
  12.148 +      if (s == "") () else throw new XML_Atom(s)
  12.149 +
  12.150 +
  12.151 +    /* structural nodes */
  12.152 +
  12.153 +    private def node(t: XML.Tree): XML.Body =
  12.154 +      t match {
  12.155 +        case XML.Elem(Markup(":", Nil), ts) => ts
  12.156 +        case _ => throw new XML_Body(List(t))
  12.157 +      }
  12.158 +
  12.159 +    private def vector(atts: XML.Attributes): List[String] =
  12.160 +    {
  12.161 +      val xs = new mutable.ListBuffer[String]
  12.162 +      var i = 0
  12.163 +      for ((a, x) <- atts) {
  12.164 +        if (int_atom(a) == i) { xs += x; i = i + 1 }
  12.165 +        else throw new XML_Atom(a)
  12.166 +      }
  12.167 +      xs.toList
  12.168 +    }
  12.169 +
  12.170 +    private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
  12.171 +      t match {
  12.172 +        case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
  12.173 +        case _ => throw new XML_Body(List(t))
  12.174 +      }
  12.175 +
  12.176 +
  12.177 +    /* representation of standard types */
  12.178 +
  12.179 +    val properties: T[Properties.T] =
  12.180 +    {
  12.181 +      case List(XML.Elem(Markup(":", props), Nil)) => props
  12.182 +      case ts => throw new XML_Body(ts)
  12.183 +    }
  12.184 +
  12.185 +    val string: T[String] =
  12.186 +    {
  12.187 +      case Nil => ""
  12.188 +      case List(XML.Text(s)) => s
  12.189 +      case ts => throw new XML_Body(ts)
  12.190 +    }
  12.191 +
  12.192 +    val long: T[Long] = (x => long_atom(string(x)))
  12.193 +
  12.194 +    val int: T[Int] = (x => int_atom(string(x)))
  12.195 +
  12.196 +    val bool: T[Boolean] = (x => bool_atom(string(x)))
  12.197 +
  12.198 +    val unit: T[Unit] = (x => unit_atom(string(x)))
  12.199 +
  12.200 +    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  12.201 +    {
  12.202 +      case List(t1, t2) => (f(node(t1)), g(node(t2)))
  12.203 +      case ts => throw new XML_Body(ts)
  12.204 +    }
  12.205 +
  12.206 +    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  12.207 +    {
  12.208 +      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
  12.209 +      case ts => throw new XML_Body(ts)
  12.210 +    }
  12.211 +
  12.212 +    def list[A](f: T[A]): T[List[A]] =
  12.213 +      (ts => ts.map(t => f(node(t))))
  12.214 +
  12.215 +    def option[A](f: T[A]): T[Option[A]] =
  12.216 +    {
  12.217 +      case Nil => None
  12.218 +      case List(t) => Some(f(node(t)))
  12.219 +      case ts => throw new XML_Body(ts)
  12.220 +    }
  12.221 +
  12.222 +    def variant[A](fs: List[V[A]]): T[A] =
  12.223 +    {
  12.224 +      case List(t) =>
  12.225 +        val (tag, (xs, ts)) = tagged(t)
  12.226 +        val f =
  12.227 +          try { fs(tag) }
  12.228 +          catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
  12.229 +        f(xs, ts)
  12.230 +      case ts => throw new XML_Body(ts)
  12.231 +    }
  12.232 +  }
  12.233  }
    13.1 --- a/src/Pure/General/xml_data.ML	Wed Jul 13 00:43:07 2011 +0900
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,154 +0,0 @@
    13.4 -(*  Title:      Pure/General/xml_data.ML
    13.5 -    Author:     Makarius
    13.6 -
    13.7 -XML as basic data representation language.
    13.8 -*)
    13.9 -
   13.10 -signature XML_DATA_OPS =
   13.11 -sig
   13.12 -  type 'a T
   13.13 -  val properties: Properties.T T
   13.14 -  val string: string T
   13.15 -  val int: int T
   13.16 -  val bool: bool T
   13.17 -  val unit: unit T
   13.18 -  val pair: 'a T -> 'b T -> ('a * 'b) T
   13.19 -  val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
   13.20 -  val list: 'a T -> 'a list T
   13.21 -  val option: 'a T -> 'a option T
   13.22 -  val variant: 'a T list -> 'a T
   13.23 -end;
   13.24 -
   13.25 -signature XML_DATA =
   13.26 -sig
   13.27 -  structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
   13.28 -  exception XML_ATOM of string
   13.29 -  exception XML_BODY of XML.body
   13.30 -  structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
   13.31 -end;
   13.32 -
   13.33 -structure XML_Data: XML_DATA =
   13.34 -struct
   13.35 -
   13.36 -(** encode **)
   13.37 -
   13.38 -structure Encode =
   13.39 -struct
   13.40 -
   13.41 -type 'a T = 'a -> XML.body;
   13.42 -
   13.43 -
   13.44 -(* basic values *)
   13.45 -
   13.46 -fun int_atom i = signed_string_of_int i;
   13.47 -
   13.48 -fun bool_atom false = "0"
   13.49 -  | bool_atom true = "1";
   13.50 -
   13.51 -fun unit_atom () = "";
   13.52 -
   13.53 -
   13.54 -(* structural nodes *)
   13.55 -
   13.56 -fun node ts = XML.Elem ((":", []), ts);
   13.57 -
   13.58 -fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
   13.59 -
   13.60 -
   13.61 -(* representation of standard types *)
   13.62 -
   13.63 -fun properties props = [XML.Elem ((":", props), [])];
   13.64 -
   13.65 -fun string "" = []
   13.66 -  | string s = [XML.Text s];
   13.67 -
   13.68 -val int = string o int_atom;
   13.69 -
   13.70 -val bool = string o bool_atom;
   13.71 -
   13.72 -val unit = string o unit_atom;
   13.73 -
   13.74 -fun pair f g (x, y) = [node (f x), node (g y)];
   13.75 -
   13.76 -fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
   13.77 -
   13.78 -fun list f xs = map (node o f) xs;
   13.79 -
   13.80 -fun option _ NONE = []
   13.81 -  | option f (SOME x) = [node (f x)];
   13.82 -
   13.83 -fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
   13.84 -
   13.85 -end;
   13.86 -
   13.87 -
   13.88 -
   13.89 -(** decode **)
   13.90 -
   13.91 -exception XML_ATOM of string;
   13.92 -exception XML_BODY of XML.tree list;
   13.93 -
   13.94 -structure Decode =
   13.95 -struct
   13.96 -
   13.97 -type 'a T = XML.body -> 'a;
   13.98 -
   13.99 -
  13.100 -(* basic values *)
  13.101 -
  13.102 -fun int_atom s =
  13.103 -  (case Int.fromString s of
  13.104 -    SOME i => i
  13.105 -  | NONE => raise XML_ATOM s);
  13.106 -
  13.107 -fun bool_atom "0" = false
  13.108 -  | bool_atom "1" = true
  13.109 -  | bool_atom s = raise XML_ATOM s;
  13.110 -
  13.111 -fun unit_atom "" = ()
  13.112 -  | unit_atom s = raise XML_ATOM s;
  13.113 -
  13.114 -
  13.115 -(* structural nodes *)
  13.116 -
  13.117 -fun node (XML.Elem ((":", []), ts)) = ts
  13.118 -  | node t = raise XML_BODY [t];
  13.119 -
  13.120 -fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
  13.121 -  | tagged t = raise XML_BODY [t];
  13.122 -
  13.123 -
  13.124 -(* representation of standard types *)
  13.125 -
  13.126 -fun properties [XML.Elem ((":", props), [])] = props
  13.127 -  | properties ts = raise XML_BODY ts;
  13.128 -
  13.129 -fun string [] = ""
  13.130 -  | string [XML.Text s] = s
  13.131 -  | string ts = raise XML_BODY ts;
  13.132 -
  13.133 -val int = int_atom o string;
  13.134 -
  13.135 -val bool = bool_atom o string;
  13.136 -
  13.137 -val unit = unit_atom o string;
  13.138 -
  13.139 -fun pair f g [t1, t2] = (f (node t1), g (node t2))
  13.140 -  | pair _ _ ts = raise XML_BODY ts;
  13.141 -
  13.142 -fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
  13.143 -  | triple _ _ _ ts = raise XML_BODY ts;
  13.144 -
  13.145 -fun list f ts = map (f o node) ts;
  13.146 -
  13.147 -fun option _ [] = NONE
  13.148 -  | option f [t] = SOME (f (node t))
  13.149 -  | option _ ts = raise XML_BODY ts;
  13.150 -
  13.151 -fun variant fs [t] = uncurry (nth fs) (tagged t)
  13.152 -  | variant _ ts = raise XML_BODY ts;
  13.153 -
  13.154 -end;
  13.155 -
  13.156 -end;
  13.157 -
    14.1 --- a/src/Pure/General/xml_data.scala	Wed Jul 13 00:43:07 2011 +0900
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,176 +0,0 @@
    14.4 -/*  Title:      Pure/General/xml_data.scala
    14.5 -    Author:     Makarius
    14.6 -
    14.7 -XML as basic data representation language.
    14.8 -*/
    14.9 -
   14.10 -package isabelle
   14.11 -
   14.12 -
   14.13 -
   14.14 -object XML_Data
   14.15 -{
   14.16 -  /** encode **/
   14.17 -
   14.18 -  object Encode
   14.19 -  {
   14.20 -    type T[A] = A => XML.Body
   14.21 -
   14.22 -
   14.23 -    /* basic values */
   14.24 -
   14.25 -    private def long_atom(i: Long): String = i.toString
   14.26 -
   14.27 -    private def int_atom(i: Int): String = i.toString
   14.28 -
   14.29 -    private def bool_atom(b: Boolean): String = if (b) "1" else "0"
   14.30 -
   14.31 -    private def unit_atom(u: Unit) = ""
   14.32 -
   14.33 -
   14.34 -    /* structural nodes */
   14.35 -
   14.36 -    private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
   14.37 -
   14.38 -    private def tagged(tag: Int, ts: XML.Body): XML.Tree =
   14.39 -      XML.Elem(Markup(int_atom(tag), Nil), ts)
   14.40 -
   14.41 -
   14.42 -    /* representation of standard types */
   14.43 -
   14.44 -    val properties: T[List[(String, String)]] =
   14.45 -      (props => List(XML.Elem(Markup(":", props), Nil)))
   14.46 -
   14.47 -    val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
   14.48 -
   14.49 -    val long: T[Long] = (x => string(long_atom(x)))
   14.50 -
   14.51 -    val int: T[Int] = (x => string(int_atom(x)))
   14.52 -
   14.53 -    val bool: T[Boolean] = (x => string(bool_atom(x)))
   14.54 -
   14.55 -    val unit: T[Unit] = (x => string(unit_atom(x)))
   14.56 -
   14.57 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
   14.58 -      (x => List(node(f(x._1)), node(g(x._2))))
   14.59 -
   14.60 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
   14.61 -      (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
   14.62 -
   14.63 -    def list[A](f: T[A]): T[List[A]] =
   14.64 -      (xs => xs.map((x: A) => node(f(x))))
   14.65 -
   14.66 -    def option[A](f: T[A]): T[Option[A]] =
   14.67 -    {
   14.68 -      case None => Nil
   14.69 -      case Some(x) => List(node(f(x)))
   14.70 -    }
   14.71 -
   14.72 -    def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
   14.73 -    {
   14.74 -      case x =>
   14.75 -        val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
   14.76 -        List(tagged(tag, f(x)))
   14.77 -    }
   14.78 -  }
   14.79 -
   14.80 -
   14.81 -
   14.82 -  /** decode **/
   14.83 -
   14.84 -  class XML_Atom(s: String) extends Exception(s)
   14.85 -  class XML_Body(body: XML.Body) extends Exception
   14.86 -
   14.87 -  object Decode
   14.88 -  {
   14.89 -    type T[A] = XML.Body => A
   14.90 -
   14.91 -
   14.92 -     /* basic values */
   14.93 -
   14.94 -    private def long_atom(s: String): Long =
   14.95 -      try { java.lang.Long.parseLong(s) }
   14.96 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
   14.97 -
   14.98 -    private def int_atom(s: String): Int =
   14.99 -      try { Integer.parseInt(s) }
  14.100 -      catch { case e: NumberFormatException => throw new XML_Atom(s) }
  14.101 -
  14.102 -    private def bool_atom(s: String): Boolean =
  14.103 -      if (s == "1") true
  14.104 -      else if (s == "0") false
  14.105 -      else throw new XML_Atom(s)
  14.106 -
  14.107 -    private def unit_atom(s: String): Unit =
  14.108 -      if (s == "") () else throw new XML_Atom(s)
  14.109 -
  14.110 -
  14.111 -    /* structural nodes */
  14.112 -
  14.113 -    private def node(t: XML.Tree): XML.Body =
  14.114 -      t match {
  14.115 -        case XML.Elem(Markup(":", Nil), ts) => ts
  14.116 -        case _ => throw new XML_Body(List(t))
  14.117 -      }
  14.118 -
  14.119 -    private def tagged(t: XML.Tree): (Int, XML.Body) =
  14.120 -      t match {
  14.121 -        case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
  14.122 -        case _ => throw new XML_Body(List(t))
  14.123 -      }
  14.124 -
  14.125 -
  14.126 -    /* representation of standard types */
  14.127 -
  14.128 -    val properties: T[List[(String, String)]] =
  14.129 -    {
  14.130 -      case List(XML.Elem(Markup(":", props), Nil)) => props
  14.131 -      case ts => throw new XML_Body(ts)
  14.132 -    }
  14.133 -
  14.134 -    val string: T[String] =
  14.135 -    {
  14.136 -      case Nil => ""
  14.137 -      case List(XML.Text(s)) => s
  14.138 -      case ts => throw new XML_Body(ts)
  14.139 -    }
  14.140 -
  14.141 -    val long: T[Long] = (x => long_atom(string(x)))
  14.142 -
  14.143 -    val int: T[Int] = (x => int_atom(string(x)))
  14.144 -
  14.145 -    val bool: T[Boolean] = (x => bool_atom(string(x)))
  14.146 -
  14.147 -    val unit: T[Unit] = (x => unit_atom(string(x)))
  14.148 -
  14.149 -    def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
  14.150 -    {
  14.151 -      case List(t1, t2) => (f(node(t1)), g(node(t2)))
  14.152 -      case ts => throw new XML_Body(ts)
  14.153 -    }
  14.154 -
  14.155 -    def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
  14.156 -    {
  14.157 -      case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
  14.158 -      case ts => throw new XML_Body(ts)
  14.159 -    }
  14.160 -
  14.161 -    def list[A](f: T[A]): T[List[A]] =
  14.162 -      (ts => ts.map(t => f(node(t))))
  14.163 -
  14.164 -    def option[A](f: T[A]): T[Option[A]] =
  14.165 -    {
  14.166 -      case Nil => None
  14.167 -      case List(t) => Some(f(node(t)))
  14.168 -      case ts => throw new XML_Body(ts)
  14.169 -    }
  14.170 -
  14.171 -    def variant[A](fs: List[T[A]]): T[A] =
  14.172 -    {
  14.173 -      case List(t) =>
  14.174 -        val (tag, ts) = tagged(t)
  14.175 -        fs(tag)(ts)
  14.176 -      case ts => throw new XML_Body(ts)
  14.177 -    }
  14.178 -  }
  14.179 -}
    15.1 --- a/src/Pure/General/yxml.ML	Wed Jul 13 00:43:07 2011 +0900
    15.2 +++ b/src/Pure/General/yxml.ML	Tue Jul 12 20:53:14 2011 +0200
    15.3 @@ -15,7 +15,9 @@
    15.4  
    15.5  signature YXML =
    15.6  sig
    15.7 -  val escape_controls: string -> string
    15.8 +  val X: Symbol.symbol
    15.9 +  val Y: Symbol.symbol
   15.10 +  val embed_controls: string -> string
   15.11    val detect: string -> bool
   15.12    val output_markup: Markup.T -> string * string
   15.13    val element: string -> XML.attributes -> string list -> string
   15.14 @@ -37,7 +39,7 @@
   15.15    then chr 192 ^ chr (128 + ord c)
   15.16    else c;
   15.17  
   15.18 -fun escape_controls str =
   15.19 +fun embed_controls str =
   15.20    if exists_string Symbol.is_ascii_control str
   15.21    then translate_string pseudo_utf8 str
   15.22    else str;
   15.23 @@ -45,12 +47,12 @@
   15.24  
   15.25  (* markers *)
   15.26  
   15.27 -val X = Symbol.ENQ;
   15.28 -val Y = Symbol.ACK;
   15.29 +val X = chr 5;
   15.30 +val Y = chr 6;
   15.31  val XY = X ^ Y;
   15.32  val XYX = XY ^ X;
   15.33  
   15.34 -val detect = exists_string (fn s => s = X);
   15.35 +val detect = exists_string (fn s => s = X orelse s = Y);
   15.36  
   15.37  
   15.38  (* output *)
    16.1 --- a/src/Pure/General/yxml.scala	Wed Jul 13 00:43:07 2011 +0900
    16.2 +++ b/src/Pure/General/yxml.scala	Tue Jul 12 20:53:14 2011 +0200
    16.3 @@ -14,10 +14,12 @@
    16.4  {
    16.5    /* chunk markers */
    16.6  
    16.7 -  private val X = '\5'
    16.8 -  private val Y = '\6'
    16.9 -  private val X_string = X.toString
   16.10 -  private val Y_string = Y.toString
   16.11 +  val X = '\5'
   16.12 +  val Y = '\6'
   16.13 +  val X_string = X.toString
   16.14 +  val Y_string = Y.toString
   16.15 +
   16.16 +  def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
   16.17  
   16.18  
   16.19    /* string representation */  // FIXME byte array version with pseudo-utf-8 (!?)
    17.1 --- a/src/Pure/IsaMakefile	Wed Jul 13 00:43:07 2011 +0900
    17.2 +++ b/src/Pure/IsaMakefile	Tue Jul 12 20:53:14 2011 +0200
    17.3 @@ -104,7 +104,6 @@
    17.4    General/timing.ML					\
    17.5    General/url.ML					\
    17.6    General/xml.ML					\
    17.7 -  General/xml_data.ML					\
    17.8    General/yxml.ML					\
    17.9    Isar/args.ML						\
   17.10    Isar/attrib.ML					\
   17.11 @@ -131,7 +130,6 @@
   17.12    Isar/overloading.ML					\
   17.13    Isar/parse.ML						\
   17.14    Isar/parse_spec.ML					\
   17.15 -  Isar/parse_value.ML					\
   17.16    Isar/proof.ML						\
   17.17    Isar/proof_context.ML					\
   17.18    Isar/proof_display.ML					\
    18.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jul 13 00:43:07 2011 +0900
    18.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 12 20:53:14 2011 +0200
    18.3 @@ -766,7 +766,7 @@
    18.4  (* nested commands *)
    18.5  
    18.6  val props_text =
    18.7 -  Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
    18.8 +  Scan.optional Parse.properties [] -- Parse.position Parse.string
    18.9    >> (fn (props, (str, pos)) =>
   18.10        (Position.of_properties (Position.default_properties pos props), str));
   18.11  
    19.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 13 00:43:07 2011 +0900
    19.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Jul 12 20:53:14 2011 +0200
    19.3 @@ -11,6 +11,30 @@
    19.4  import scala.collection.mutable
    19.5  
    19.6  
    19.7 +object Outer_Syntax
    19.8 +{
    19.9 +  def quote_string(str: String): String =
   19.10 +  {
   19.11 +    val result = new StringBuilder(str.length + 10)
   19.12 +    result += '"'
   19.13 +    for (s <- Symbol.iterator(str)) {
   19.14 +      if (s.length == 1) {
   19.15 +        val c = s(0)
   19.16 +        if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
   19.17 +          result += '\\'
   19.18 +          if (c < 10) result += '0'
   19.19 +          if (c < 100) result += '0'
   19.20 +          result ++= (c.asInstanceOf[Int].toString)
   19.21 +        }
   19.22 +        else result += c
   19.23 +      }
   19.24 +      else result ++= s
   19.25 +    }
   19.26 +    result += '"'
   19.27 +    result.toString
   19.28 +  }
   19.29 +}
   19.30 +
   19.31  class Outer_Syntax
   19.32  {
   19.33    protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
    20.1 --- a/src/Pure/Isar/parse.ML	Wed Jul 13 00:43:07 2011 +0900
    20.2 +++ b/src/Pure/Isar/parse.ML	Tue Jul 12 20:53:14 2011 +0200
    20.3 @@ -60,6 +60,7 @@
    20.4    val and_list1': 'a context_parser -> 'a list context_parser
    20.5    val list: 'a parser -> 'a list parser
    20.6    val list1: 'a parser -> 'a list parser
    20.7 +  val properties: Properties.T parser
    20.8    val name: bstring parser
    20.9    val binding: binding parser
   20.10    val xname: xstring parser
   20.11 @@ -230,6 +231,8 @@
   20.12  fun list1 scan = enum1 "," scan;
   20.13  fun list scan = enum "," scan;
   20.14  
   20.15 +val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
   20.16 +
   20.17  
   20.18  (* names and text *)
   20.19  
    21.1 --- a/src/Pure/Isar/parse_value.ML	Wed Jul 13 00:43:07 2011 +0900
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,42 +0,0 @@
    21.4 -(*  Title:      Pure/Isar/parse_value.ML
    21.5 -    Author:     Makarius
    21.6 -
    21.7 -Outer syntax parsers for basic ML values.
    21.8 -*)
    21.9 -
   21.10 -signature PARSE_VALUE =
   21.11 -sig
   21.12 -  val comma: 'a parser -> 'a parser
   21.13 -  val equal: 'a parser -> 'a parser
   21.14 -  val parens: 'a parser -> 'a parser
   21.15 -  val unit: unit parser
   21.16 -  val pair: 'a parser -> 'b parser -> ('a * 'b) parser
   21.17 -  val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
   21.18 -  val list: 'a parser -> 'a list parser
   21.19 -  val properties: Properties.T parser
   21.20 -end;
   21.21 -
   21.22 -structure Parse_Value: PARSE_VALUE =
   21.23 -struct
   21.24 -
   21.25 -(* syntax utilities *)
   21.26 -
   21.27 -fun comma p = Parse.$$$ "," |-- Parse.!!! p;
   21.28 -fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
   21.29 -fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
   21.30 -
   21.31 -
   21.32 -(* tuples *)
   21.33 -
   21.34 -val unit = parens (Scan.succeed ());
   21.35 -fun pair p1 p2 = parens (p1 -- comma p2);
   21.36 -fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
   21.37 -
   21.38 -
   21.39 -(* lists *)
   21.40 -
   21.41 -fun list p = parens (Parse.enum "," p);
   21.42 -val properties = list (Parse.string -- equal Parse.string);
   21.43 -
   21.44 -end;
   21.45 -
    22.1 --- a/src/Pure/Isar/token.ML	Wed Jul 13 00:43:07 2011 +0900
    22.2 +++ b/src/Pure/Isar/token.ML	Tue Jul 12 20:53:14 2011 +0200
    22.3 @@ -191,15 +191,12 @@
    22.4  
    22.5  (* unparse *)
    22.6  
    22.7 -fun escape q =
    22.8 -  implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
    22.9 -
   22.10  fun unparse (Token (_, (kind, x), _)) =
   22.11    (case kind of
   22.12 -    String => x |> quote o escape "\""
   22.13 -  | AltString => x |> enclose "`" "`" o escape "`"
   22.14 -  | Verbatim => x |> enclose "{*" "*}"
   22.15 -  | Comment => x |> enclose "(*" "*)"
   22.16 +    String => Symbol_Pos.quote_string_qq x
   22.17 +  | AltString => Symbol_Pos.quote_string_bq x
   22.18 +  | Verbatim => enclose "{*" "*}" x
   22.19 +  | Comment => enclose "(*" "*)" x
   22.20    | Sync => ""
   22.21    | EOF => ""
   22.22    | _ => x);
    23.1 --- a/src/Pure/PIDE/document.scala	Wed Jul 13 00:43:07 2011 +0900
    23.2 +++ b/src/Pure/PIDE/document.scala	Tue Jul 12 20:53:14 2011 +0200
    23.3 @@ -16,12 +16,7 @@
    23.4    /* formal identifiers */
    23.5  
    23.6    type ID = Long
    23.7 -
    23.8 -  object ID
    23.9 -  {
   23.10 -    def apply(id: ID): String = Markup.Long.apply(id)
   23.11 -    def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
   23.12 -  }
   23.13 +  val ID = Properties.Value.Long
   23.14  
   23.15    type Version_ID = ID
   23.16    type Command_ID = ID
    24.1 --- a/src/Pure/PIDE/isar_document.ML	Wed Jul 13 00:43:07 2011 +0900
    24.2 +++ b/src/Pure/PIDE/isar_document.ML	Tue Jul 12 20:53:14 2011 +0200
    24.3 @@ -18,10 +18,10 @@
    24.4          val old_id = Document.parse_id old_id_string;
    24.5          val new_id = Document.parse_id new_id_string;
    24.6          val edits = YXML.parse_body edits_yxml |>
    24.7 -          let open XML_Data.Decode
    24.8 +          let open XML.Decode
    24.9            in list (pair string (option (list (pair (option int) (option int))))) end;
   24.10          val headers = YXML.parse_body headers_yxml |>
   24.11 -          let open XML_Data.Decode
   24.12 +          let open XML.Decode
   24.13            in list (pair string (triple string (list string) (list string))) end;
   24.14  
   24.15        val await_cancellation = Document.cancel_execution state;
    25.1 --- a/src/Pure/PIDE/isar_document.scala	Wed Jul 13 00:43:07 2011 +0900
    25.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Jul 12 20:53:14 2011 +0200
    25.3 @@ -143,12 +143,12 @@
    25.4        edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
    25.5    {
    25.6      val arg1 =
    25.7 -    { import XML_Data.Encode._
    25.8 +    { import XML.Encode._
    25.9        list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
   25.10  
   25.11      val arg2 =
   25.12 -    { import XML_Data.Encode._
   25.13 -      list(pair(string, Thy_Header.encode_xml_data))(headers) }
   25.14 +    { import XML.Encode._
   25.15 +      list(pair(string, Thy_Header.xml_encode))(headers) }
   25.16  
   25.17      input("Isar_Document.edit_version",
   25.18        Document.ID(old_id), Document.ID(new_id),
    26.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Jul 13 00:43:07 2011 +0900
    26.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 12 20:53:14 2011 +0200
    26.3 @@ -22,7 +22,7 @@
    26.4  val thm_depsN = "thm_deps";                (*meta-information about theorem deps*)
    26.5  val test_markupN = "test_markup";          (*XML markup for everything*)
    26.6  
    26.7 -fun special ch = Symbol.SOH ^ ch;
    26.8 +fun special ch = chr 1 ^ ch;
    26.9  
   26.10  
   26.11  (* render markup *)
    27.1 --- a/src/Pure/ROOT.ML	Wed Jul 13 00:43:07 2011 +0900
    27.2 +++ b/src/Pure/ROOT.ML	Tue Jul 12 20:53:14 2011 +0200
    27.3 @@ -53,7 +53,6 @@
    27.4  use "General/linear_set.ML";
    27.5  use "General/buffer.ML";
    27.6  use "General/xml.ML";
    27.7 -use "General/xml_data.ML";
    27.8  use "General/pretty.ML";
    27.9  use "General/path.ML";
   27.10  use "General/url.ML";
   27.11 @@ -189,7 +188,6 @@
   27.12  use "Isar/token.ML";
   27.13  use "Isar/keyword.ML";
   27.14  use "Isar/parse.ML";
   27.15 -use "Isar/parse_value.ML";
   27.16  use "Isar/args.ML";
   27.17  
   27.18  (*ML support*)
    28.1 --- a/src/Pure/System/isabelle_process.ML	Wed Jul 13 00:43:07 2011 +0900
    28.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Jul 12 20:53:14 2011 +0200
    28.3 @@ -66,17 +66,18 @@
    28.4  
    28.5  fun chunk s = [string_of_int (size s), "\n", s];
    28.6  
    28.7 -fun message _ _ _ "" = ()
    28.8 -  | message mbox ch raw_props body =
    28.9 -      let
   28.10 -        val robust_props = map (pairself YXML.escape_controls) raw_props;
   28.11 -        val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
   28.12 -      in Mailbox.send mbox (chunk header @ chunk body) end;
   28.13 +fun message mbox ch raw_props body =
   28.14 +  let
   28.15 +    val robust_props = map (pairself YXML.embed_controls) raw_props;
   28.16 +    val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
   28.17 +  in Mailbox.send mbox (chunk header @ chunk body) end;
   28.18  
   28.19  fun standard_message mbox with_serial ch body =
   28.20 -  message mbox ch
   28.21 -    ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
   28.22 -      (Position.properties_of (Position.thread_data ()))) body;
   28.23 +  if body = "" then ()
   28.24 +  else
   28.25 +    message mbox ch
   28.26 +      ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
   28.27 +        (Position.properties_of (Position.thread_data ()))) body;
   28.28  
   28.29  fun message_output mbox out_stream =
   28.30    let
    29.1 --- a/src/Pure/System/isabelle_process.scala	Wed Jul 13 00:43:07 2011 +0900
    29.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Jul 12 20:53:14 2011 +0200
    29.3 @@ -46,7 +46,7 @@
    29.4    class Result(val message: XML.Elem) extends Message
    29.5    {
    29.6      def kind: String = message.markup.name
    29.7 -    def properties: XML.Attributes = message.markup.properties
    29.8 +    def properties: Properties.T = message.markup.properties
    29.9      def body: XML.Body = message.body
   29.10  
   29.11      def is_init = kind == Markup.INIT
   29.12 @@ -95,7 +95,7 @@
   29.13  
   29.14    private val xml_cache = new XML.Cache()
   29.15  
   29.16 -  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   29.17 +  private def put_result(kind: String, props: Properties.T, body: XML.Body)
   29.18    {
   29.19      if (kind == Markup.INIT) rm_fifos()
   29.20      if (kind == Markup.RAW)
    30.1 --- a/src/Pure/System/isabelle_syntax.scala	Wed Jul 13 00:43:07 2011 +0900
    30.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.3 @@ -1,74 +0,0 @@
    30.4 -/*  Title:      Pure/System/isabelle_syntax.scala
    30.5 -    Author:     Makarius
    30.6 -
    30.7 -Isabelle outer syntax.
    30.8 -*/
    30.9 -
   30.10 -package isabelle
   30.11 -
   30.12 -
   30.13 -object Isabelle_Syntax
   30.14 -{
   30.15 -  /* string token */
   30.16 -
   30.17 -  def append_string(str: String, result: StringBuilder)
   30.18 -  {
   30.19 -    result.append("\"")
   30.20 -    for (c <- str) {
   30.21 -      if (c < 32 || c == '\\' || c == '\"') {
   30.22 -        result.append("\\")
   30.23 -        if (c < 10) result.append('0')
   30.24 -        if (c < 100) result.append('0')
   30.25 -        result.append(c.asInstanceOf[Int].toString)
   30.26 -      }
   30.27 -      else result.append(c)
   30.28 -    }
   30.29 -    result.append("\"")
   30.30 -  }
   30.31 -
   30.32 -  def encode_string(str: String) =
   30.33 -  {
   30.34 -    val result = new StringBuilder(str.length + 10)
   30.35 -    append_string(str, result)
   30.36 -    result.toString
   30.37 -  }
   30.38 -
   30.39 -
   30.40 -  /* list */
   30.41 -
   30.42 -  def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
   30.43 -    result: StringBuilder)
   30.44 -  {
   30.45 -    result.append("(")
   30.46 -    val elems = body.iterator
   30.47 -    if (elems.hasNext) append_elem(elems.next, result)
   30.48 -    while (elems.hasNext) {
   30.49 -      result.append(", ")
   30.50 -      append_elem(elems.next, result)
   30.51 -    }
   30.52 -    result.append(")")
   30.53 -  }
   30.54 -
   30.55 -  def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
   30.56 -  {
   30.57 -    val result = new StringBuilder
   30.58 -    append_list(append_elem, elems, result)
   30.59 -    result.toString
   30.60 -  }
   30.61 -
   30.62 -
   30.63 -  /* properties */
   30.64 -
   30.65 -  def append_properties(props: List[(String, String)], result: StringBuilder)
   30.66 -  {
   30.67 -    append_list((p: (String, String), res) =>
   30.68 -      { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
   30.69 -  }
   30.70 -
   30.71 -  def encode_properties(props: List[(String, String)]) =
   30.72 -  {
   30.73 -    val result = new StringBuilder
   30.74 -    append_properties(props, result)
   30.75 -    result.toString
   30.76 -  }
   30.77 -}
    31.1 --- a/src/Pure/Thy/thy_header.scala	Wed Jul 13 00:43:07 2011 +0900
    31.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Jul 12 20:53:14 2011 +0200
    31.3 @@ -31,10 +31,10 @@
    31.4        Header(f(name), imports.map(f), uses.map(f))
    31.5    }
    31.6  
    31.7 -  val encode_xml_data: XML_Data.Encode.T[Header] =
    31.8 +  val xml_encode: XML.Encode.T[Header] =
    31.9    {
   31.10      case Header(name, imports, uses) =>
   31.11 -      import XML_Data.Encode._
   31.12 +      import XML.Encode._
   31.13        triple(string, list(string), list(string))(name, imports, uses)
   31.14    }
   31.15  
    32.1 --- a/src/Pure/Tools/find_theorems.ML	Wed Jul 13 00:43:07 2011 +0900
    32.2 +++ b/src/Pure/Tools/find_theorems.ML	Tue Jul 12 20:53:14 2011 +0200
    32.3 @@ -139,8 +139,8 @@
    32.4            |> (if rem_dups then cons ("rem_dups", "") else I)
    32.5            |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
    32.6        in
    32.7 -        XML.Elem (("Query", properties), XML_Data.Encode.list
    32.8 -          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
    32.9 +        XML.Elem (("Query", properties), XML.Encode.list
   32.10 +          (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
   32.11        end
   32.12    | xml_of_query _ = raise Fail "cannot serialize goal";
   32.13  
   32.14 @@ -149,7 +149,7 @@
   32.15          val rem_dups = Properties.defined properties "rem_dups";
   32.16          val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
   32.17          val criteria =
   32.18 -          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
   32.19 +          XML.Decode.list (XML.Decode.pair XML.Decode.bool
   32.20              (criterion_of_xml o the_single)) body;
   32.21        in
   32.22          {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
   32.23 @@ -190,12 +190,12 @@
   32.24      val properties =
   32.25        if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   32.26    in
   32.27 -    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
   32.28 +    XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
   32.29    end;
   32.30  
   32.31  fun result_of_xml (XML.Elem (("Result", properties), body)) =
   32.32        (Properties.get properties "found" |> Option.map Markup.parse_int,
   32.33 -       XML_Data.Decode.list (theorem_of_xml o the_single) body)
   32.34 +       XML.Decode.list (theorem_of_xml o the_single) body)
   32.35    | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
   32.36  
   32.37  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
    33.1 --- a/src/Pure/build-jars	Wed Jul 13 00:43:07 2011 +0900
    33.2 +++ b/src/Pure/build-jars	Tue Jul 12 20:53:14 2011 +0200
    33.3 @@ -20,11 +20,11 @@
    33.4    General/path.scala
    33.5    General/position.scala
    33.6    General/pretty.scala
    33.7 +  General/properties.scala
    33.8    General/scan.scala
    33.9    General/sha1.scala
   33.10    General/symbol.scala
   33.11    General/xml.scala
   33.12 -  General/xml_data.scala
   33.13    General/yxml.scala
   33.14    Isar/keyword.scala
   33.15    Isar/outer_syntax.scala
   33.16 @@ -43,7 +43,6 @@
   33.17    System/invoke_scala.scala
   33.18    System/isabelle_charset.scala
   33.19    System/isabelle_process.scala
   33.20 -  System/isabelle_syntax.scala
   33.21    System/isabelle_system.scala
   33.22    System/platform.scala
   33.23    System/session.scala
   33.24 @@ -59,6 +58,7 @@
   33.25    library.scala
   33.26    package.scala
   33.27    term.scala
   33.28 +  term_xml.scala
   33.29  )
   33.30  
   33.31  
    34.1 --- a/src/Pure/more_thm.ML	Wed Jul 13 00:43:07 2011 +0900
    34.2 +++ b/src/Pure/more_thm.ML	Tue Jul 12 20:53:14 2011 +0200
    34.3 @@ -76,9 +76,9 @@
    34.4    val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
    34.5    val no_attributes: 'a -> 'a * 'b list
    34.6    val simple_fact: 'a -> ('a * 'b list) list
    34.7 -  val tag_rule: Properties.property -> thm -> thm
    34.8 +  val tag_rule: Properties.entry -> thm -> thm
    34.9    val untag_rule: string -> thm -> thm
   34.10 -  val tag: Properties.property -> attribute
   34.11 +  val tag: Properties.entry -> attribute
   34.12    val untag: string -> attribute
   34.13    val def_name: string -> string
   34.14    val def_name_optional: string -> string -> string
    35.1 --- a/src/Pure/pure_setup.ML	Wed Jul 13 00:43:07 2011 +0900
    35.2 +++ b/src/Pure/pure_setup.ML	Tue Jul 12 20:53:14 2011 +0200
    35.3 @@ -18,6 +18,7 @@
    35.4  
    35.5  (* ML toplevel pretty printing *)
    35.6  
    35.7 +toplevel_pp ["XML", "tree"] "Pretty.str o XML.string_of";
    35.8  toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
    35.9  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
   35.10  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
    36.1 --- a/src/Pure/term.scala	Wed Jul 13 00:43:07 2011 +0900
    36.2 +++ b/src/Pure/term.scala	Tue Jul 12 20:53:14 2011 +0200
    36.3 @@ -1,7 +1,7 @@
    36.4  /*  Title:      Pure/term.scala
    36.5      Author:     Makarius
    36.6  
    36.7 -Lambda terms with XML data representation.
    36.8 +Lambda terms, types, sorts.
    36.9  
   36.10  Note: Isabelle/ML is the primary environment for logical operations.
   36.11  */
   36.12 @@ -11,8 +11,6 @@
   36.13  
   36.14  object Term
   36.15  {
   36.16 -  /* basic type definitions */
   36.17 -
   36.18    type Indexname = (String, Int)
   36.19  
   36.20    type Sort = List[String]
   36.21 @@ -33,59 +31,3 @@
   36.22    case class App(fun: Term, arg: Term) extends Term
   36.23  }
   36.24  
   36.25 -
   36.26 -object Term_XML
   36.27 -{
   36.28 -  import Term._
   36.29 -
   36.30 -
   36.31 -  /* XML data representation */
   36.32 -
   36.33 -  object Encode
   36.34 -  {
   36.35 -    import XML_Data.Encode._
   36.36 -
   36.37 -    val indexname: T[Indexname] = pair(string, int)
   36.38 -
   36.39 -    val sort: T[Sort] = list(string)
   36.40 -
   36.41 -    def typ: T[Typ] =
   36.42 -      variant[Typ](List(
   36.43 -        { case Type(a, b) => pair(string, list(typ))((a, b)) },
   36.44 -        { case TFree(a, b) => pair(string, sort)((a, b)) },
   36.45 -        { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
   36.46 -
   36.47 -    def term: T[Term] =
   36.48 -      variant[Term](List(
   36.49 -        { case Const(a, b) => pair(string, typ)((a, b)) },
   36.50 -        { case Free(a, b) => pair(string, typ)((a, b)) },
   36.51 -        { case Var(a, b) => pair(indexname, typ)((a, b)) },
   36.52 -        { case Bound(a) => int(a) },
   36.53 -        { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
   36.54 -        { case App(a, b) => pair(term, term)((a, b)) }))
   36.55 -  }
   36.56 -
   36.57 -  object Decode
   36.58 -  {
   36.59 -    import XML_Data.Decode._
   36.60 -
   36.61 -    val indexname: T[Indexname] = pair(string, int)
   36.62 -
   36.63 -    val sort: T[Sort] = list(string)
   36.64 -
   36.65 -    def typ: T[Typ] =
   36.66 -      variant[Typ](List(
   36.67 -        (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
   36.68 -        (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
   36.69 -        (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
   36.70 -
   36.71 -    def term: T[Term] =
   36.72 -      variant[Term](List(
   36.73 -        (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
   36.74 -        (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
   36.75 -        (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
   36.76 -        (x => Bound(int(x))),
   36.77 -        (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
   36.78 -        (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
   36.79 -  }
   36.80 -}
    37.1 --- a/src/Pure/term_xml.ML	Wed Jul 13 00:43:07 2011 +0900
    37.2 +++ b/src/Pure/term_xml.ML	Tue Jul 12 20:53:14 2011 +0200
    37.3 @@ -7,7 +7,6 @@
    37.4  signature TERM_XML_OPS =
    37.5  sig
    37.6    type 'a T
    37.7 -  val indexname: indexname T
    37.8    val sort: sort T
    37.9    val typ: typ T
   37.10    val term: term T
   37.11 @@ -15,63 +14,54 @@
   37.12  
   37.13  signature TERM_XML =
   37.14  sig
   37.15 -  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
   37.16 -  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
   37.17 +  structure Encode: TERM_XML_OPS
   37.18 +  structure Decode: TERM_XML_OPS
   37.19  end;
   37.20  
   37.21  structure Term_XML: TERM_XML =
   37.22  struct
   37.23  
   37.24 -(* encode *)
   37.25 -
   37.26  structure Encode =
   37.27  struct
   37.28  
   37.29 -open XML_Data.Encode;
   37.30 -
   37.31 -val indexname = pair string int;
   37.32 +open XML.Encode;
   37.33  
   37.34  val sort = list string;
   37.35  
   37.36  fun typ T = T |> variant
   37.37 - [fn Type x => pair string (list typ) x,
   37.38 -  fn TFree x => pair string sort x,
   37.39 -  fn TVar x => pair indexname sort x];
   37.40 + [fn Type (a, b) => ([a], (list typ) b),
   37.41 +  fn TFree (a, b) => ([a], sort b),
   37.42 +  fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
   37.43  
   37.44  fun term t = t |> variant
   37.45 - [fn Const x => pair string typ x,
   37.46 -  fn Free x => pair string typ x,
   37.47 -  fn Var x => pair indexname typ x,
   37.48 -  fn Bound x => int x,
   37.49 -  fn Abs x => triple string typ term x,
   37.50 -  fn op $ x => pair term term x];
   37.51 + [fn Const (a, b) => ([a], typ b),
   37.52 +  fn Free (a, b) => ([a], typ b),
   37.53 +  fn Var ((a, b), c) => ([a, int_atom b], typ c),
   37.54 +  fn Bound a => ([int_atom a], []),
   37.55 +  fn Abs (a, b, c) => ([a], pair typ term (b, c)),
   37.56 +  fn a $ b => ([], pair term term (a, b))];
   37.57  
   37.58  end;
   37.59  
   37.60 -
   37.61 -(* decode *)
   37.62 -
   37.63  structure Decode =
   37.64  struct
   37.65  
   37.66 -open XML_Data.Decode;
   37.67 -
   37.68 -val indexname = pair string int;
   37.69 +open XML.Decode;
   37.70  
   37.71  val sort = list string;
   37.72  
   37.73  fun typ T = T |> variant
   37.74 - [Type o pair string (list typ),
   37.75 -  TFree o pair string sort,
   37.76 -  TVar o pair indexname sort];
   37.77 + [fn ([a], b) => Type (a, list typ b),
   37.78 +  fn ([a], b) => TFree (a, sort b),
   37.79 +  fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
   37.80  
   37.81  fun term t = t |> variant
   37.82 - [Const o pair string typ,
   37.83 -  Free o pair string typ,
   37.84 -  Var o pair indexname typ,
   37.85 -  Bound o int,
   37.86 -  Abs o triple string typ term,
   37.87 -  op $ o pair term term];
   37.88 + [fn ([a], b) => Const (a, typ b),
   37.89 +  fn ([a], b) => Free (a, typ b),
   37.90 +  fn ([a, b], c) => Var ((a, int_atom b), typ c),
   37.91 +  fn ([a], []) => Bound (int_atom a),
   37.92 +  fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end,
   37.93 +  fn ([], a) => op $ (pair term term a)];
   37.94  
   37.95  end;
   37.96  
    38.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.2 +++ b/src/Pure/term_xml.scala	Tue Jul 12 20:53:14 2011 +0200
    38.3 @@ -0,0 +1,57 @@
    38.4 +/*  Title:      Pure/term_xml.scala
    38.5 +    Author:     Makarius
    38.6 +
    38.7 +XML data representation of lambda terms.
    38.8 +*/
    38.9 +
   38.10 +package isabelle
   38.11 +
   38.12 +
   38.13 +object Term_XML
   38.14 +{
   38.15 +  import Term._
   38.16 +
   38.17 +  object Encode
   38.18 +  {
   38.19 +    import XML.Encode._
   38.20 +
   38.21 +    val sort: T[Sort] = list(string)
   38.22 +
   38.23 +    def typ: T[Typ] =
   38.24 +      variant[Typ](List(
   38.25 +        { case Type(a, b) => (List(a), list(typ)(b)) },
   38.26 +        { case TFree(a, b) => (List(a), sort(b)) },
   38.27 +        { case TVar((a, b), c) => (List(a, int_atom(b)), sort(c)) }))
   38.28 +
   38.29 +    def term: T[Term] =
   38.30 +      variant[Term](List(
   38.31 +        { case Const(a, b) => (List(a), typ(b)) },
   38.32 +        { case Free(a, b) => (List(a), typ(b)) },
   38.33 +        { case Var((a, b), c) => (List(a, int_atom(b)), typ(c)) },
   38.34 +        { case Bound(a) => (List(int_atom(a)), Nil) },
   38.35 +        { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
   38.36 +        { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
   38.37 +  }
   38.38 +
   38.39 +  object Decode
   38.40 +  {
   38.41 +    import XML.Decode._
   38.42 +
   38.43 +    val sort: T[Sort] = list(string)
   38.44 +
   38.45 +    def typ: T[Typ] =
   38.46 +      variant[Typ](List(
   38.47 +        { case (List(a), b) => Type(a, list(typ)(b)) },
   38.48 +        { case (List(a), b) => TFree(a, sort(b)) },
   38.49 +        { case (List(a, b), c) => TVar((a, int_atom(b)), sort(c)) }))
   38.50 +
   38.51 +    def term: T[Term] =
   38.52 +      variant[Term](List(
   38.53 +        { case (List(a), b) => Const(a, typ(b)) },
   38.54 +        { case (List(a), b) => Free(a, typ(b)) },
   38.55 +        { case (List(a, b), c) => Var((a, int_atom(b)), typ(c)) },
   38.56 +        { case (List(a), Nil) => Bound(int_atom(a)) },
   38.57 +        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
   38.58 +        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
   38.59 +  }
   38.60 +}