On Wed, 10 Jul 2013, Tjark Weber wrote:
I vaguely remember a private discussion about the performance of inner
syntax parsing in this respect. For a realistic import one would
bypass that anyway, i.e. not generate source files to parse them again,
but read things directly via some Isabelle/ML functions.
Agreed. Related functionality is available in HOL/ex/SAT_Examples.thy.
(Cleaning up old mail threads ...)
Looking superficially at
http://isabelle.in.tum.de/repos/isabelle/file/b7a83845bc93/src/HOL/ex/SAT_Examples.thy
I wonder if this actually works right now.
It used to be subject to "try use_thy ..." for several years, and the
current HOL/ROOT has it commented-out.
If you have some ambition to put it into shape, I can give some hints what
needs to be done. E.g. global ML reference variables need to be
eliminated and replaced by "configuration options" in ML (structure Config
with certain operations in structure Attrib) or "system options" in
ML/Scala (which are subject to persistent user preferences, potentially
available in the front-end).
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
