# HG changeset patch
# User wenzelm
# Date 1219830534 -7200
# Node ID 4919bd124a58b9c2370a3dac1ca36c8bb4809880
# Parent  b46f48256dab0431605b0166baf5ef4abfc251fa
type Properties.T;

diff -r b46f48256dab -r 4919bd124a58 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Aug 27 11:24:35 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Aug 27 11:48:54 2008 +0200
@@ -317,7 +317,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  @{ML "Sign.declare_const: Markup.property list -> bstring * typ * mixfix
+  @{ML "Sign.declare_const: Properties.T -> bstring * typ * mixfix
   -> theory -> term * theory"} \\
   @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
   \end{mldecls}
diff -r b46f48256dab -r 4919bd124a58 doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Aug 27 11:24:35 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Aug 27 11:48:54 2008 +0200
@@ -326,9 +326,9 @@
   @{index_ML fastype_of: "term -> typ"} \\
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
-  @{index_ML Sign.declare_const: "Markup.property list -> bstring * typ * mixfix ->
+  @{index_ML Sign.declare_const: "Properties.T -> bstring * typ * mixfix ->
   theory -> term * theory"} \\
-  @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term ->
+  @{index_ML Sign.add_abbrev: "string -> Properties.T -> bstring * term ->
   theory -> (term * term) * theory"} \\
   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
diff -r b46f48256dab -r 4919bd124a58 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/General/markup.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -7,8 +7,7 @@
 
 signature MARKUP =
 sig
-  type property = string * string
-  type T = string * property list
+  type T = string * Properties.T
   val get_string: T -> string -> string option
   val get_int: T -> string -> int option
   val none: T
@@ -21,7 +20,7 @@
   val idN: string
   val kindN: string
   val internalK: string
-  val property_internal: property
+  val property_internal: Properties.property
   val lineN: string
   val columnN: string
   val offsetN: string
@@ -116,8 +115,7 @@
 
 (* basic markup *)
 
-type property = string * string;
-type T = string * property list;
+type T = string * Properties.T;
 
 val none = ("", []);
 
@@ -126,9 +124,9 @@
 
 
 fun properties more_props ((elem, props): T) =
-  (elem, fold_rev (AList.update (op =)) more_props props);
+  (elem, fold_rev Properties.put more_props props);
 
-fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
+fun get_string (_, props) = Properties.get props;
 fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
 
 fun markup_elem elem = (elem, (elem, []): T);
diff -r b46f48256dab -r 4919bd124a58 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/General/position.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -21,9 +21,9 @@
   val line_file: int -> string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
-  val of_properties: Markup.property list -> T
-  val properties_of: T -> Markup.property list
-  val default_properties: T -> Markup.property list -> Markup.property list
+  val of_properties: Properties.T -> T
+  val properties_of: T -> Properties.T
+  val default_properties: T -> Properties.T -> Properties.T
   val report: Markup.T -> T -> unit
   val str_of: T -> string
   type range = T * T
@@ -41,7 +41,7 @@
 
 (* datatype position *)
 
-datatype T = Pos of (int * int * int) * Markup.property list;
+datatype T = Pos of (int * int * int) * Properties.T;
 
 fun valid (i: int) = i > 0;
 fun if_valid i i' = if valid i then i' else i;
@@ -55,7 +55,7 @@
 fun column_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
 fun offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
 
-fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
+fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
 
 
 (* advance *)
@@ -97,13 +97,13 @@
 
 (* markup properties *)
 
-fun get_id (Pos (_, props)) = AList.lookup (op =) props Markup.idN;
-fun put_id id (Pos (count, props)) = Pos (count, AList.update (op =) (Markup.idN, id) props);
+fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
+fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
 
 fun of_properties props =
   let
     fun get name =
-      (case AList.lookup (op =) props name of
+      (case Properties.get props name of
         NONE => 0
       | SOME s => the_default 0 (Int.fromString s));
     val count = (get Markup.lineN, get Markup.columnN, get Markup.offsetN);
@@ -145,12 +145,12 @@
 val no_range = (none, none);
 
 fun encode_range (Pos (count, props), Pos ((i, j, k), _)) =
-  let val props' = props |> fold_rev (AList.update op =)
+  let val props' = props |> fold_rev Properties.put
     (value Markup.end_lineN i @ value Markup.end_columnN j @ value Markup.end_offsetN k)
   in Pos (count, props') end;
 
 fun reset_range (Pos (count, props)) =
-  let val props' = props |> fold (AList.delete op =)
+  let val props' = props |> fold Properties.remove
     [Markup.end_lineN, Markup.end_columnN, Markup.end_offsetN]
   in Pos (count, props') end;
 
diff -r b46f48256dab -r 4919bd124a58 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/General/xml.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -7,7 +7,7 @@
 
 signature XML =
 sig
-  type attributes = Markup.property list
+  type attributes = Properties.T
   datatype tree =
       Elem of string * attributes * tree list
     | Text of string
@@ -32,7 +32,7 @@
 
 (** XML trees **)
 
-type attributes = Markup.property list;
+type attributes = Properties.T;
 
 datatype tree =
     Elem of string * attributes * tree list
diff -r b46f48256dab -r 4919bd124a58 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/Isar/class.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -14,9 +14,9 @@
     -> theory -> string * Proof.context
 
   val init: class -> theory -> Proof.context
-  val declare: class -> Markup.property list
+  val declare: class -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
-  val abbrev: class -> Syntax.mode -> Markup.property list
+  val abbrev: class -> Syntax.mode -> Properties.T
     -> (string * mixfix) * term -> theory -> theory
   val note: class -> string
     -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
diff -r b46f48256dab -r 4919bd124a58 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/Isar/local_theory.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -11,8 +11,8 @@
 sig
   type operations
   val group_of: local_theory -> string
-  val group_properties_of: local_theory -> Markup.property list
-  val group_position_of: local_theory -> Markup.property list
+  val group_properties_of: local_theory -> Properties.T
+  val group_position_of: local_theory -> Properties.T
   val set_group: string -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
diff -r b46f48256dab -r 4919bd124a58 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -60,7 +60,7 @@
     'a * token list -> 'b list * ('a * token list)
   val list: (token list -> 'a * token list) -> token list -> 'a list * token list
   val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
-  val properties: token list -> Markup.property list * token list
+  val properties: token list -> Properties.T * token list
   val name: token list -> bstring * token list
   val xname: token list -> xstring * token list
   val text: token list -> string * token list
diff -r b46f48256dab -r 4919bd124a58 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -131,7 +131,7 @@
   val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     Context.generic -> Context.generic
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
-  val add_abbrev: string -> Markup.property list ->
+  val add_abbrev: string -> Properties.T ->
     bstring * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val verbose: bool ref
@@ -145,9 +145,9 @@
   val prems_limit: int ref
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
-  val query_type: Proof.context -> string -> Markup.property list
-  val query_const: Proof.context -> string -> Markup.property list
-  val query_class: Proof.context -> string -> Markup.property list
+  val query_type: Proof.context -> string -> Properties.T
+  val query_const: Proof.context -> string -> Properties.T
+  val query_class: Proof.context -> string -> Properties.T
 end;
 
 structure ProofContext: PROOF_CONTEXT =
diff -r b46f48256dab -r 4919bd124a58 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -112,9 +112,9 @@
 
 (** XML utils **)
 
-fun has_attr (attr : string) attrs = AList.defined (op =) attrs attr
+fun has_attr attr attrs = Properties.defined attrs attr
 
-fun get_attr_opt (attr : string) attrs = AList.lookup (op =) attrs attr
+fun get_attr_opt attr attrs = Properties.get attrs attr
 
 fun get_attr attr attrs =
     (case get_attr_opt attr attrs of
diff -r b46f48256dab -r 4919bd124a58 src/Pure/Tools/xml_syntax.ML
--- a/src/Pure/Tools/xml_syntax.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/Tools/xml_syntax.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -102,11 +102,11 @@
   NONE => raise XML (s ^ ": bad index", tree) | SOME i => i);
 
 fun type_of_xml (tree as XML.Elem ("TVar", atts, classes)) = TVar
-      ((case AList.lookup op = atts "name" of
+      ((case Properties.get atts "name" of
           NONE => raise XML ("type_of_xml: name of TVar missing", tree)
         | SOME name => name,
         the_default 0 (Option.map (index_of_string "type_of_xml" tree)
-          (AList.lookup op = atts "index"))),
+          (Properties.get atts "index"))),
        map class_of_xml classes)
   | type_of_xml (XML.Elem ("TFree", [("name", s)], classes)) =
       TFree (s, map class_of_xml classes)
@@ -119,11 +119,11 @@
   | term_of_xml (XML.Elem ("Free", [("name", s)], [typ])) =
       Free (s, type_of_xml typ)
   | term_of_xml (tree as XML.Elem ("Var", atts, [typ])) = Var
-      ((case AList.lookup op = atts "name" of
+      ((case Properties.get atts "name" of
           NONE => raise XML ("type_of_xml: name of Var missing", tree)
         | SOME name => name,
         the_default 0 (Option.map (index_of_string "term_of_xml" tree)
-          (AList.lookup op = atts "index"))),
+          (Properties.get atts "index"))),
        type_of_xml typ)
   | term_of_xml (XML.Elem ("Const", [("name", s)], [typ])) =
       Const (s, type_of_xml typ)
diff -r b46f48256dab -r 4919bd124a58 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/consts.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -17,7 +17,7 @@
   val the_type: T -> string -> typ                             (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
-  val the_tags: T -> string -> Markup.property list            (*exception TYPE*)
+  val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
   val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   val the_constraint: T -> string -> typ                       (*exception TYPE*)
   val space_of: T -> NameSpace.T
@@ -30,9 +30,9 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> NameSpace.naming -> Markup.property list -> (bstring * typ) -> T -> T
+  val declare: bool -> NameSpace.naming -> Properties.T -> (bstring * typ) -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Markup.property list ->
+  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
     bstring * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
@@ -47,7 +47,7 @@
 
 (* datatype T *)
 
-type decl = {T: typ, typargs: int list list, tags: Markup.property list, authentic: bool};
+type decl = {T: typ, typargs: int list list, tags: Properties.T, authentic: bool};
 type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
 
 datatype T = Consts of
diff -r b46f48256dab -r 4919bd124a58 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/more_thm.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -46,9 +46,9 @@
   val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
-  val tag_rule: Markup.property -> thm -> thm
+  val tag_rule: Properties.property -> thm -> thm
   val untag_rule: string -> thm -> thm
-  val tag: Markup.property -> attribute
+  val tag: Properties.property -> attribute
   val untag: string -> attribute
   val position_of: thm -> Position.T
   val default_position: Position.T -> thm -> thm
@@ -71,7 +71,7 @@
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
   val kind_internal: attribute
-  val has_internal: Markup.property list -> bool
+  val has_internal: Properties.property list -> bool
   val is_internal: thm -> bool
 end;
 
@@ -337,10 +337,9 @@
 
 (* theorem groups *)
 
-fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN;
+fun get_group thm = Properties.get (Thm.get_tags thm) Markup.groupN;
 
-fun put_group name =
-  if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name));
+fun put_group name = if name = "" then I else Thm.map_tags (Properties.put (Markup.groupN, name));
 
 fun group name = rule_attribute (K (put_group name));
 
@@ -355,7 +354,7 @@
 val corollaryK = "corollary";
 val internalK = Markup.internalK;
 
-fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN);
+fun the_kind thm = the (Properties.get (Thm.get_tags thm) Markup.kindN);
 
 val has_kind = can the_kind;
 val get_kind = the_default "" o try the_kind;
diff -r b46f48256dab -r 4919bd124a58 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/sign.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -93,9 +93,8 @@
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
-  val declare_const: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
-  val add_abbrev: string -> Markup.property list ->
-    bstring * term -> theory -> (term * term) * theory
+  val declare_const: Properties.T -> bstring * typ * mixfix -> theory -> term * theory
+  val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory
   val revert_abbrev: string -> string -> theory -> theory
   val add_const_constraint: string * typ option -> theory -> theory
   val primitive_class: string * class list -> theory -> theory
@@ -515,7 +514,7 @@
         val T' = Logic.varifyT T;
       in ((c, T'), (c', T', mx), Const (full_c, T)) end;
     val args = map prep raw_args;
-    val tags' = tags |> AList.update (op =) (Markup.theory_nameN, Context.theory_name thy);
+    val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
   in
     thy
     |> map_consts (fold (Consts.declare authentic (naming_of thy) tags' o #1) args)
diff -r b46f48256dab -r 4919bd124a58 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/theory.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -38,7 +38,7 @@
   val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
-  val specify_const: Markup.property list -> bstring * typ * mixfix -> (string * typ) list ->
+  val specify_const: Properties.T -> bstring * typ * mixfix -> (string * typ) list ->
    theory -> term * theory
   val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
 end
diff -r b46f48256dab -r 4919bd124a58 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/thm.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -42,7 +42,7 @@
   val rep_thm: thm ->
    {thy_ref: theory_ref,
     der: bool * Proofterm.proof,
-    tags: Markup.property list,
+    tags: Properties.T,
     maxidx: int,
     shyps: sort list,
     hyps: term list,
@@ -51,7 +51,7 @@
   val crep_thm: thm ->
    {thy_ref: theory_ref,
     der: bool * Proofterm.proof,
-    tags: Markup.property list,
+    tags: Properties.T,
     maxidx: int,
     shyps: sort list,
     hyps: cterm list,
@@ -138,8 +138,8 @@
   val full_prop_of: thm -> term
   val get_name: thm -> string
   val put_name: string -> thm -> thm
-  val get_tags: thm -> Markup.property list
-  val map_tags: (Markup.property list -> Markup.property list) -> thm -> thm
+  val get_tags: thm -> Properties.T
+  val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   val norm_proof: thm -> thm
   val adjust_maxidx_thm: int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
@@ -338,7 +338,7 @@
 abstype thm = Thm of
  {thy_ref: theory_ref,         (*dynamic reference to theory*)
   der: bool * Pt.proof,        (*derivation*)
-  tags: Markup.property list,  (*additional annotations/comments*)
+  tags: Properties.T,          (*additional annotations/comments*)
   maxidx: int,                 (*maximum index of any Var or TVar*)
   shyps: sort list,            (*sort hypotheses as ordered list*)
   hyps: term list,             (*hypotheses as ordered list*)
diff -r b46f48256dab -r 4919bd124a58 src/Pure/type.ML
--- a/src/Pure/type.ML	Wed Aug 27 11:24:35 2008 +0200
+++ b/src/Pure/type.ML	Wed Aug 27 11:48:54 2008 +0200
@@ -17,7 +17,7 @@
   val rep_tsig: tsig ->
    {classes: NameSpace.T * Sorts.algebra,
     default: sort,
-    types: ((decl * Markup.property list) * serial) NameSpace.table,
+    types: ((decl * Properties.T) * serial) NameSpace.table,
     log_types: string list}
   val empty_tsig: tsig
   val defaultS: tsig -> sort
@@ -40,7 +40,7 @@
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int
   val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
-  val the_tags: tsig -> string -> Markup.property list
+  val the_tags: tsig -> string -> Properties.T
 
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
@@ -73,9 +73,9 @@
   val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
-  val add_type: NameSpace.naming -> Markup.property list -> bstring * int -> tsig -> tsig
-  val add_abbrev: NameSpace.naming -> Markup.property list -> string * string list * typ -> tsig -> tsig
-  val add_nonterminal: NameSpace.naming -> Markup.property list -> string -> tsig -> tsig
+  val add_type: NameSpace.naming -> Properties.T -> bstring * int -> tsig -> tsig
+  val add_abbrev: NameSpace.naming -> Properties.T -> string * string list * typ -> tsig -> tsig
+  val add_nonterminal: NameSpace.naming -> Properties.T -> string -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
   val add_arity: Pretty.pp -> arity -> tsig -> tsig
   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -105,7 +105,7 @@
   TSig of {
     classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
     default: sort,                          (*default sort on input*)
-    types: ((decl * Markup.property list) * serial) NameSpace.table, (*declared types*)
+    types: ((decl * Properties.T) * serial) NameSpace.table, (*declared types*)
     log_types: string list};                (*logical types sorted by number of arguments*)
 
 fun rep_tsig (TSig comps) = comps;