simplified signature (NB: interpretation of properties is mainly done via XML.Encode/Decode);
--- 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;
--- 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);