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