# HG changeset patch
# User wenzelm
# Date 1118329002 -7200
# Node ID 6f0ca9628840040796c9c8974a373d0f01e06c5b
# Parent  94e565ded526ad1658ec87b0691672bdba1257bf
simplified is_stale, check_stale;
fixed map_sg -- proper treatment of non-drafts;

diff -r 94e565ded526 -r 6f0ca9628840 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Jun 09 12:06:38 2005 +0200
+++ b/src/Pure/sign.ML	Thu Jun 09 16:56:42 2005 +0200
@@ -235,7 +235,13 @@
 val stamp_names_of = rev o map ! o stamps_of;
 fun exists_stamp name = exists (equal name o !) o stamps_of;
 
-fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg);
+fun is_stale (Sg ({id, ...}, {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
+      id <> id'
+  | is_stale _ = false;
+
+fun pretty_sg sg =
+  Pretty.str_list "{" "}" (stamp_names_of sg @ (if is_stale sg then ["!"] else []));
+
 val pprint_sg = Pretty.pprint o pretty_sg;
 
 fun pretty_abbrev_sg sg =
@@ -249,13 +255,9 @@
 
 (* id and self *)
 
-fun check_stale pos (sg as Sg ({id, ...},
-        {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
-      if id = id' then sg
-      else raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
-  | check_stale _ _ = sys_error "Sign.check_stale";
-
-val is_stale = not o can (check_stale "Sign.is_stale");
+fun check_stale pos sg =
+  if is_stale sg then raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
+  else sg;
 
 fun self_ref (sg as Sg (_, {self, ...})) = (check_stale "Sign.self_ref" sg; self);
 
@@ -374,18 +376,25 @@
 val copy = new_sg copy_data;
 
 fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
- (check_stale "Sign.add_name" sg;
-  create_sg name self stamps naming data (syn, tsig, consts, spaces));
+  let
+    val _ = check_stale "Sign.add_name" sg;
+    val (self', data') =
+      if is_draft sg then (self, data)
+      else (SgRef (SOME (ref sg)), prep_ext_data data);
+  in create_sg name self' stamps naming data' (syn, tsig, consts, spaces) end;
 
-fun map_sg f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
+fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
   let
     val _ = check_stale "Sign.map_sg" sg;
-    val (naming', data', sign') = f (naming, data, (syn, tsig, consts, spaces));
-  in create_sg "#" self stamps naming' data' sign' end;
+    val (self', data') =
+      if is_draft sg andalso keep then (self, data)
+      else (SgRef (SOME (ref sg)), prep_ext_data data);
+    val (naming', data', sign') = f (naming, data', (syn, tsig, consts, spaces));
+  in create_sg "#" self' stamps naming' data' sign' end;
 
-fun map_naming f = map_sg (fn (naming, data, sign) => (f naming, data, sign));
-fun map_data f = map_sg (fn (naming, data, sign) => (naming, f data, sign));
-fun map_sign f = map_sg (fn (naming, data, sign) => (naming, data, f sign));
+fun map_naming f = map_sg true (fn (naming, data, sign) => (f naming, data, sign));
+fun map_data f = map_sg true (fn (naming, data, sign) => (naming, f data, sign));
+fun map_sign f = map_sg true (fn (naming, data, sign) => (naming, data, f sign));
 fun map_syn f = map_sign (fn (syn, tsig, consts, spaces) => (f syn, tsig, consts, spaces));