src/Pure/sign.ML
changeset 16354 6f0ca9628840
parent 16337 5734de2f7ace
child 16368 a06868ebeb0f
     1.1 --- a/src/Pure/sign.ML	Thu Jun 09 12:06:38 2005 +0200
     1.2 +++ b/src/Pure/sign.ML	Thu Jun 09 16:56:42 2005 +0200
     1.3 @@ -235,7 +235,13 @@
     1.4  val stamp_names_of = rev o map ! o stamps_of;
     1.5  fun exists_stamp name = exists (equal name o !) o stamps_of;
     1.6  
     1.7 -fun pretty_sg sg = Pretty.str_list "{" "}" (stamp_names_of sg);
     1.8 +fun is_stale (Sg ({id, ...}, {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
     1.9 +      id <> id'
    1.10 +  | is_stale _ = false;
    1.11 +
    1.12 +fun pretty_sg sg =
    1.13 +  Pretty.str_list "{" "}" (stamp_names_of sg @ (if is_stale sg then ["!"] else []));
    1.14 +
    1.15  val pprint_sg = Pretty.pprint o pretty_sg;
    1.16  
    1.17  fun pretty_abbrev_sg sg =
    1.18 @@ -249,13 +255,9 @@
    1.19  
    1.20  (* id and self *)
    1.21  
    1.22 -fun check_stale pos (sg as Sg ({id, ...},
    1.23 -        {self = SgRef (SOME (ref (Sg ({id = id', ...}, _)))), ...})) =
    1.24 -      if id = id' then sg
    1.25 -      else raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
    1.26 -  | check_stale _ _ = sys_error "Sign.check_stale";
    1.27 -
    1.28 -val is_stale = not o can (check_stale "Sign.is_stale");
    1.29 +fun check_stale pos sg =
    1.30 +  if is_stale sg then raise TERM ("Stale signature (in " ^ pos ^ "): " ^ str_of_sg sg, [])
    1.31 +  else sg;
    1.32  
    1.33  fun self_ref (sg as Sg (_, {self, ...})) = (check_stale "Sign.self_ref" sg; self);
    1.34  
    1.35 @@ -374,18 +376,25 @@
    1.36  val copy = new_sg copy_data;
    1.37  
    1.38  fun add_name name (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
    1.39 - (check_stale "Sign.add_name" sg;
    1.40 -  create_sg name self stamps naming data (syn, tsig, consts, spaces));
    1.41 +  let
    1.42 +    val _ = check_stale "Sign.add_name" sg;
    1.43 +    val (self', data') =
    1.44 +      if is_draft sg then (self, data)
    1.45 +      else (SgRef (SOME (ref sg)), prep_ext_data data);
    1.46 +  in create_sg name self' stamps naming data' (syn, tsig, consts, spaces) end;
    1.47  
    1.48 -fun map_sg f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
    1.49 +fun map_sg keep f (sg as Sg ({stamps, syn, ...}, {self, tsig, consts, naming, spaces, data})) =
    1.50    let
    1.51      val _ = check_stale "Sign.map_sg" sg;
    1.52 -    val (naming', data', sign') = f (naming, data, (syn, tsig, consts, spaces));
    1.53 -  in create_sg "#" self stamps naming' data' sign' end;
    1.54 +    val (self', data') =
    1.55 +      if is_draft sg andalso keep then (self, data)
    1.56 +      else (SgRef (SOME (ref sg)), prep_ext_data data);
    1.57 +    val (naming', data', sign') = f (naming, data', (syn, tsig, consts, spaces));
    1.58 +  in create_sg "#" self' stamps naming' data' sign' end;
    1.59  
    1.60 -fun map_naming f = map_sg (fn (naming, data, sign) => (f naming, data, sign));
    1.61 -fun map_data f = map_sg (fn (naming, data, sign) => (naming, f data, sign));
    1.62 -fun map_sign f = map_sg (fn (naming, data, sign) => (naming, data, f sign));
    1.63 +fun map_naming f = map_sg true (fn (naming, data, sign) => (f naming, data, sign));
    1.64 +fun map_data f = map_sg true (fn (naming, data, sign) => (naming, f data, sign));
    1.65 +fun map_sign f = map_sg true (fn (naming, data, sign) => (naming, data, f sign));
    1.66  fun map_syn f = map_sign (fn (syn, tsig, consts, spaces) => (f syn, tsig, consts, spaces));
    1.67  
    1.68