[isabelle-dev] NEWS: more uniform options (e.g. quick_and_dirty)

Makarius 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 mailing list