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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
