* 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
users.
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
