src/Pure/sign.ML

--- a/src/Pure/sign.ML	Wed Oct 15 15:15:22 1997 +0200
+++ b/src/Pure/sign.ML	Wed Oct 15 15:17:32 1997 +0200
@@ -102,12 +102,14 @@
   val add_path: string -> sg -> sg
   val add_space: string * string list -> sg -> sg
   val add_name: string -> sg -> sg
-  val make_draft: sg -> sg
-  val print_data: sg -> unit
-  val init_data: string * exn * (exn * exn -> exn) * (string -> exn -> Pretty.T) -> sg -> sg
+  val init_data: string * exn * (exn -> exn) * (exn * exn -> exn) *
+    (string -> exn -> unit) -> sg -> sg
   val get_data: sg -> string -> exn
   val put_data: string * exn -> sg -> sg
+  val print_data: sg -> string -> unit
+  val prep_ext: sg -> sg
   val merge: sg * sg -> sg
+  val nontriv_merge: sg * sg -> sg
   val proto_pure: sg
   val pure: sg
   val cpure: sg
@@ -356,12 +358,13 @@
     fun pretty_const (c, ty) = Pretty.block
       [Pretty.str (quote c ^ " ::"), Pretty.brk 1, prt_typ ty];
 
-    val Sg {tsig, const_tab, syn = _, path, spaces, data = _, stamps} = sg;
+    val Sg {tsig, const_tab, syn = _, path, spaces, data, stamps} = sg;
     val spaces' = sort (fn ((k1, _), (k2, _)) => k1 < k2) spaces;
     val {classes, classrel, default, tycons, abbrs, arities} =
       Type.rep_tsig tsig;
   in
     Pretty.writeln (Pretty.strs ("stamps:" :: stamp_names stamps));
+    Pretty.writeln (Pretty.strs ("data:" :: Data.kinds data));
     Pretty.writeln (Pretty.strs ["name entry path:", NameSpace.pack path]);
     Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_space spaces'));
     Pretty.writeln (pretty_classes classes);
@@ -799,26 +802,32 @@
 
 (* additional signature data *)
 
-fun print_data (Sg {data, ...}) = Data.print data;
-fun get_data (Sg {data, ...}) = Data.get data;
-
 fun map_data f (Sg {tsig, const_tab, syn, path, spaces, data, stamps}) =
   make_sign (syn, tsig, const_tab, (path, spaces)) (f data) stamps "#";
 
-fun init_data (kind, e, mrg, prt) = map_data (fn d => Data.init d kind e mrg prt);
+fun init_data (kind, e, ext, mrg, prt) =
+  map_data (fn d => Data.init d kind e ext mrg prt);
+
+fun get_data (Sg {data, ...}) = Data.get data;
 fun put_data (kind, e) = map_data (fn d => Data.put d kind e);
+fun print_data (Sg {data, ...}) kind = Data.print data kind;
+
+(*prepare extension*)
+val prep_ext = map_data Data.prep_ext;
 
 
 
 (** merge signatures **)    (*exception TERM*)
 
-fun merge_aux (sg1, sg2) =
+fun merge_aux triv_only (sg1, sg2) =
   if fast_subsig (sg2, sg1) then sg1
   else if fast_subsig (sg1, sg2) then sg2
   else if subsig (sg2, sg1) then sg1
   else if subsig (sg1, sg2) then sg2
   else if is_draft sg1 orelse is_draft sg2 then
     raise TERM ("Illegal merge of draft signatures", [])
+  else if triv_only then
+    raise TERM ("Illegal non-trivial merge of signatures", [])
   else
     (*neither is union already; must form union*)
     let
@@ -855,11 +864,14 @@
         path = [], spaces = spaces, data = data, stamps = stamps}
     end;
 
-fun merge sgs =
-  (case handle_error merge_aux sgs of
+fun gen_merge triv sgs =
+  (case handle_error (merge_aux triv) sgs of
     OK sg => sg
   | Error msg => raise TERM (msg, []));
 
+val merge = gen_merge true;
+val nontriv_merge = gen_merge false;
+
 
 
 (** the Pure signature **)