class COMPILER_COUNTER inherit SHARED_WORKBENCH COMPILER_EXPORTER create make feature -- Initialization make is -- Create a new counter. do end append (other: like Current) is -- Append ids generated by `other' to `Current' and -- renumber the resulting set of ids. require other_not_void: other /= Void do precompiled_offset := (precompiled_offset).max (other.count) count := precompiled_offset end feature -- Access next_id: INTEGER is -- Next id do count := count + 1 Result := count ensure id_not_void: Result > 0 end precompiled_offset: INTEGER -- Last Ids retrieved from precompiled library. count: INTEGER -- Number of ids in system. current_count: INTEGER is -- Number of ids generated during current compilation. do Result := count - precompiled_offset end is_precompiled (an_id: INTEGER): BOOLEAN is -- Is `an_id' a precompiled id? do Result := an_id <= precompiled_offset end feature -- Setting set_value (value: INTEGER) is -- Reset the counter so that next geneareted id -- will be `value' + 1 do count := value end set_precompiled_offset (v: INTEGER) is -- Assign `v' to `precompiled_offset'. require valid_value: v > 0 do precompiled_offset := v ensure precompiled_offset_set: precompiled_offset = v end end -- class COMPILER_COUNTER