# HG changeset patch
# User wenzelm
# Date 1331145172 -3600
# Node ID 9770573e2172018681434cefdbfb0bdd8a0fb496
# Parent  b1d15637381aedea9aaca58a40756735240b3b7f
simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode);

diff -r b1d15637381a -r 9770573e2172 src/Pure/General/properties.ML
--- a/src/Pure/General/properties.ML	Wed Mar 07 16:13:49 2012 +0100
+++ b/src/Pure/General/properties.ML	Wed Mar 07 19:32:52 2012 +0100
@@ -10,9 +10,7 @@
   type T = entry 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 remove: string -> T -> T
 end;
 
@@ -23,13 +21,8 @@
 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 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;
diff -r b1d15637381a -r 9770573e2172 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 07 16:13:49 2012 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Mar 07 19:32:52 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);