[isabelle-dev] NEWS: asynchronous print functions etc.
makarius at sketis.net
Wed Jul 17 21:40:41 CEST 2013
On Mon, 15 Jul 2013, Makarius wrote:
> On Mon, 15 Jul 2013, Dmitriy Traytel wrote:
>> "Code generator: dropping subsumed code equation" by Auto Quickcheck
>> I guess it would be the task the tools to omit such outbursts and not
>> globally on the IDE side?
> In principle Context_Position.is_visible should control that, and the tools
> should observe it accordingly.
The canonical way to do that is
Context_Position.if_visible ctxt warning
but this does not work for code equations, because the operations of
src/Pure/Isar/code.ML act on a global theory, which is always "visible" in
that sense. (Such flags cannot be changed on the background theory on the
fly, because it would extend that according to Theory.subthy and thus
affect derived results.)
I have a slightly different plan to silence solve_direct, with its global
unify trace options: depending on Context_Position.is_visible these will
be reset, on a different (auxiliary) theory that is used for the
Maybe Florian also has some ideas about codegen.
Now that things start to look nice in the Prover IDE, the old somewhat
crude message output becomes more apparant. Standards are higher today
than several years ago.
More information about the isabelle-dev