# HG changeset patch # User wenzelm # Date 1701283554 -3600 # Node ID 9d6359b712641de6f5e5be583a1895c88972a305 # Parent 2c457c4cd4864e9d44424f0839c00129bbbbb89c more compact representation of theory_id -- via consecutive thread-local ids; diff -r 2c457c4cd486 -r 9d6359b71264 src/Pure/context.ML --- a/src/Pure/context.ML Wed Nov 29 15:32:42 2023 +0100 +++ b/src/Pure/context.ML Wed Nov 29 19:45:54 2023 +0100 @@ -138,7 +138,26 @@ (* theory identity *) type id = int; -val new_id = Counter.make (); + +local + val new_block = Counter.make (); + fun new_elem () = Bitset.make_elem (new_block (), 0); + val var = Thread_Data.var () : id Thread_Data.var; +in + +fun new_id () = + let + val id = + (case Option.map Bitset.dest_elem (Thread_Data.get var) of + NONE => new_elem () + | SOME (m, n) => + (case try Bitset.make_elem (m, n + 1) of + NONE => new_elem () + | SOME elem => elem)); + val _ = Thread_Data.put var (SOME id); + in id end; + +end; abstype theory_id = Thy_Id of