added str_of_sg: sg -> string;
authorwenzelm
Fri Oct 31 15:15:06 1997 +0100 (1997-10-31)
changeset 40516b72919c9b4b
parent 4050 543df9687d7b
child 4052 026069ba0316
added str_of_sg: sg -> string;
improved error handling of data access;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Thu Oct 30 17:05:20 1997 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Oct 31 15:15:06 1997 +0100
     1.3 @@ -60,6 +60,7 @@
     1.4    val intern_tycons: sg -> xtyp -> typ
     1.5    val print_sg: sg -> unit
     1.6    val pretty_sg: sg -> Pretty.T
     1.7 +  val str_of_sg: sg -> string
     1.8    val pprint_sg: sg -> pprint_args -> unit
     1.9    val pretty_term: sg -> term -> Pretty.T
    1.10    val pretty_typ: sg -> typ -> Pretty.T
    1.11 @@ -159,8 +160,6 @@
    1.12  val pprint_sg = Pretty.pprint o pretty_sg;
    1.13  
    1.14  val tsig_of = #tsig o rep_sg;
    1.15 -val get_data = Data.get o #data o rep_sg;
    1.16 -val print_data = Data.print o #data o rep_sg;
    1.17  
    1.18  fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
    1.19  val classes = #classes o Type.rep_tsig o tsig_of;
    1.20 @@ -170,6 +169,15 @@
    1.21  val nonempty_sort = Type.nonempty_sort o tsig_of;
    1.22  
    1.23  
    1.24 +(* data *)
    1.25 +
    1.26 +fun access_data f sg = f (#data (rep_sg sg))
    1.27 +  handle ERROR => error ("of theory " ^ str_of_sg sg);
    1.28 +
    1.29 +val get_data = access_data Data.get;
    1.30 +val print_data = access_data Data.print;
    1.31 +
    1.32 +
    1.33  (* id and self *)
    1.34  
    1.35  fun check_stale (sg as Sg ({id, ...},
    1.36 @@ -849,7 +857,6 @@
    1.37    | merge_refs _ = sys_error "Sign.merge_refs";
    1.38  
    1.39  
    1.40 -
    1.41  (* proper merge *)
    1.42  
    1.43  fun merge_aux (sg1, sg2) =