Re: [isabelle-dev] [isabelle] Code_Abstract_Nat raises exception for a variable with name g

2014-06-29 Thread Florian Haftmann
Hi Andreas, see now http://isabelle.in.tum.de/repos/isabelle/rev/91f9e4148460. Despite the ambitious commit message, for economic reasons I did not attempt to modernize the whole preprocessor but restricted myself to low-level tinkering with maxidx. Cheers, Florian On 18.06.2014 23:19,

Re: [isabelle-dev] JinjaThreads CYCLES-Exception at export-code

2014-06-29 Thread Florian Haftmann
See now http://isabelle.in.tum.de/repos/isabelle/rev/47c8475e7864. Interesting to see how bad dynamic typing actually is… Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP

[isabelle-dev] Code preprocessor tracing

2014-06-29 Thread Florian Haftmann
Hi Andreas, with http://isabelle.in.tum.de/repos/isabelle/rev/020cea57eaa4 I have provided very basic means to trace the code preprocessor. Alas, I only dimly remember what your real requirements are, so feel free to comment on it. Anyway, it is a starting point. Cheers, Florian --

[isabelle-dev] Product on lists

2014-06-29 Thread Florian Haftmann
The attached patches provide product on lists, where as much of the development is shared with sums on lists (similar to products and sums on sets). I am reluctant to push such a massive extension so short before a release without having it exposed to critical eyes. For my part I do not see much

Re: [isabelle-dev] JEdit FAILED

2014-06-29 Thread Lars Noschinski
On 28.06.2014 17:24, Makarius wrote: On Sat, 28 Jun 2014, Makarius wrote: On Sat, 28 Jun 2014, Florian Haftmann wrote: suggests that something is bad with $JEDIT_HOME in the mira build environment. JEDIT_HOME is a normal Isabelle setting, provided by the etc/settings of that component