type constructors now with markup

--- a/src/Pure/codegen.ML	Fri Jun 20 21:00:25 2008 +0200
+++ b/src/Pure/codegen.ML	Fri Jun 20 21:00:26 2008 +0200
@@ -388,7 +388,7 @@
     val tc = Sign.intern_type thy s;
   in
     case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
-      SOME (Type.LogicalType i, _) =>
+      SOME ((Type.LogicalType i, _), _) =>
         if num_args_of (fst syn) > i then
           error ("More arguments than corresponding type constructor " ^ s)
         else (case AList.lookup (op =) types tc of

--- a/src/Pure/display.ML	Fri Jun 20 21:00:25 2008 +0200
+++ b/src/Pure/display.ML	Fri Jun 20 21:00:26 2008 +0200
@@ -149,14 +149,14 @@
       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
 
     val tfrees = map (fn v => TFree (v, []));
-    fun pretty_type syn (t, (Type.LogicalType n, _)) =
+    fun pretty_type syn (t, ((Type.LogicalType n, _), _)) =
           if syn then NONE
           else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n))))
-      | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
+      | pretty_type syn (t, ((Type.Abbreviation (vs, U, syn'), _), _)) =
           if syn <> syn' then NONE
           else SOME (Pretty.block
             [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
-      | pretty_type syn (t, (Type.Nonterminal, _)) =
+      | pretty_type syn (t, ((Type.Nonterminal, _), _)) =
           if not syn then NONE
           else SOME (prt_typ (Type (t, [])));
 

--- a/src/Pure/sign.ML	Fri Jun 20 21:00:25 2008 +0200
+++ b/src/Pure/sign.ML	Fri Jun 20 21:00:26 2008 +0200
@@ -439,7 +439,8 @@
   let
     val syn' = Syntax.update_type_gram types syn;
     val decls = map (fn (a, n, mx) => (Syntax.type_name a mx, n)) types;
-    val tsig' = Type.add_types naming decls tsig;
+    val tags = [(Markup.theory_nameN, Context.theory_name thy)];
+    val tsig' = fold (Type.add_type naming tags) decls tsig;
   in (naming, syn', tsig', consts) end);
 
 
@@ -448,7 +449,7 @@
 fun add_nonterminals ns thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
     val syn' = Syntax.update_consts ns syn;
-    val tsig' = Type.add_nonterminals naming ns tsig;
+    val tsig' = fold (Type.add_nonterminal naming []) ns tsig;
   in (naming, syn', tsig', consts) end);
 
 
@@ -462,7 +463,7 @@
       val a' = Syntax.type_name a mx;
       val abbr = (a', vs, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt rhs))
         handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote a');
-      val tsig' = Type.add_abbrevs naming [abbr] tsig;
+      val tsig' = Type.add_abbrev naming [] abbr tsig;
     in (naming, syn', tsig', consts) end);
 
 val add_tyabbrs = fold (gen_add_tyabbr Syntax.parse_typ);

--- a/src/Pure/type.ML	Fri Jun 20 21:00:25 2008 +0200
+++ b/src/Pure/type.ML	Fri Jun 20 21:00:26 2008 +0200
@@ -17,7 +17,7 @@
   val rep_tsig: tsig ->
    {classes: NameSpace.T * Sorts.algebra,
     default: sort,
-    types: (decl * serial) NameSpace.table,
+    types: ((decl * Markup.property list) * serial) NameSpace.table,
     log_types: string list}
   val empty_tsig: tsig
   val defaultS: tsig -> sort
@@ -40,6 +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
 
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
@@ -72,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_types: NameSpace.naming -> (bstring * int) list -> tsig -> tsig
-  val add_abbrevs: NameSpace.naming -> (string * string list * typ) list -> tsig -> tsig
-  val add_nonterminals: NameSpace.naming -> string list -> 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 hide_type: bool -> string -> tsig -> tsig
   val add_arity: Pretty.pp -> arity -> tsig -> tsig
   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -104,7 +105,7 @@
   TSig of {
     classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
     default: sort,                          (*default sort on input*)
-    types: (decl * serial) NameSpace.table, (*declared types*)
+    types: ((decl * Markup.property list) * serial) NameSpace.table, (*declared types*)
     log_types: string list};                (*logical types sorted by number of arguments*)
 
 fun rep_tsig (TSig comps) = comps;
@@ -115,7 +116,7 @@
 fun build_tsig ((space, classes), default, types) =
   let
     val log_types =
-      Symtab.fold (fn (c, (LogicalType n, _)) => cons (c, n) | _ => I) (snd types) []
+      Symtab.fold (fn (c, ((LogicalType n, _), _)) => cons (c, n) | _ => I) (snd types) []
       |> Library.sort (Library.int_ord o pairself snd) |> map fst;
   in make_tsig ((space, classes), default, types, log_types) end;
 
@@ -125,6 +126,10 @@
 val empty_tsig =
   build_tsig ((NameSpace.empty, Sorts.empty_algebra), [], NameSpace.empty_table);
 
+fun lookup_type (TSig {types, ...}) = Option.map fst o Symtab.lookup (snd types);
+
+fun the_tags tsig = snd o the o lookup_type tsig;
+
 
 (* classes and sorts *)
 
@@ -177,7 +182,6 @@
 
 fun cert_typ_mode (Mode {normalize, logical}) tsig ty =
   let
-    val TSig {types = (_, types), ...} = tsig;
     fun err msg = raise TYPE (msg, [ty], []);
 
     val check_logical =
@@ -189,7 +193,7 @@
             val Ts' = map cert Ts;
             fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
           in
-            (case Symtab.lookup types c of
+            (case lookup_type tsig c of
               SOME (LogicalType n, _) => (nargs n; Type (c, Ts'))
             | SOME (Abbreviation (vs, U, syn), _) =>
                (nargs (length vs);
@@ -215,8 +219,8 @@
 
 (* type arities *)
 
-fun arity_number (TSig {types = (_, types), ...}) a =
-  (case Symtab.lookup types a of
+fun arity_number tsig a =
+  (case lookup_type tsig a of
     SOME (LogicalType n, _) => n
   | _ => error (undecl_type a));
 
@@ -514,7 +518,7 @@
 fun add_arity pp (t, Ss, S) tsig = tsig |> map_tsig (fn ((space, classes), default, types) =>
   let
     val _ =
-      (case Symtab.lookup (#2 types) t of
+      (case lookup_type tsig t of
         SOME (LogicalType n, _) => if length Ss <> n then error (bad_nargs t) else ()
       | SOME (decl, _) => error ("Illegal " ^ str_of_decl decl ^ ": " ^ quote t)
       | NONE => error (undecl_type t));
@@ -554,17 +558,17 @@
     else error ("Conflict of " ^ s ^ " with " ^ s' ^ ": " ^ quote c)
   end;
 
-fun new_decl naming (c, decl) (space, types) =
+fun new_decl naming tags (c, decl) (space, types) =
   let
     val c' = NameSpace.full naming c;
     val space' = NameSpace.declare naming c' space;
     val types' =
       (case Symtab.lookup types c' of
-        SOME (decl', _) => err_in_decls c' decl decl'
-      | NONE => Symtab.update (c', (decl, serial ())) types);
+        SOME ((decl', _), _) => err_in_decls c' decl decl'
+      | NONE => Symtab.update (c', ((decl, tags), serial ())) types);
   in (space', types') end;
 
-fun the_decl (_, types) = fst o the o Symtab.lookup types;
+fun the_decl (_, types) = fst o fst o the o Symtab.lookup types;
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
@@ -574,11 +578,16 @@
   in (classes, default, (space', tab')) end);
 
 fun syntactic types (Type (c, Ts)) =
-      (case Symtab.lookup types c of SOME (Nonterminal, _) => true | _ => false)
+      (case Symtab.lookup types c of SOME ((Nonterminal, _), _) => true | _ => false)
         orelse exists (syntactic types) Ts
   | syntactic _ _ = false;
 
-fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
+in
+
+fun add_type naming tags (c, n) = if n < 0 then err_neg_args c else
+  map_types (new_decl naming tags (c, LogicalType n));
+
+fun add_abbrev naming tags (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   let
     fun err msg = cat_error msg ("The error(s) above occurred in type abbreviation: " ^ quote a);
     val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
@@ -590,17 +599,10 @@
     (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
       [] => []
     | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
-    types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
+    types |> new_decl naming tags (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs'))
   end);
 
-in
-
-fun add_types naming ps = map_types (fold (new_decl naming) (ps |> map (fn (c, n) =>
-  if n < 0 then err_neg_args c else (c, LogicalType n))));
-
-val add_abbrevs = fold o add_abbrev;
-
-fun add_nonterminals naming = map_types o fold (new_decl naming) o map (rpair Nonterminal);
+fun add_nonterminal naming tags = map_types o new_decl naming tags o rpair Nonterminal;
 
 fun merge_types (types1, types2) =
   NameSpace.merge_tables (Library.eq_snd (op = : serial * serial -> bool)) (types1, types2)