clarified history stage: allow independent updates that are merged later;
authorwenzelm
Thu Jul 04 11:26:00 2019 +0200 (2 weeks ago)
changeset 7036003430649a7d2
parent 70359 470d4f145e4c
child 70361 34b271c4f400
clarified history stage: allow independent updates that are merged later;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Mon Jun 24 16:26:25 2019 +0200
     1.2 +++ b/src/Pure/context.ML	Thu Jul 04 11:26:00 2019 +0200
     1.3 @@ -117,6 +117,10 @@
     1.4  
     1.5  (** datatype theory **)
     1.6  
     1.7 +type stage = int * int Synchronized.var;
     1.8 +fun init_stage () : stage = (0, Synchronized.var "Context.stage" 1);
     1.9 +fun next_stage ((_, state): stage) = (Synchronized.change_result state (fn n => (n, n + 1)), state);
    1.10 +
    1.11  datatype theory_id =
    1.12    Theory_Id of
    1.13     (*identity*)
    1.14 @@ -124,7 +128,7 @@
    1.15      ids: Inttab.set} *            (*cumulative identifiers -- symbolic body content*)
    1.16     (*history*)
    1.17     {name: string,                 (*official theory name*)
    1.18 -    stage: int};                  (*counter for anonymous updates*)
    1.19 +    stage: stage option};         (*index and counter for anonymous updates*)
    1.20  
    1.21  datatype theory =
    1.22    Theory of
    1.23 @@ -153,7 +157,7 @@
    1.24  val data_of = #3 o rep_theory;
    1.25  
    1.26  fun make_identity id ids = {id = id, ids = ids};
    1.27 -fun make_history name stage = {name = name, stage = stage};
    1.28 +fun make_history name = {name = name, stage = SOME (init_stage ())};
    1.29  fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
    1.30  
    1.31  val theory_id_long_name = #name o history_of_id;
    1.32 @@ -169,11 +173,11 @@
    1.33  (* names *)
    1.34  
    1.35  val PureN = "Pure";
    1.36 -val finished = ~1;
    1.37  
    1.38  fun display_name thy_id =
    1.39 -  let val {name, stage} = history_of_id thy_id;
    1.40 -  in if stage = finished then name else name ^ ":" ^ string_of_int stage end;
    1.41 +  (case history_of_id thy_id of
    1.42 +    {name, stage = NONE} => name
    1.43 +  | {name, stage = SOME (i, _)} => name ^ ":" ^ string_of_int i);
    1.44  
    1.45  fun display_names thy =
    1.46    let
    1.47 @@ -197,7 +201,7 @@
    1.48      (case find_first (fn thy' => theory_name' long thy' = name) (ancestors_of thy) of
    1.49        SOME thy' => thy'
    1.50      | NONE => error ("Unknown ancestor theory " ^ quote name))
    1.51 -  else if #stage (history_of thy) = finished then thy
    1.52 +  else if is_none (#stage (history_of thy)) then thy
    1.53    else error ("Unfinished theory " ^ quote name);
    1.54  
    1.55  
    1.56 @@ -335,7 +339,7 @@
    1.57  (* primitives *)
    1.58  
    1.59  val pre_pure_thy =
    1.60 -  create_thy Inttab.empty (make_history PureN 0) (make_ancestry [] []) Datatab.empty;
    1.61 +  create_thy Inttab.empty (make_history PureN) (make_ancestry [] []) Datatab.empty;
    1.62  
    1.63  local
    1.64  
    1.65 @@ -344,10 +348,10 @@
    1.66      val Theory_Id ({id, ids}, {name, stage}) = theory_id thy;
    1.67      val Theory (_, ancestry, data) = thy;
    1.68      val (ancestry', data') =
    1.69 -      if stage = finished then
    1.70 +      if is_none stage then
    1.71          (make_ancestry [thy] (extend_ancestors thy (ancestors_of thy)), extend_data data)
    1.72        else (ancestry, data);
    1.73 -    val history' = {name = name, stage = if finish then finished else stage + 1};
    1.74 +    val history' = {name = name, stage = if finish then NONE else Option.map next_stage stage};
    1.75      val ids' = insert_id id ids;
    1.76      val data'' = f data';
    1.77    in create_thy ids' history' ancestry' data'' end;
    1.78 @@ -368,7 +372,7 @@
    1.79  fun merge_thys thys =
    1.80    let
    1.81      val ids = merge_ids thys;
    1.82 -    val history = make_history "" 0;
    1.83 +    val history = make_history "";
    1.84      val ancestry = make_ancestry [] [];
    1.85      val data = merge_data thys (apply2 data_of thys);
    1.86    in create_thy ids history ancestry data end;
    1.87 @@ -394,7 +398,7 @@
    1.88          | thy :: thys => Library.foldl merge_thys (thy, thys));
    1.89        val Theory_Id ({ids, ...}, _) = theory_id thy0;
    1.90  
    1.91 -      val history = make_history name 0;
    1.92 +      val history = make_history name;
    1.93        val ancestry = make_ancestry parents ancestors;
    1.94      in create_thy ids history ancestry (data_of thy0) |> tap finish_thy end;
    1.95