--- a/lib/fonts/IsabelleText.sfd Wed Jul 13 00:43:07 2011 +0900
+++ b/lib/fonts/IsabelleText.sfd Tue Jul 12 20:53:14 2011 +0200
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1308688123
+ModificationTime: 1310461984
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2241,9 +2241,9 @@
DisplaySize: -48
AntiAlias: 1
FitToEm: 1
-WinInfo: 8608 16 10
+WinInfo: 0 16 10
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
-BeginChars: 1114189 1090
+BeginChars: 1114189 1094
StartChar: u10000
Encoding: 65536 65536 0
@@ -55412,7 +55412,7 @@
StartChar: uni21D6
Encoding: 8662 8662 1086
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -55438,7 +55438,7 @@
StartChar: uni21D7
Encoding: 8663 8663 1087
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -55464,7 +55464,7 @@
StartChar: uni21D8
Encoding: 8664 8664 1088
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -55490,7 +55490,7 @@
StartChar: uni21D9
Encoding: 8665 8665 1089
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -55512,5 +55512,103 @@
398 127 l 1,0,-1
EndSplineSet
EndChar
+
+StartChar: uni0005
+Encoding: 5 5 1090
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1071 0 m 1,0,-1
+ 780 0 l 1,1,-1
+ 580 512 l 1,2,-1
+ 180 0 l 1,3,-1
+ -143 0 l 1,4,-1
+ 471 782 l 1,5,-1
+ 184 1493 l 1,6,-1
+ 475 1493 l 1,7,-1
+ 662 1030 l 1,8,-1
+ 1022 1493 l 1,9,-1
+ 1343 1493 l 1,10,-1
+ 770 756 l 1,11,-1
+ 1071 0 l 1,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni0006
+Encoding: 6 6 1091
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+145 1493 m 1,0,-1
+ 438 1493 l 1,1,-1
+ 625 844 l 1,2,-1
+ 1036 1493 l 1,3,-1
+ 1358 1493 l 1,4,-1
+ 725 588 l 1,5,-1
+ 610 0 l 1,6,-1
+ 317 0 l 1,7,-1
+ 432 588 l 1,8,-1
+ 145 1493 l 1,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni007F
+Encoding: 127 127 1092
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+994 410 m 1,0,-1
+ 994 983 l 1,1,-1
+ 886.193 983 l 1,2,-1
+ 685.584 696.5 l 1,3,-1
+ 886.193 410 l 1,4,-1
+ 994 410 l 1,0,-1
+1108 296 m 1,5,-1
+ 125 296 l 1,6,-1
+ 125 1097 l 1,7,-1
+ 1108 1097 l 1,8,-1
+ 1108 296 l 1,5,-1
+484.976 983 m 1,9,-1
+ 616 795.877 l 1,10,-1
+ 747.024 983 l 1,11,-1
+ 484.976 983 l 1,9,-1
+345.807 983 m 1,12,-1
+ 239 983 l 1,13,-1
+ 239 410 l 1,14,-1
+ 345.807 410 l 1,15,-1
+ 546.416 696.5 l 1,16,-1
+ 345.807 983 l 1,12,-1
+747.024 410 m 1,17,-1
+ 616 597.123 l 1,18,-1
+ 484.976 410 l 1,19,-1
+ 747.024 410 l 1,17,-1
+EndSplineSet
+EndChar
+
+StartChar: uni0007
+Encoding: 7 7 1093
+Width: 1233
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+104 -362 m 1,0,-1
+ 104 1444 l 1,1,-1
+ 1128 1444 l 1,2,-1
+ 1128 -362 l 1,3,-1
+ 104 -362 l 1,0,-1
+219 -248 m 1,4,-1
+ 1014 -248 l 1,5,-1
+ 1014 1329 l 1,6,-1
+ 219 1329 l 1,7,-1
+ 219 -248 l 1,4,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
Binary file lib/fonts/IsabelleText.ttf has changed
--- a/lib/fonts/IsabelleTextBold.sfd Wed Jul 13 00:43:07 2011 +0900
+++ b/lib/fonts/IsabelleTextBold.sfd Tue Jul 12 20:53:14 2011 +0200
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1308688237
+ModificationTime: 1310462018
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1675,8 +1675,8 @@
DisplaySize: -48
AntiAlias: 1
FitToEm: 1
-WinInfo: 8576 16 10
-BeginChars: 1114112 1079
+WinInfo: 0 16 10
+BeginChars: 1114112 1083
StartChar: u10000
Encoding: 65536 65536 0
@@ -58428,7 +58428,7 @@
StartChar: uni21D6
Encoding: 8662 8662 1075
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -58454,7 +58454,7 @@
StartChar: uni21D7
Encoding: 8663 8663 1076
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -58480,7 +58480,7 @@
StartChar: uni21D8
Encoding: 8664 8664 1077
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -58506,7 +58506,7 @@
StartChar: uni21D9
Encoding: 8665 8665 1078
Width: 1233
-Flags: HW
+Flags: W
LayerCount: 2
Fore
SplineSet
@@ -58528,5 +58528,103 @@
312 243 l 1,0,-1
EndSplineSet
EndChar
+
+StartChar: uni0005
+Encoding: 5 5 1079
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1071 0 m 1,0,-1
+ 780 0 l 1,1,-1
+ 580 512 l 1,2,-1
+ 180 0 l 1,3,-1
+ -143 0 l 1,4,-1
+ 471 782 l 1,5,-1
+ 184 1493 l 1,6,-1
+ 475 1493 l 1,7,-1
+ 662 1030 l 1,8,-1
+ 1022 1493 l 1,9,-1
+ 1343 1493 l 1,10,-1
+ 770 756 l 1,11,-1
+ 1071 0 l 1,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni0006
+Encoding: 6 6 1080
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+145 1493 m 1,0,-1
+ 438 1493 l 1,1,-1
+ 625 844 l 1,2,-1
+ 1036 1493 l 1,3,-1
+ 1358 1493 l 1,4,-1
+ 725 588 l 1,5,-1
+ 610 0 l 1,6,-1
+ 317 0 l 1,7,-1
+ 432 588 l 1,8,-1
+ 145 1493 l 1,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni007F
+Encoding: 127 127 1081
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+1138 296 m 1,0,-1
+ 95 296 l 1,1,-1
+ 95 1097 l 1,2,-1
+ 1138 1097 l 1,3,-1
+ 1138 296 l 1,0,-1
+994 440 m 1,4,-1
+ 994 953 l 1,5,-1
+ 875.188 953 l 1,6,-1
+ 695.584 696.5 l 1,7,-1
+ 875.188 440 l 1,8,-1
+ 994 440 l 1,4,-1
+515.981 953 m 1,9,-1
+ 616 810.158 l 1,10,-1
+ 716.019 953 l 1,11,-1
+ 515.981 953 l 1,9,-1
+239 440 m 1,12,-1
+ 356.812 440 l 1,13,-1
+ 536.416 696.5 l 1,14,-1
+ 356.812 953 l 1,15,-1
+ 239 953 l 1,16,-1
+ 239 440 l 1,12,-1
+716.019 440 m 1,17,-1
+ 616 582.842 l 1,18,-1
+ 515.981 440 l 1,19,-1
+ 716.019 440 l 1,17,-1
+EndSplineSet
+EndChar
+
+StartChar: uni0007
+Encoding: 7 7 1082
+Width: 1233
+Flags: HW
+LayerCount: 2
+Fore
+SplineSet
+104 -362 m 1,0,-1
+ 104 1444 l 1,1,-1
+ 1128 1444 l 1,2,-1
+ 1128 -362 l 1,3,-1
+ 104 -362 l 1,0,-1
+219 -248 m 1,4,-1
+ 1014 -248 l 1,5,-1
+ 1014 1329 l 1,6,-1
+ 219 1329 l 1,7,-1
+ 219 -248 l 1,4,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
Binary file lib/fonts/IsabelleTextBold.ttf has changed
--- a/src/Pure/General/markup.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/markup.scala Tue Jul 12 20:53:14 2011 +0200
@@ -9,73 +9,6 @@
object Markup
{
- /* plain values */
-
- object Int
- {
- def apply(x: scala.Int): String = x.toString
- def unapply(s: String): Option[scala.Int] =
- try { Some(Integer.parseInt(s)) }
- catch { case _: NumberFormatException => None }
- }
-
- object Long
- {
- def apply(x: scala.Long): String = x.toString
- def unapply(s: String): Option[scala.Long] =
- try { Some(java.lang.Long.parseLong(s)) }
- catch { case _: NumberFormatException => None }
- }
-
- object Double
- {
- def apply(x: scala.Double): String = x.toString
- def unapply(s: String): Option[scala.Double] =
- try { Some(java.lang.Double.parseDouble(s)) }
- catch { case _: NumberFormatException => None }
- }
-
-
- /* named properties */
-
- class Property(val name: String)
- {
- def apply(value: String): List[(String, String)] = List((name, value))
- def unapply(props: List[(String, String)]): Option[String] =
- props.find(_._1 == name).map(_._2)
- }
-
- class Int_Property(name: String)
- {
- def apply(value: scala.Int): List[(String, String)] = List((name, Int(value)))
- def unapply(props: List[(String, String)]): Option[Int] =
- props.find(_._1 == name) match {
- case None => None
- case Some((_, value)) => Int.unapply(value)
- }
- }
-
- class Long_Property(name: String)
- {
- def apply(value: scala.Long): List[(String, String)] = List((name, Long(value)))
- def unapply(props: List[(String, String)]): Option[Long] =
- props.find(_._1 == name) match {
- case None => None
- case Some((_, value)) => Long.unapply(value)
- }
- }
-
- class Double_Property(name: String)
- {
- def apply(value: scala.Double): List[(String, String)] = List((name, Double(value)))
- def unapply(props: List[(String, String)]): Option[Double] =
- props.find(_._1 == name) match {
- case None => None
- case Some((_, value)) => Double.unapply(value)
- }
- }
-
-
/* empty */
val Empty = Markup("", Nil)
@@ -84,10 +17,10 @@
/* misc properties */
val NAME = "name"
- val Name = new Property(NAME)
+ val Name = new Properties.String(NAME)
val KIND = "kind"
- val Kind = new Property(KIND)
+ val Kind = new Properties.String(KIND)
/* formal entities */
@@ -145,9 +78,9 @@
/* pretty printing */
- val Indent = new Int_Property("indent")
+ val Indent = new Properties.Int("indent")
val BLOCK = "block"
- val Width = new Int_Property("width")
+ val Width = new Properties.Int("width")
val BREAK = "break"
@@ -260,13 +193,15 @@
{
def apply(timing: isabelle.Timing): Markup =
Markup(TIMING, List(
- (ELAPSED, Double(timing.elapsed.seconds)),
- (CPU, Double(timing.cpu.seconds)),
- (GC, Double(timing.gc.seconds))))
+ (ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
+ (CPU, Properties.Value.Double(timing.cpu.seconds)),
+ (GC, Properties.Value.Double(timing.gc.seconds))))
def unapply(markup: Markup): Option[isabelle.Timing] =
markup match {
case Markup(TIMING, List(
- (ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) =>
+ (ELAPSED, Properties.Value.Double(elapsed)),
+ (CPU, Properties.Value.Double(cpu)),
+ (GC, Properties.Value.Double(gc)))) =>
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
case _ => None
}
@@ -310,7 +245,7 @@
/* messages */
- val Serial = new Long_Property("serial")
+ val Serial = new Properties.Long("serial")
val MESSAGE = "message"
@@ -336,12 +271,12 @@
/* raw message functions */
val FUNCTION = "function"
- val Function = new Property(FUNCTION)
+ val Function = new Properties.String(FUNCTION)
val INVOKE_SCALA = "invoke_scala"
object Invoke_Scala
{
- def unapply(props: List[(String, String)]): Option[(String, String)] =
+ def unapply(props: Properties.T): Option[(String, String)] =
props match {
case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
case _ => None
@@ -354,4 +289,4 @@
val Data = Markup("data", Nil)
}
-sealed case class Markup(name: String, properties: List[(String, String)])
+sealed case class Markup(name: String, properties: Properties.T)
--- a/src/Pure/General/position.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/position.scala Tue Jul 12 20:53:14 2011 +0200
@@ -9,13 +9,13 @@
object Position
{
- type T = List[(String, String)]
+ type T = Properties.T
- val Line = new Markup.Int_Property(Markup.LINE)
- val Offset = new Markup.Int_Property(Markup.OFFSET)
- val End_Offset = new Markup.Int_Property(Markup.END_OFFSET)
- val File = new Markup.Property(Markup.FILE)
- val Id = new Markup.Long_Property(Markup.ID)
+ val Line = new Properties.Int(Markup.LINE)
+ val Offset = new Properties.Int(Markup.OFFSET)
+ val End_Offset = new Properties.Int(Markup.END_OFFSET)
+ val File = new Properties.String(Markup.FILE)
+ val Id = new Properties.Long(Markup.ID)
object Range
{
--- a/src/Pure/General/properties.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/properties.ML Tue Jul 12 20:53:14 2011 +0200
@@ -6,27 +6,30 @@
signature PROPERTIES =
sig
- type property = string * string
- type T = property list
+ type entry = string * string
+ type T = entry list
val defined: T -> string -> bool
val get: T -> string -> string option
val get_int: T -> string -> int option
- val put: string * string -> T -> T
+ val put: entry -> T -> T
+ val put_int: string * int -> T -> T
val remove: string -> T -> T
end;
structure Properties: PROPERTIES =
struct
-type property = string * string;
-type T = property list;
+type entry = string * string;
+type T = entry list;
fun defined (props: T) name = AList.defined (op =) props name;
fun get (props: T) name = AList.lookup (op =) props name;
fun get_int props name = (case get props name of NONE => NONE | SOME s => Int.fromString s);
-fun put prop (props: T) = AList.update (op =) prop props;
+fun put entry (props: T) = AList.update (op =) entry props;
+fun put_int (name, i) = put (name, signed_string_of_int i);
+
fun remove name (props: T) = AList.delete (op =) name props;
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/properties.scala Tue Jul 12 20:53:14 2011 +0200
@@ -0,0 +1,84 @@
+/* Title: Pure/General/properties.scala
+ Author: Makarius
+
+Property lists.
+*/
+
+package isabelle
+
+
+object Properties
+{
+ /* plain values */
+
+ object Value
+ {
+ object Int
+ {
+ def apply(x: scala.Int): java.lang.String = x.toString
+ def unapply(s: java.lang.String): Option[scala.Int] =
+ try { Some(Integer.parseInt(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+
+ object Long
+ {
+ def apply(x: scala.Long): java.lang.String = x.toString
+ def unapply(s: java.lang.String): Option[scala.Long] =
+ try { Some(java.lang.Long.parseLong(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+
+ object Double
+ {
+ def apply(x: scala.Double): java.lang.String = x.toString
+ def unapply(s: java.lang.String): Option[scala.Double] =
+ try { Some(java.lang.Double.parseDouble(s)) }
+ catch { case _: NumberFormatException => None }
+ }
+ }
+
+
+ /* named entries */
+
+ type Entry = (java.lang.String, java.lang.String)
+ type T = List[Entry]
+
+ class String(val name: java.lang.String)
+ {
+ def apply(value: java.lang.String): T = List((name, value))
+ def unapply(props: T): Option[java.lang.String] =
+ props.find(_._1 == name).map(_._2)
+ }
+
+ class Int(name: java.lang.String)
+ {
+ def apply(value: scala.Int): T = List((name, Value.Int(value)))
+ def unapply(props: T): Option[scala.Int] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Value.Int.unapply(value)
+ }
+ }
+
+ class Long(name: java.lang.String)
+ {
+ def apply(value: scala.Long): T = List((name, Value.Long(value)))
+ def unapply(props: T): Option[scala.Long] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Value.Long.unapply(value)
+ }
+ }
+
+ class Double(name: java.lang.String)
+ {
+ def apply(value: scala.Double): T = List((name, Value.Double(value)))
+ def unapply(props: T): Option[scala.Double] =
+ props.find(_._1 == name) match {
+ case None => None
+ case Some((_, value)) => Value.Double.unapply(value)
+ }
+ }
+}
+
--- a/src/Pure/General/symbol.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/symbol.ML Tue Jul 12 20:53:14 2011 +0200
@@ -7,10 +7,7 @@
signature SYMBOL =
sig
type symbol = string
- val SOH: symbol
val STX: symbol
- val ENQ: symbol
- val ACK: symbol
val DEL: symbol
val space: symbol
val spaces: int -> string
@@ -89,10 +86,7 @@
type symbol = string;
-val SOH = chr 1;
val STX = chr 2;
-val ENQ = chr 5;
-val ACK = chr 6;
val DEL = chr 127;
val space = chr 32;
--- a/src/Pure/General/symbol_pos.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/symbol_pos.ML Tue Jul 12 20:53:14 2011 +0200
@@ -19,6 +19,9 @@
val scan_string_q: T list -> (Position.T * (T list * Position.T)) * T list
val scan_string_qq: T list -> (Position.T * (T list * Position.T)) * T list
val scan_string_bq: T list -> (Position.T * (T list * Position.T)) * T list
+ val quote_string_q: string -> string
+ val quote_string_qq: string -> string
+ val quote_string_bq: string -> string
val scan_comment: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
T list -> T list * T list
val scan_comment_body: (string -> (T list -> T list * T list) -> T list -> T list * T list) ->
@@ -75,7 +78,7 @@
val scan_pos = Scan.ahead (Scan.one (K true)) >> (fn (_, pos): T => pos);
-(* Isabelle strings *)
+(* scan string literals *)
local
@@ -104,6 +107,29 @@
end;
+(* quote string literals *)
+
+local
+
+fun char_code i =
+ (if i < 10 then "00" else if i < 100 then "0" else "") ^ string_of_int i;
+
+fun quote_str q s =
+ if Symbol.is_ascii_control s then "\\" ^ char_code (ord s)
+ else if s = q orelse s = "\\" then "\\" ^ s
+ else s;
+
+fun quote_string q = enclose q q o implode o map (quote_str q) o Symbol.explode;
+
+in
+
+val quote_string_q = quote_string "'";
+val quote_string_qq = quote_string "\"";
+val quote_string_bq = quote_string "`";
+
+end;
+
+
(* ML-style comments *)
local
--- a/src/Pure/General/xml.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/xml.ML Tue Jul 12 20:53:14 2011 +0200
@@ -1,9 +1,29 @@
(* Title: Pure/General/xml.ML
Author: David Aspinall, Stefan Berghofer and Markus Wenzel
-Simple XML tree values.
+Untyped XML trees.
*)
+signature XML_DATA_OPS =
+sig
+ type 'a A
+ type 'a T
+ type 'a V
+ val int_atom: int A
+ val bool_atom: bool A
+ val unit_atom: unit A
+ val properties: Properties.T T
+ val string: string T
+ val int: int T
+ val bool: bool T
+ val unit: unit T
+ val pair: 'a T -> 'b T -> ('a * 'b) T
+ val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
+ val list: 'a T -> 'a list T
+ val option: 'a T -> 'a option T
+ val variant: 'a V list -> 'a T
+end;
+
signature XML =
sig
type attributes = Properties.T
@@ -24,6 +44,10 @@
val parse_element: string list -> tree * string list
val parse_document: string list -> tree * string list
val parse: string -> tree
+ exception XML_ATOM of string
+ exception XML_BODY of body
+ structure Encode: XML_DATA_OPS
+ structure Decode: XML_DATA_OPS
end;
structure XML: XML =
@@ -190,4 +214,137 @@
end;
+
+
+(** XML as data representation language **)
+
+exception XML_ATOM of string;
+exception XML_BODY of tree list;
+
+
+structure Encode =
+struct
+
+type 'a A = 'a -> string;
+type 'a T = 'a -> body;
+type 'a V = 'a -> string list * body;
+
+
+(* atomic values *)
+
+fun int_atom i = signed_string_of_int i;
+
+fun bool_atom false = "0"
+ | bool_atom true = "1";
+
+fun unit_atom () = "";
+
+
+(* structural nodes *)
+
+fun node ts = Elem ((":", []), ts);
+
+fun vector xs = map_index (fn (i, x) => (int_atom i, x)) xs;
+
+fun tagged (tag, (xs, ts)) = Elem ((int_atom tag, vector xs), ts);
+
+
+(* representation of standard types *)
+
+fun properties props = [Elem ((":", props), [])];
+
+fun string "" = []
+ | string s = [Text s];
+
+val int = string o int_atom;
+
+val bool = string o bool_atom;
+
+val unit = string o unit_atom;
+
+fun pair f g (x, y) = [node (f x), node (g y)];
+
+fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
+
+fun list f xs = map (node o f) xs;
+
+fun option _ NONE = []
+ | option f (SOME x) = [node (f x)];
+
+fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
+
end;
+
+
+structure Decode =
+struct
+
+type 'a A = string -> 'a;
+type 'a T = body -> 'a;
+type 'a V = string list * body -> 'a;
+
+
+(* atomic values *)
+
+fun int_atom s =
+ (case Int.fromString s of
+ SOME i => i
+ | NONE => raise XML_ATOM s);
+
+fun bool_atom "0" = false
+ | bool_atom "1" = true
+ | bool_atom s = raise XML_ATOM s;
+
+fun unit_atom "" = ()
+ | unit_atom s = raise XML_ATOM s;
+
+
+(* structural nodes *)
+
+fun node (Elem ((":", []), ts)) = ts
+ | node t = raise XML_BODY [t];
+
+fun vector atts =
+ fold_map (fn (a, x) => fn i => if int_atom a = i then (x, i + 1) else raise XML_ATOM a) atts;
+
+fun tagged (Elem ((name, atts), ts)) = (int_atom name, (#1 (vector atts 0), ts))
+ | tagged t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun properties [Elem ((":", props), [])] = props
+ | properties ts = raise XML_BODY ts;
+
+fun string [] = ""
+ | string [Text s] = s
+ | string ts = raise XML_BODY ts;
+
+val int = int_atom o string;
+
+val bool = bool_atom o string;
+
+val unit = unit_atom o string;
+
+fun pair f g [t1, t2] = (f (node t1), g (node t2))
+ | pair _ _ ts = raise XML_BODY ts;
+
+fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
+ | triple _ _ _ ts = raise XML_BODY ts;
+
+fun list f ts = map (f o node) ts;
+
+fun option _ [] = NONE
+ | option f [t] = SOME (f (node t))
+ | option _ ts = raise XML_BODY ts;
+
+fun variant fs [t] =
+ let
+ val (tag, (xs, ts)) = tagged t;
+ val f = nth fs tag handle General.Subscript => raise XML_BODY [t];
+ in f (xs, ts) end
+ | variant _ ts = raise XML_BODY ts;
+
+end;
+
+end;
--- a/src/Pure/General/xml.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/xml.scala Tue Jul 12 20:53:14 2011 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/General/xml.scala
Author: Makarius
-Simple XML tree values.
+Untyped XML trees.
*/
package isabelle
@@ -12,13 +12,16 @@
import javax.xml.parsers.DocumentBuilderFactory
import scala.actors.Actor._
+import scala.collection.mutable
object XML
{
+ /** XML trees **/
+
/* datatype representation */
- type Attributes = List[(String, String)]
+ type Attributes = Properties.T
sealed abstract class Tree { override def toString = string_of_tree(this) }
case class Elem(markup: Markup, body: List[Tree]) extends Tree
@@ -115,7 +118,7 @@
val z = trim_bytes(x)
if (z.length > max_string) z else store(z)
}
- def cache_props(x: List[(String, String)]): List[(String, String)] =
+ def cache_props(x: Properties.T): Properties.T =
if (x.isEmpty) x
else
lookup(x) match {
@@ -174,7 +177,8 @@
}
- /* document object model (W3C DOM) */
+
+ /** document object model (W3C DOM) **/
def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
node.getUserData(Markup.Data.name) match {
@@ -200,4 +204,184 @@
}
DOM(tree)
}
+
+
+
+ /** XML as data representation language **/
+
+ class XML_Atom(s: String) extends Exception(s)
+ class XML_Body(body: XML.Body) extends Exception
+
+ object Encode
+ {
+ type T[A] = A => XML.Body
+
+
+ /* atomic values */
+
+ def long_atom(i: Long): String = i.toString
+
+ def int_atom(i: Int): String = i.toString
+
+ def bool_atom(b: Boolean): String = if (b) "1" else "0"
+
+ def unit_atom(u: Unit) = ""
+
+
+ /* structural nodes */
+
+ private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
+
+ private def vector(xs: List[String]): XML.Attributes =
+ xs.zipWithIndex.map(p => (int_atom(p._2), p._1))
+
+ private def tagged(tag: Int, data: (List[String], XML.Body)): XML.Tree =
+ XML.Elem(Markup(int_atom(tag), vector(data._1)), data._2)
+
+
+ /* representation of standard types */
+
+ val properties: T[Properties.T] =
+ (props => List(XML.Elem(Markup(":", props), Nil)))
+
+ val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
+
+ val long: T[Long] = (x => string(long_atom(x)))
+
+ val int: T[Int] = (x => string(int_atom(x)))
+
+ val bool: T[Boolean] = (x => string(bool_atom(x)))
+
+ val unit: T[Unit] = (x => string(unit_atom(x)))
+
+ def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+ (x => List(node(f(x._1)), node(g(x._2))))
+
+ def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+ (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
+
+ def list[A](f: T[A]): T[List[A]] =
+ (xs => xs.map((x: A) => node(f(x))))
+
+ def option[A](f: T[A]): T[Option[A]] =
+ {
+ case None => Nil
+ case Some(x) => List(node(f(x)))
+ }
+
+ def variant[A](fs: List[PartialFunction[A, (List[String], XML.Body)]]): T[A] =
+ {
+ case x =>
+ val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
+ List(tagged(tag, f(x)))
+ }
+ }
+
+ object Decode
+ {
+ type T[A] = XML.Body => A
+ type V[A] = (List[String], XML.Body) => A
+
+
+ /* atomic values */
+
+ def long_atom(s: String): Long =
+ try { java.lang.Long.parseLong(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ def int_atom(s: String): Int =
+ try { Integer.parseInt(s) }
+ catch { case e: NumberFormatException => throw new XML_Atom(s) }
+
+ def bool_atom(s: String): Boolean =
+ if (s == "1") true
+ else if (s == "0") false
+ else throw new XML_Atom(s)
+
+ def unit_atom(s: String): Unit =
+ if (s == "") () else throw new XML_Atom(s)
+
+
+ /* structural nodes */
+
+ private def node(t: XML.Tree): XML.Body =
+ t match {
+ case XML.Elem(Markup(":", Nil), ts) => ts
+ case _ => throw new XML_Body(List(t))
+ }
+
+ private def vector(atts: XML.Attributes): List[String] =
+ {
+ val xs = new mutable.ListBuffer[String]
+ var i = 0
+ for ((a, x) <- atts) {
+ if (int_atom(a) == i) { xs += x; i = i + 1 }
+ else throw new XML_Atom(a)
+ }
+ xs.toList
+ }
+
+ private def tagged(t: XML.Tree): (Int, (List[String], XML.Body)) =
+ t match {
+ case XML.Elem(Markup(name, atts), ts) => (int_atom(name), (vector(atts), ts))
+ case _ => throw new XML_Body(List(t))
+ }
+
+
+ /* representation of standard types */
+
+ val properties: T[Properties.T] =
+ {
+ case List(XML.Elem(Markup(":", props), Nil)) => props
+ case ts => throw new XML_Body(ts)
+ }
+
+ val string: T[String] =
+ {
+ case Nil => ""
+ case List(XML.Text(s)) => s
+ case ts => throw new XML_Body(ts)
+ }
+
+ val long: T[Long] = (x => long_atom(string(x)))
+
+ val int: T[Int] = (x => int_atom(string(x)))
+
+ val bool: T[Boolean] = (x => bool_atom(string(x)))
+
+ val unit: T[Unit] = (x => unit_atom(string(x)))
+
+ def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
+ {
+ case List(t1, t2) => (f(node(t1)), g(node(t2)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
+ {
+ case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def list[A](f: T[A]): T[List[A]] =
+ (ts => ts.map(t => f(node(t))))
+
+ def option[A](f: T[A]): T[Option[A]] =
+ {
+ case Nil => None
+ case List(t) => Some(f(node(t)))
+ case ts => throw new XML_Body(ts)
+ }
+
+ def variant[A](fs: List[V[A]]): T[A] =
+ {
+ case List(t) =>
+ val (tag, (xs, ts)) = tagged(t)
+ val f =
+ try { fs(tag) }
+ catch { case _: IndexOutOfBoundsException => throw new XML_Body(List(t)) }
+ f(xs, ts)
+ case ts => throw new XML_Body(ts)
+ }
+ }
}
--- a/src/Pure/General/xml_data.ML Wed Jul 13 00:43:07 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,154 +0,0 @@
-(* Title: Pure/General/xml_data.ML
- Author: Makarius
-
-XML as basic data representation language.
-*)
-
-signature XML_DATA_OPS =
-sig
- type 'a T
- val properties: Properties.T T
- val string: string T
- val int: int T
- val bool: bool T
- val unit: unit T
- val pair: 'a T -> 'b T -> ('a * 'b) T
- val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
- val list: 'a T -> 'a list T
- val option: 'a T -> 'a option T
- val variant: 'a T list -> 'a T
-end;
-
-signature XML_DATA =
-sig
- structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
- exception XML_ATOM of string
- exception XML_BODY of XML.body
- structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
-end;
-
-structure XML_Data: XML_DATA =
-struct
-
-(** encode **)
-
-structure Encode =
-struct
-
-type 'a T = 'a -> XML.body;
-
-
-(* basic values *)
-
-fun int_atom i = signed_string_of_int i;
-
-fun bool_atom false = "0"
- | bool_atom true = "1";
-
-fun unit_atom () = "";
-
-
-(* structural nodes *)
-
-fun node ts = XML.Elem ((":", []), ts);
-
-fun tagged (tag, ts) = XML.Elem ((int_atom tag, []), ts);
-
-
-(* representation of standard types *)
-
-fun properties props = [XML.Elem ((":", props), [])];
-
-fun string "" = []
- | string s = [XML.Text s];
-
-val int = string o int_atom;
-
-val bool = string o bool_atom;
-
-val unit = string o unit_atom;
-
-fun pair f g (x, y) = [node (f x), node (g y)];
-
-fun triple f g h (x, y, z) = [node (f x), node (g y), node (h z)];
-
-fun list f xs = map (node o f) xs;
-
-fun option _ NONE = []
- | option f (SOME x) = [node (f x)];
-
-fun variant fs x = [tagged (the (get_index (fn f => try f x) fs))];
-
-end;
-
-
-
-(** decode **)
-
-exception XML_ATOM of string;
-exception XML_BODY of XML.tree list;
-
-structure Decode =
-struct
-
-type 'a T = XML.body -> 'a;
-
-
-(* basic values *)
-
-fun int_atom s =
- (case Int.fromString s of
- SOME i => i
- | NONE => raise XML_ATOM s);
-
-fun bool_atom "0" = false
- | bool_atom "1" = true
- | bool_atom s = raise XML_ATOM s;
-
-fun unit_atom "" = ()
- | unit_atom s = raise XML_ATOM s;
-
-
-(* structural nodes *)
-
-fun node (XML.Elem ((":", []), ts)) = ts
- | node t = raise XML_BODY [t];
-
-fun tagged (XML.Elem ((s, []), ts)) = (int_atom s, ts)
- | tagged t = raise XML_BODY [t];
-
-
-(* representation of standard types *)
-
-fun properties [XML.Elem ((":", props), [])] = props
- | properties ts = raise XML_BODY ts;
-
-fun string [] = ""
- | string [XML.Text s] = s
- | string ts = raise XML_BODY ts;
-
-val int = int_atom o string;
-
-val bool = bool_atom o string;
-
-val unit = unit_atom o string;
-
-fun pair f g [t1, t2] = (f (node t1), g (node t2))
- | pair _ _ ts = raise XML_BODY ts;
-
-fun triple f g h [t1, t2, t3] = (f (node t1), g (node t2), h (node t3))
- | triple _ _ _ ts = raise XML_BODY ts;
-
-fun list f ts = map (f o node) ts;
-
-fun option _ [] = NONE
- | option f [t] = SOME (f (node t))
- | option _ ts = raise XML_BODY ts;
-
-fun variant fs [t] = uncurry (nth fs) (tagged t)
- | variant _ ts = raise XML_BODY ts;
-
-end;
-
-end;
-
--- a/src/Pure/General/xml_data.scala Wed Jul 13 00:43:07 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,176 +0,0 @@
-/* Title: Pure/General/xml_data.scala
- Author: Makarius
-
-XML as basic data representation language.
-*/
-
-package isabelle
-
-
-
-object XML_Data
-{
- /** encode **/
-
- object Encode
- {
- type T[A] = A => XML.Body
-
-
- /* basic values */
-
- private def long_atom(i: Long): String = i.toString
-
- private def int_atom(i: Int): String = i.toString
-
- private def bool_atom(b: Boolean): String = if (b) "1" else "0"
-
- private def unit_atom(u: Unit) = ""
-
-
- /* structural nodes */
-
- private def node(ts: XML.Body): XML.Tree = XML.Elem(Markup(":", Nil), ts)
-
- private def tagged(tag: Int, ts: XML.Body): XML.Tree =
- XML.Elem(Markup(int_atom(tag), Nil), ts)
-
-
- /* representation of standard types */
-
- val properties: T[List[(String, String)]] =
- (props => List(XML.Elem(Markup(":", props), Nil)))
-
- val string: T[String] = (s => if (s.isEmpty) Nil else List(XML.Text(s)))
-
- val long: T[Long] = (x => string(long_atom(x)))
-
- val int: T[Int] = (x => string(int_atom(x)))
-
- val bool: T[Boolean] = (x => string(bool_atom(x)))
-
- val unit: T[Unit] = (x => string(unit_atom(x)))
-
- def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
- (x => List(node(f(x._1)), node(g(x._2))))
-
- def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
- (x => List(node(f(x._1)), node(g(x._2)), node(h(x._3))))
-
- def list[A](f: T[A]): T[List[A]] =
- (xs => xs.map((x: A) => node(f(x))))
-
- def option[A](f: T[A]): T[Option[A]] =
- {
- case None => Nil
- case Some(x) => List(node(f(x)))
- }
-
- def variant[A](fs: List[PartialFunction[A, XML.Body]]): T[A] =
- {
- case x =>
- val (f, tag) = fs.iterator.zipWithIndex.find(p => p._1.isDefinedAt(x)).get
- List(tagged(tag, f(x)))
- }
- }
-
-
-
- /** decode **/
-
- class XML_Atom(s: String) extends Exception(s)
- class XML_Body(body: XML.Body) extends Exception
-
- object Decode
- {
- type T[A] = XML.Body => A
-
-
- /* basic values */
-
- private def long_atom(s: String): Long =
- try { java.lang.Long.parseLong(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- private def int_atom(s: String): Int =
- try { Integer.parseInt(s) }
- catch { case e: NumberFormatException => throw new XML_Atom(s) }
-
- private def bool_atom(s: String): Boolean =
- if (s == "1") true
- else if (s == "0") false
- else throw new XML_Atom(s)
-
- private def unit_atom(s: String): Unit =
- if (s == "") () else throw new XML_Atom(s)
-
-
- /* structural nodes */
-
- private def node(t: XML.Tree): XML.Body =
- t match {
- case XML.Elem(Markup(":", Nil), ts) => ts
- case _ => throw new XML_Body(List(t))
- }
-
- private def tagged(t: XML.Tree): (Int, XML.Body) =
- t match {
- case XML.Elem(Markup(s, Nil), ts) => (int_atom(s), ts)
- case _ => throw new XML_Body(List(t))
- }
-
-
- /* representation of standard types */
-
- val properties: T[List[(String, String)]] =
- {
- case List(XML.Elem(Markup(":", props), Nil)) => props
- case ts => throw new XML_Body(ts)
- }
-
- val string: T[String] =
- {
- case Nil => ""
- case List(XML.Text(s)) => s
- case ts => throw new XML_Body(ts)
- }
-
- val long: T[Long] = (x => long_atom(string(x)))
-
- val int: T[Int] = (x => int_atom(string(x)))
-
- val bool: T[Boolean] = (x => bool_atom(string(x)))
-
- val unit: T[Unit] = (x => unit_atom(string(x)))
-
- def pair[A, B](f: T[A], g: T[B]): T[(A, B)] =
- {
- case List(t1, t2) => (f(node(t1)), g(node(t2)))
- case ts => throw new XML_Body(ts)
- }
-
- def triple[A, B, C](f: T[A], g: T[B], h: T[C]): T[(A, B, C)] =
- {
- case List(t1, t2, t3) => (f(node(t1)), g(node(t2)), h(node(t3)))
- case ts => throw new XML_Body(ts)
- }
-
- def list[A](f: T[A]): T[List[A]] =
- (ts => ts.map(t => f(node(t))))
-
- def option[A](f: T[A]): T[Option[A]] =
- {
- case Nil => None
- case List(t) => Some(f(node(t)))
- case ts => throw new XML_Body(ts)
- }
-
- def variant[A](fs: List[T[A]]): T[A] =
- {
- case List(t) =>
- val (tag, ts) = tagged(t)
- fs(tag)(ts)
- case ts => throw new XML_Body(ts)
- }
- }
-}
--- a/src/Pure/General/yxml.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/yxml.ML Tue Jul 12 20:53:14 2011 +0200
@@ -15,7 +15,9 @@
signature YXML =
sig
- val escape_controls: string -> string
+ val X: Symbol.symbol
+ val Y: Symbol.symbol
+ val embed_controls: string -> string
val detect: string -> bool
val output_markup: Markup.T -> string * string
val element: string -> XML.attributes -> string list -> string
@@ -37,7 +39,7 @@
then chr 192 ^ chr (128 + ord c)
else c;
-fun escape_controls str =
+fun embed_controls str =
if exists_string Symbol.is_ascii_control str
then translate_string pseudo_utf8 str
else str;
@@ -45,12 +47,12 @@
(* markers *)
-val X = Symbol.ENQ;
-val Y = Symbol.ACK;
+val X = chr 5;
+val Y = chr 6;
val XY = X ^ Y;
val XYX = XY ^ X;
-val detect = exists_string (fn s => s = X);
+val detect = exists_string (fn s => s = X orelse s = Y);
(* output *)
--- a/src/Pure/General/yxml.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/General/yxml.scala Tue Jul 12 20:53:14 2011 +0200
@@ -14,10 +14,12 @@
{
/* chunk markers */
- private val X = '\5'
- private val Y = '\6'
- private val X_string = X.toString
- private val Y_string = Y.toString
+ val X = '\5'
+ val Y = '\6'
+ val X_string = X.toString
+ val Y_string = Y.toString
+
+ def detect(s: String): Boolean = s.exists(c => c == X || c == Y)
/* string representation */ // FIXME byte array version with pseudo-utf-8 (!?)
--- a/src/Pure/IsaMakefile Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/IsaMakefile Tue Jul 12 20:53:14 2011 +0200
@@ -104,7 +104,6 @@
General/timing.ML \
General/url.ML \
General/xml.ML \
- General/xml_data.ML \
General/yxml.ML \
Isar/args.ML \
Isar/attrib.ML \
@@ -131,7 +130,6 @@
Isar/overloading.ML \
Isar/parse.ML \
Isar/parse_spec.ML \
- Isar/parse_value.ML \
Isar/proof.ML \
Isar/proof_context.ML \
Isar/proof_display.ML \
--- a/src/Pure/Isar/isar_syn.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/Isar/isar_syn.ML Tue Jul 12 20:53:14 2011 +0200
@@ -766,7 +766,7 @@
(* nested commands *)
val props_text =
- Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
+ Scan.optional Parse.properties [] -- Parse.position Parse.string
>> (fn (props, (str, pos)) =>
(Position.of_properties (Position.default_properties pos props), str));
--- a/src/Pure/Isar/outer_syntax.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/Isar/outer_syntax.scala Tue Jul 12 20:53:14 2011 +0200
@@ -11,6 +11,30 @@
import scala.collection.mutable
+object Outer_Syntax
+{
+ def quote_string(str: String): String =
+ {
+ val result = new StringBuilder(str.length + 10)
+ result += '"'
+ for (s <- Symbol.iterator(str)) {
+ if (s.length == 1) {
+ val c = s(0)
+ if (c < 32 && c != YXML.X && c != YXML.Y || c == '\\' || c == '"') {
+ result += '\\'
+ if (c < 10) result += '0'
+ if (c < 100) result += '0'
+ result ++= (c.asInstanceOf[Int].toString)
+ }
+ else result += c
+ }
+ else result ++= s
+ }
+ result += '"'
+ result.toString
+ }
+}
+
class Outer_Syntax
{
protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
--- a/src/Pure/Isar/parse.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/Isar/parse.ML Tue Jul 12 20:53:14 2011 +0200
@@ -60,6 +60,7 @@
val and_list1': 'a context_parser -> 'a list context_parser
val list: 'a parser -> 'a list parser
val list1: 'a parser -> 'a list parser
+ val properties: Properties.T parser
val name: bstring parser
val binding: binding parser
val xname: xstring parser
@@ -230,6 +231,8 @@
fun list1 scan = enum1 "," scan;
fun list scan = enum "," scan;
+val properties = $$$ "(" |-- !!! (list (string -- ($$$ "=" |-- string)) --| $$$ ")");
+
(* names and text *)
--- a/src/Pure/Isar/parse_value.ML Wed Jul 13 00:43:07 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-(* Title: Pure/Isar/parse_value.ML
- Author: Makarius
-
-Outer syntax parsers for basic ML values.
-*)
-
-signature PARSE_VALUE =
-sig
- val comma: 'a parser -> 'a parser
- val equal: 'a parser -> 'a parser
- val parens: 'a parser -> 'a parser
- val unit: unit parser
- val pair: 'a parser -> 'b parser -> ('a * 'b) parser
- val triple: 'a parser -> 'b parser -> 'c parser -> ('a * 'b * 'c) parser
- val list: 'a parser -> 'a list parser
- val properties: Properties.T parser
-end;
-
-structure Parse_Value: PARSE_VALUE =
-struct
-
-(* syntax utilities *)
-
-fun comma p = Parse.$$$ "," |-- Parse.!!! p;
-fun equal p = Parse.$$$ "=" |-- Parse.!!! p;
-fun parens p = Parse.$$$ "(" |-- Parse.!!! (p --| Parse.$$$ ")");
-
-
-(* tuples *)
-
-val unit = parens (Scan.succeed ());
-fun pair p1 p2 = parens (p1 -- comma p2);
-fun triple p1 p2 p3 = parens (p1 -- comma p2 -- comma p3) >> Parse.triple1;
-
-
-(* lists *)
-
-fun list p = parens (Parse.enum "," p);
-val properties = list (Parse.string -- equal Parse.string);
-
-end;
-
--- a/src/Pure/Isar/token.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/Isar/token.ML Tue Jul 12 20:53:14 2011 +0200
@@ -191,15 +191,12 @@
(* unparse *)
-fun escape q =
- implode o map (fn s => if s = q orelse s = "\\" then "\\" ^ s else s) o Symbol.explode;
-
fun unparse (Token (_, (kind, x), _)) =
(case kind of
- String => x |> quote o escape "\""
- | AltString => x |> enclose "`" "`" o escape "`"
- | Verbatim => x |> enclose "{*" "*}"
- | Comment => x |> enclose "(*" "*)"
+ String => Symbol_Pos.quote_string_qq x
+ | AltString => Symbol_Pos.quote_string_bq x
+ | Verbatim => enclose "{*" "*}" x
+ | Comment => enclose "(*" "*)" x
| Sync => ""
| EOF => ""
| _ => x);
--- a/src/Pure/PIDE/document.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/PIDE/document.scala Tue Jul 12 20:53:14 2011 +0200
@@ -16,12 +16,7 @@
/* formal identifiers */
type ID = Long
-
- object ID
- {
- def apply(id: ID): String = Markup.Long.apply(id)
- def unapply(s: String): Option[ID] = Markup.Long.unapply(s)
- }
+ val ID = Properties.Value.Long
type Version_ID = ID
type Command_ID = ID
--- a/src/Pure/PIDE/isar_document.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/PIDE/isar_document.ML Tue Jul 12 20:53:14 2011 +0200
@@ -18,10 +18,10 @@
val old_id = Document.parse_id old_id_string;
val new_id = Document.parse_id new_id_string;
val edits = YXML.parse_body edits_yxml |>
- let open XML_Data.Decode
+ let open XML.Decode
in list (pair string (option (list (pair (option int) (option int))))) end;
val headers = YXML.parse_body headers_yxml |>
- let open XML_Data.Decode
+ let open XML.Decode
in list (pair string (triple string (list string) (list string))) end;
val await_cancellation = Document.cancel_execution state;
--- a/src/Pure/PIDE/isar_document.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/PIDE/isar_document.scala Tue Jul 12 20:53:14 2011 +0200
@@ -143,12 +143,12 @@
edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
{
val arg1 =
- { import XML_Data.Encode._
+ { import XML.Encode._
list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
val arg2 =
- { import XML_Data.Encode._
- list(pair(string, Thy_Header.encode_xml_data))(headers) }
+ { import XML.Encode._
+ list(pair(string, Thy_Header.xml_encode))(headers) }
input("Isar_Document.edit_version",
Document.ID(old_id), Document.ID(new_id),
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jul 12 20:53:14 2011 +0200
@@ -22,7 +22,7 @@
val thm_depsN = "thm_deps"; (*meta-information about theorem deps*)
val test_markupN = "test_markup"; (*XML markup for everything*)
-fun special ch = Symbol.SOH ^ ch;
+fun special ch = chr 1 ^ ch;
(* render markup *)
--- a/src/Pure/ROOT.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/ROOT.ML Tue Jul 12 20:53:14 2011 +0200
@@ -53,7 +53,6 @@
use "General/linear_set.ML";
use "General/buffer.ML";
use "General/xml.ML";
-use "General/xml_data.ML";
use "General/pretty.ML";
use "General/path.ML";
use "General/url.ML";
@@ -189,7 +188,6 @@
use "Isar/token.ML";
use "Isar/keyword.ML";
use "Isar/parse.ML";
-use "Isar/parse_value.ML";
use "Isar/args.ML";
(*ML support*)
--- a/src/Pure/System/isabelle_process.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/System/isabelle_process.ML Tue Jul 12 20:53:14 2011 +0200
@@ -66,17 +66,18 @@
fun chunk s = [string_of_int (size s), "\n", s];
-fun message _ _ _ "" = ()
- | message mbox ch raw_props body =
- let
- val robust_props = map (pairself YXML.escape_controls) raw_props;
- val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
- in Mailbox.send mbox (chunk header @ chunk body) end;
+fun message mbox ch raw_props body =
+ let
+ val robust_props = map (pairself YXML.embed_controls) raw_props;
+ val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
+ in Mailbox.send mbox (chunk header @ chunk body) end;
fun standard_message mbox with_serial ch body =
- message mbox ch
- ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
- (Position.properties_of (Position.thread_data ()))) body;
+ if body = "" then ()
+ else
+ message mbox ch
+ ((if with_serial then cons (Markup.serialN, serial_string ()) else I)
+ (Position.properties_of (Position.thread_data ()))) body;
fun message_output mbox out_stream =
let
--- a/src/Pure/System/isabelle_process.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/System/isabelle_process.scala Tue Jul 12 20:53:14 2011 +0200
@@ -46,7 +46,7 @@
class Result(val message: XML.Elem) extends Message
{
def kind: String = message.markup.name
- def properties: XML.Attributes = message.markup.properties
+ def properties: Properties.T = message.markup.properties
def body: XML.Body = message.body
def is_init = kind == Markup.INIT
@@ -95,7 +95,7 @@
private val xml_cache = new XML.Cache()
- private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
+ private def put_result(kind: String, props: Properties.T, body: XML.Body)
{
if (kind == Markup.INIT) rm_fifos()
if (kind == Markup.RAW)
--- a/src/Pure/System/isabelle_syntax.scala Wed Jul 13 00:43:07 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,74 +0,0 @@
-/* Title: Pure/System/isabelle_syntax.scala
- Author: Makarius
-
-Isabelle outer syntax.
-*/
-
-package isabelle
-
-
-object Isabelle_Syntax
-{
- /* string token */
-
- def append_string(str: String, result: StringBuilder)
- {
- result.append("\"")
- for (c <- str) {
- if (c < 32 || c == '\\' || c == '\"') {
- result.append("\\")
- if (c < 10) result.append('0')
- if (c < 100) result.append('0')
- result.append(c.asInstanceOf[Int].toString)
- }
- else result.append(c)
- }
- result.append("\"")
- }
-
- def encode_string(str: String) =
- {
- val result = new StringBuilder(str.length + 10)
- append_string(str, result)
- result.toString
- }
-
-
- /* list */
-
- def append_list[A](append_elem: (A, StringBuilder) => Unit, body: Iterable[A],
- result: StringBuilder)
- {
- result.append("(")
- val elems = body.iterator
- if (elems.hasNext) append_elem(elems.next, result)
- while (elems.hasNext) {
- result.append(", ")
- append_elem(elems.next, result)
- }
- result.append(")")
- }
-
- def encode_list[A](append_elem: (A, StringBuilder) => Unit, elems: Iterable[A]) =
- {
- val result = new StringBuilder
- append_list(append_elem, elems, result)
- result.toString
- }
-
-
- /* properties */
-
- def append_properties(props: List[(String, String)], result: StringBuilder)
- {
- append_list((p: (String, String), res) =>
- { append_string(p._1, res); res.append(" = "); append_string(p._2, res) }, props, result)
- }
-
- def encode_properties(props: List[(String, String)]) =
- {
- val result = new StringBuilder
- append_properties(props, result)
- result.toString
- }
-}
--- a/src/Pure/Thy/thy_header.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/Thy/thy_header.scala Tue Jul 12 20:53:14 2011 +0200
@@ -31,10 +31,10 @@
Header(f(name), imports.map(f), uses.map(f))
}
- val encode_xml_data: XML_Data.Encode.T[Header] =
+ val xml_encode: XML.Encode.T[Header] =
{
case Header(name, imports, uses) =>
- import XML_Data.Encode._
+ import XML.Encode._
triple(string, list(string), list(string))(name, imports, uses)
}
--- a/src/Pure/Tools/find_theorems.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/Tools/find_theorems.ML Tue Jul 12 20:53:14 2011 +0200
@@ -139,8 +139,8 @@
|> (if rem_dups then cons ("rem_dups", "") else I)
|> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
in
- XML.Elem (("Query", properties), XML_Data.Encode.list
- (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
+ XML.Elem (("Query", properties), XML.Encode.list
+ (XML.Encode.pair XML.Encode.bool (single o xml_of_criterion)) criteria)
end
| xml_of_query _ = raise Fail "cannot serialize goal";
@@ -149,7 +149,7 @@
val rem_dups = Properties.defined properties "rem_dups";
val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
val criteria =
- XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
+ XML.Decode.list (XML.Decode.pair XML.Decode.bool
(criterion_of_xml o the_single)) body;
in
{goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
@@ -190,12 +190,12 @@
val properties =
if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
in
- XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
+ XML.Elem (("Result", properties), XML.Encode.list (single o xml_of_theorem) theorems)
end;
fun result_of_xml (XML.Elem (("Result", properties), body)) =
(Properties.get properties "found" |> Option.map Markup.parse_int,
- XML_Data.Decode.list (theorem_of_xml o the_single) body)
+ XML.Decode.list (theorem_of_xml o the_single) body)
| result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
--- a/src/Pure/build-jars Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/build-jars Tue Jul 12 20:53:14 2011 +0200
@@ -20,11 +20,11 @@
General/path.scala
General/position.scala
General/pretty.scala
+ General/properties.scala
General/scan.scala
General/sha1.scala
General/symbol.scala
General/xml.scala
- General/xml_data.scala
General/yxml.scala
Isar/keyword.scala
Isar/outer_syntax.scala
@@ -43,7 +43,6 @@
System/invoke_scala.scala
System/isabelle_charset.scala
System/isabelle_process.scala
- System/isabelle_syntax.scala
System/isabelle_system.scala
System/platform.scala
System/session.scala
@@ -59,6 +58,7 @@
library.scala
package.scala
term.scala
+ term_xml.scala
)
--- a/src/Pure/more_thm.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/more_thm.ML Tue Jul 12 20:53:14 2011 +0200
@@ -76,9 +76,9 @@
val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
val no_attributes: 'a -> 'a * 'b list
val simple_fact: 'a -> ('a * 'b list) list
- val tag_rule: Properties.property -> thm -> thm
+ val tag_rule: Properties.entry -> thm -> thm
val untag_rule: string -> thm -> thm
- val tag: Properties.property -> attribute
+ val tag: Properties.entry -> attribute
val untag: string -> attribute
val def_name: string -> string
val def_name_optional: string -> string -> string
--- a/src/Pure/pure_setup.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/pure_setup.ML Tue Jul 12 20:53:14 2011 +0200
@@ -18,6 +18,7 @@
(* ML toplevel pretty printing *)
+toplevel_pp ["XML", "tree"] "Pretty.str o XML.string_of";
toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"<pretty>\")";
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
--- a/src/Pure/term.scala Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/term.scala Tue Jul 12 20:53:14 2011 +0200
@@ -1,7 +1,7 @@
/* Title: Pure/term.scala
Author: Makarius
-Lambda terms with XML data representation.
+Lambda terms, types, sorts.
Note: Isabelle/ML is the primary environment for logical operations.
*/
@@ -11,8 +11,6 @@
object Term
{
- /* basic type definitions */
-
type Indexname = (String, Int)
type Sort = List[String]
@@ -33,59 +31,3 @@
case class App(fun: Term, arg: Term) extends Term
}
-
-object Term_XML
-{
- import Term._
-
-
- /* XML data representation */
-
- object Encode
- {
- import XML_Data.Encode._
-
- val indexname: T[Indexname] = pair(string, int)
-
- val sort: T[Sort] = list(string)
-
- def typ: T[Typ] =
- variant[Typ](List(
- { case Type(a, b) => pair(string, list(typ))((a, b)) },
- { case TFree(a, b) => pair(string, sort)((a, b)) },
- { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
-
- def term: T[Term] =
- variant[Term](List(
- { case Const(a, b) => pair(string, typ)((a, b)) },
- { case Free(a, b) => pair(string, typ)((a, b)) },
- { case Var(a, b) => pair(indexname, typ)((a, b)) },
- { case Bound(a) => int(a) },
- { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
- { case App(a, b) => pair(term, term)((a, b)) }))
- }
-
- object Decode
- {
- import XML_Data.Decode._
-
- val indexname: T[Indexname] = pair(string, int)
-
- val sort: T[Sort] = list(string)
-
- def typ: T[Typ] =
- variant[Typ](List(
- (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
- (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
- (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
-
- def term: T[Term] =
- variant[Term](List(
- (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
- (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
- (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
- (x => Bound(int(x))),
- (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
- (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
- }
-}
--- a/src/Pure/term_xml.ML Wed Jul 13 00:43:07 2011 +0900
+++ b/src/Pure/term_xml.ML Tue Jul 12 20:53:14 2011 +0200
@@ -7,7 +7,6 @@
signature TERM_XML_OPS =
sig
type 'a T
- val indexname: indexname T
val sort: sort T
val typ: typ T
val term: term T
@@ -15,63 +14,54 @@
signature TERM_XML =
sig
- structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
- structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
+ structure Encode: TERM_XML_OPS
+ structure Decode: TERM_XML_OPS
end;
structure Term_XML: TERM_XML =
struct
-(* encode *)
-
structure Encode =
struct
-open XML_Data.Encode;
-
-val indexname = pair string int;
+open XML.Encode;
val sort = list string;
fun typ T = T |> variant
- [fn Type x => pair string (list typ) x,
- fn TFree x => pair string sort x,
- fn TVar x => pair indexname sort x];
+ [fn Type (a, b) => ([a], (list typ) b),
+ fn TFree (a, b) => ([a], sort b),
+ fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
fun term t = t |> variant
- [fn Const x => pair string typ x,
- fn Free x => pair string typ x,
- fn Var x => pair indexname typ x,
- fn Bound x => int x,
- fn Abs x => triple string typ term x,
- fn op $ x => pair term term x];
+ [fn Const (a, b) => ([a], typ b),
+ fn Free (a, b) => ([a], typ b),
+ fn Var ((a, b), c) => ([a, int_atom b], typ c),
+ fn Bound a => ([int_atom a], []),
+ fn Abs (a, b, c) => ([a], pair typ term (b, c)),
+ fn a $ b => ([], pair term term (a, b))];
end;
-
-(* decode *)
-
structure Decode =
struct
-open XML_Data.Decode;
-
-val indexname = pair string int;
+open XML.Decode;
val sort = list string;
fun typ T = T |> variant
- [Type o pair string (list typ),
- TFree o pair string sort,
- TVar o pair indexname sort];
+ [fn ([a], b) => Type (a, list typ b),
+ fn ([a], b) => TFree (a, sort b),
+ fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
fun term t = t |> variant
- [Const o pair string typ,
- Free o pair string typ,
- Var o pair indexname typ,
- Bound o int,
- Abs o triple string typ term,
- op $ o pair term term];
+ [fn ([a], b) => Const (a, typ b),
+ fn ([a], b) => Free (a, typ b),
+ fn ([a, b], c) => Var ((a, int_atom b), typ c),
+ fn ([a], []) => Bound (int_atom a),
+ fn ([a], b) => let val (c, d) = pair typ term b in Abs (a, c, d) end,
+ fn ([], a) => op $ (pair term term a)];
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/term_xml.scala Tue Jul 12 20:53:14 2011 +0200
@@ -0,0 +1,57 @@
+/* Title: Pure/term_xml.scala
+ Author: Makarius
+
+XML data representation of lambda terms.
+*/
+
+package isabelle
+
+
+object Term_XML
+{
+ import Term._
+
+ object Encode
+ {
+ import XML.Encode._
+
+ val sort: T[Sort] = list(string)
+
+ def typ: T[Typ] =
+ variant[Typ](List(
+ { case Type(a, b) => (List(a), list(typ)(b)) },
+ { case TFree(a, b) => (List(a), sort(b)) },
+ { case TVar((a, b), c) => (List(a, int_atom(b)), sort(c)) }))
+
+ def term: T[Term] =
+ variant[Term](List(
+ { case Const(a, b) => (List(a), typ(b)) },
+ { case Free(a, b) => (List(a), typ(b)) },
+ { case Var((a, b), c) => (List(a, int_atom(b)), typ(c)) },
+ { case Bound(a) => (List(int_atom(a)), Nil) },
+ { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
+ { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
+ }
+
+ object Decode
+ {
+ import XML.Decode._
+
+ val sort: T[Sort] = list(string)
+
+ def typ: T[Typ] =
+ variant[Typ](List(
+ { case (List(a), b) => Type(a, list(typ)(b)) },
+ { case (List(a), b) => TFree(a, sort(b)) },
+ { case (List(a, b), c) => TVar((a, int_atom(b)), sort(c)) }))
+
+ def term: T[Term] =
+ variant[Term](List(
+ { case (List(a), b) => Const(a, typ(b)) },
+ { case (List(a), b) => Free(a, typ(b)) },
+ { case (List(a, b), c) => Var((a, int_atom(b)), typ(c)) },
+ { case (List(a), Nil) => Bound(int_atom(a)) },
+ { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
+ { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
+ }
+}