[isabelle-dev] The coming release

[Jasmin Blanchette]

Am 24.09.2013 um 22:10 schrieb Makarius <makarius at sketis.net>:

> OK, I will tell you when we are getting close to the fork point.

Thanks. We'll try to maintain the "ready to be forked" invariant, but it's always good to have advance notice, if nothing else so that we avoid bigger changes right before the fork.

> Just formally for a proper release, you need to make sure that there are no spurious tracing and debugging messages left.

54c8dee1295a should address that.

(Lorenz, you can reintroduce the messages once Makarius has forked. Alternatively, you can use a configuration option to control the level of output. See e.g. the "metis_trace" option in "src/HOL/Tools/Metis/metis_generate.ML" for how it's usually done.)

> BTW, Pretty.item allows to make nice square bullets for itemization (visible in Isabelle/jEdit only).

Do you have a specific use in mind w.r.t. BNF or is this just a general hint (e.g. for Sledgehammer and Nitpick)?

Jasmin