On Thu, 18 Jul 2013, Makarius wrote:
On Thu, 18 Jul 2013, Florian Haftmann 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.
I have generalized the concept to allow changing the visibility of a global
theory context as well. This is observed by unify.ML, as a guard to its many
tracing options, find_theorems.ML then copies the Proof.context visibility
over to a copy of the background theory of the goal state, so 'solve_direct'
no longer produces spam from this source, see Isabelle/d68fd63bf082.
One more amendment here: b824497c8e86 (I should not write emails while
isabelle build is running).
The desastrous effects of HO unify traces, which where showing up here in
solve_direct were mentioned on this thread started by Florian in 2009:
http://www.mail-archive.com/[email protected]/msg00776.html
Interesting, because it is mainly about the critical transition from PG
3.7.1.1 to PG 4.x and GNU Emacs 22 to 23 at that time. Neither of that is
of much relevance now, so it is fun to read about the old worries of
getting *any* combination to work at all.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
