[isabelle-dev] NEWS: more uniform options (e.g. quick_and_dirty)
makarius at sketis.net
Fri May 17 22:40:21 CEST 2013
* Uniform management of "quick_and_dirty" as system option (see also
"isabelle options"), configuration option within the context (see also
Config.get in Isabelle/ML), and attribute in Isabelle/Isar. Minor
INCOMPATIBILITY, need to use more official Isabelle means to access
quick_and_dirty, instead of historical poking into mutable reference.
This refers to Isabelle/fd533ac64390.
Various other options have become more "official" over the past few days,
months, years; quick_and_dirty is mentioned specifically in the NEWS since
it is likely to occur in old-stile "quick_and_dirty := true" form for some
Here are further examples how it works now:
$ isabelle-process -o quick_and_dirty=true
$ isabelle tty -o quick_and_dirty=true
ML> Config.put quick_and_dirty true
Isar> declare [[quick_and_dirty = true]]
Proof General provides the usual (stateful) preferences, which work again
after many years of unclear state.
Isabelle/jEdit does *not* provide a way to change the option on the fly,
since its model is stateless.
More information about the isabelle-dev