# HG changeset patch # User wenzelm # Date 1331158860 -3600 # Node ID be56a254d880ea708677f5990a258a7a676b390a # Parent a5fa1dc5594534d547d57494571c963fcb4a4692# Parent 050e344825c83a5b800057356479dedbc2465c5d merged diff -r a5fa1dc55945 -r be56a254d880 src/Pure/General/properties.ML --- 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; diff -r a5fa1dc55945 -r be56a254d880 src/Pure/PIDE/yxml.ML --- 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" diff -r a5fa1dc55945 -r be56a254d880 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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); diff -r a5fa1dc55945 -r be56a254d880 src/Pure/more_thm.ML --- 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