[isabelle-dev] Towards the next release

[Makarius]

On Wed, 18 Apr 2012, Gerwin Klein wrote:

>> If 3) means "configuration option" in the sense of Config.T, here is 
>> the canonical 1-liner to make one for a package:
>>
>>  val split_limit = Attrib.setup_config_int @{binding linarith_split_limit} (K 9);
>
> Yes, that's what I meant. It's easy to set up, but pollutes the config 
> name space a little more for users. Of course it also means that it can 
> be changed at runtime. If there is a slight preference for this, I'm 
> happy to go that road.

The config name space is not a big deal.  The convention is now to have 
the tool prefix first, so the output of print_configs can be read as a 
poor-man's hierarchical structure of configuration options.

BTW, with the option changeable in the context, you could also make a 
boolean "record_codegen" without having to come up with a magic number for 
the limit.

The critical usage is then like this:

   declare [[record_codegen = false]]

   record my_big_record = ...

   declare [[record_codegen]]


 	Makarius