>>> "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. > > Maybe Florian also has some ideas about codegen.
One answer would be to eliminate this meanwhile somehow ridiculous
warning entirely.
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
