# 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);