merged

--- a/src/Pure/General/properties.ML	Wed Mar 07 21:38:29 2012 +0100
+++ b/src/Pure/General/properties.ML	Wed Mar 07 23:21:00 2012 +0100
@@ -6,30 +6,21 @@
 
 signature PROPERTIES =
 sig
-  type entry = string * string
-  type T = entry list
+  type T = (string * string) list
   val defined: T -> string -> bool
   val get: T -> string -> string option
-  val get_int: T -> string -> int option
-  val put: entry -> T -> T
-  val put_int: string * int -> T -> T
+  val put: string * string -> T -> T
   val remove: string -> T -> T
 end;
 
 structure Properties: PROPERTIES =
 struct
 
-type entry = string * string;
-type T = entry list;
+type T = (string * string) 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 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;

--- a/src/Pure/PIDE/yxml.ML	Wed Mar 07 21:38:29 2012 +0100
+++ b/src/Pure/PIDE/yxml.ML	Wed Mar 07 23:21:00 2012 +0100
@@ -21,7 +21,6 @@
   val embed_controls: string -> string
   val detect: string -> bool
   val output_markup: Markup.T -> string * string
-  val element: string -> XML.attributes -> string list -> string
   val string_of_body: XML.body -> string
   val string_of: XML.tree -> string
   val parse_body: string -> XML.body
@@ -62,15 +61,9 @@
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
 
-fun element name atts body =
-  let val (pre, post) = output_markup (name, atts)
-  in pre ^ implode body ^ post end;
-
 fun string_of_body body =
   let
-    fun attrib (a, x) =
-      Buffer.add Y #>
-      Buffer.add a #> Buffer.add "=" #> Buffer.add x;
+    fun attrib (a, x) = Buffer.add Y #> Buffer.add a #> Buffer.add "=" #> Buffer.add x;
     fun tree (XML.Elem ((name, atts), ts)) =
           Buffer.add XY #> Buffer.add name #> fold attrib atts #> Buffer.add X #>
           trees ts #>
@@ -99,7 +92,7 @@
 
 (* structural errors *)
 
-fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
+fun err msg = raise Fail ("Malformed YXML: " ^ msg);
 fun err_attribute () = err "bad attribute";
 fun err_element () = err "bad element";
 fun err_unbalanced "" = err "unbalanced element"

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 07 21:38:29 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 07 23:21:00 2012 +0100
@@ -104,6 +104,9 @@
  [Isabelle_Markup.tfreeN, Isabelle_Markup.tvarN, Isabelle_Markup.freeN,
   Isabelle_Markup.boundN, Isabelle_Markup.varN, Isabelle_Markup.skolemN];
 
+fun get_int props name =
+  (case Properties.get props name of NONE => NONE | SOME s => Int.fromString s);
+
 in
 
 fun pgml_terms (XML.Elem ((name, atts), body)) =
@@ -114,9 +117,9 @@
         let val content = maps pgml_terms body in
           if name = Isabelle_Markup.blockN then
             [Pgml.Box {orient = NONE,
-              indent = Properties.get_int atts Isabelle_Markup.indentN, content = content}]
+              indent = get_int atts Isabelle_Markup.indentN, content = content}]
           else if name = Isabelle_Markup.breakN then
-            [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Isabelle_Markup.widthN}]
+            [Pgml.Break {mandatory = NONE, indent = get_int atts Isabelle_Markup.widthN}]
           else content
         end
   | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);

--- a/src/Pure/more_thm.ML	Wed Mar 07 21:38:29 2012 +0100
+++ b/src/Pure/more_thm.ML	Wed Mar 07 23:21:00 2012 +0100
@@ -79,9 +79,9 @@
   val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
-  val tag_rule: Properties.entry -> thm -> thm
+  val tag_rule: string * string -> thm -> thm
   val untag_rule: string -> thm -> thm
-  val tag: Properties.entry -> attribute
+  val tag: string * string -> attribute
   val untag: string -> attribute
   val def_name: string -> string
   val def_name_optional: string -> string -> string