Use serial to be more debug friendly.
authorballarin
Mon Feb 01 21:55:00 2010 +0100 (2010-02-01)
changeset 36088a4369989bc45
parent 34963 366a1a44aac2
child 36089 8078d496582c
Use serial to be more debug friendly.
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Fri Jan 22 16:59:21 2010 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Feb 01 21:55:00 2010 +0100
     1.3 @@ -97,11 +97,11 @@
     1.4    intros: thm option * thm option,
     1.5    axioms: thm list,
     1.6    (** dynamic part **)
     1.7 -  decls: (declaration * stamp) list * (declaration * stamp) list,
     1.8 +  decls: (declaration * serial) list * (declaration * serial) list,
     1.9      (* type and term syntax declarations *)
    1.10 -  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list,
    1.11 +  notes: ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * serial) list,
    1.12      (* theorem declarations *)
    1.13 -  dependencies: ((string * morphism) * stamp) list
    1.14 +  dependencies: ((string * morphism) * serial) list
    1.15      (* locale dependencies (sublocale relation) *)
    1.16  };
    1.17  
    1.18 @@ -143,8 +143,8 @@
    1.19    thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
    1.20      (binding,
    1.21        mk_locale ((parameters, spec, intros, axioms),
    1.22 -        ((pairself (map (fn decl => (decl, stamp ()))) decls, map (fn n => (n, stamp ())) notes),
    1.23 -          map (fn d => (d, stamp ())) dependencies))) #> snd);
    1.24 +        ((pairself (map (fn decl => (decl, serial ()))) decls, map (fn n => (n, serial ())) notes),
    1.25 +          map (fn d => (d, serial ())) dependencies))) #> snd);
    1.26  
    1.27  fun change_locale name =
    1.28    Locales.map o apsnd o Symtab.map_entry name o map_locale o apsnd;
    1.29 @@ -331,9 +331,9 @@
    1.30  
    1.31  structure Registrations = Theory_Data
    1.32  (
    1.33 -  type T = ((string * (morphism * morphism)) * stamp) list *
    1.34 +  type T = ((string * (morphism * morphism)) * serial) list *
    1.35      (* registrations, in reverse order of declaration *)
    1.36 -    (stamp * ((morphism * bool) * stamp) list) list;
    1.37 +    (serial * ((morphism * bool) * serial) list) list;
    1.38      (* alist of mixin lists, per list mixins in reverse order of declaration *)
    1.39    val empty = ([], []);
    1.40    val extend = I;
    1.41 @@ -349,8 +349,8 @@
    1.42  fun compose_mixins mixins =
    1.43    fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity;
    1.44  
    1.45 -fun reg_morph mixins ((name, (base, export)), stamp) =
    1.46 -  let val mix = the_default [] (AList.lookup (op =) mixins stamp) |> compose_mixins;
    1.47 +fun reg_morph mixins ((name, (base, export)), serial) =
    1.48 +  let val mix = the_default [] (AList.lookup (op =) mixins serial) |> compose_mixins;
    1.49    in (name, base $> mix $> export) end;
    1.50  
    1.51  fun these_registrations thy name = Registrations.get thy
    1.52 @@ -367,7 +367,7 @@
    1.53      case find_first (fn ((name', (morph', export')), _) => ident_eq thy
    1.54        ((name', instance_of thy name' (morph' $> export')), (name, instance_of thy name morph))) (rev regs) of
    1.55        NONE => []
    1.56 -    | SOME (_, stamp) => the_default [] (AList.lookup (op =) mixins stamp)
    1.57 +    | SOME (_, serial) => the_default [] (AList.lookup (op =) mixins serial)
    1.58    end;
    1.59  
    1.60  fun collect_mixins thy (name, morph) =
    1.61 @@ -442,8 +442,8 @@
    1.62            quote (extern thy name) ^ " and\nparameter instantiation " ^
    1.63            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
    1.64            " available")
    1.65 -      | SOME (_, stamp') => Registrations.map 
    1.66 -          (apsnd (AList.map_default (op =) (stamp', []) (cons (mixin, stamp ())))) thy
    1.67 +      | SOME (_, serial') => Registrations.map 
    1.68 +          (apsnd (AList.map_default (op =) (serial', []) (cons (mixin, serial ())))) thy
    1.69      (* FIXME deal with inheritance: propagate to existing children *)
    1.70    end;
    1.71  
    1.72 @@ -461,10 +461,11 @@
    1.73          fun add_reg (dep', morph') =
    1.74            let
    1.75              val mixins = collect_mixins thy (dep', morph' $> export);
    1.76 -            val stamp = stamp ();
    1.77 +            (* FIXME empty list *)
    1.78 +            val serial = serial ();
    1.79            in
    1.80 -            Registrations.map (apfst (cons ((dep', (morph', export)), stamp))
    1.81 -              #> apsnd (cons (stamp, mixins)))
    1.82 +            Registrations.map (apfst (cons ((dep', (morph', export)), serial))
    1.83 +              #> apsnd (cons (serial, mixins)))
    1.84            end
    1.85        in
    1.86          (get_idents (Context.Theory thy), thy)
    1.87 @@ -484,7 +485,7 @@
    1.88  
    1.89  fun add_dependency loc (dep, morph) export thy =
    1.90    thy
    1.91 -  |> (change_locale loc o apsnd) (cons ((dep, morph $> export), stamp ()))
    1.92 +  |> (change_locale loc o apsnd) (cons ((dep, morph $> export), serial ()))
    1.93    |> (fn thy => fold_rev (Context.theory_map o activate_facts' export)
    1.94        (all_registrations thy) thy);
    1.95    (* FIXME deal with inheritance: propagate mixins to new children *)
    1.96 @@ -498,7 +499,7 @@
    1.97    let
    1.98      val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
    1.99      val ctxt'' = ctxt' |> ProofContext.theory (
   1.100 -      (change_locale loc o apfst o apsnd) (cons (args', stamp ()))
   1.101 +      (change_locale loc o apfst o apsnd) (cons (args', serial ()))
   1.102          #>
   1.103        (* Registrations *)
   1.104        (fn thy => fold_rev (fn (_, morph) =>
   1.105 @@ -517,7 +518,7 @@
   1.106  fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   1.107  
   1.108  fun add_decls add loc decl =
   1.109 -  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   1.110 +  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, serial ()))) #>
   1.111    add_thmss loc ""
   1.112      [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
   1.113        [([Drule.dummy_thm], [])])];