[isabelle-dev] Concerning AFP 2a0f81020af9

2013-10-31 Thread Florian Haftmann
In thys/JinjaThreads/Examples/ApprenticeChallenge.thy: export_code ApprenticeChallenge_annotated exec_J_rr J2JVM Apprentice main Null exec_JVM_rr in SML module_name JT file /tmp/NEW ^^ This is definitely not nice, especially in a shared

Re: [isabelle-dev] Concerning AFP 2a0f81020af9

2013-10-31 Thread Florian Haftmann
The whole export_code - block can be removed, I'll do it in afp-devel, Thanks. but someone has to remove it in the snapshot. What is »the snapshot« in this context? The develepment snapshot on http://afp.sourceforge.net/download.shtml is volatile. Florian -- PGP available:

Re: [isabelle-dev] Concerning AFP 2a0f81020af9

2013-10-31 Thread Peter Lammich
On Do, 2013-10-31 at 10:57 +0100, Florian Haftmann wrote: The whole export_code - block can be removed, I'll do it in afp-devel, Thanks. but someone has to remove it in the snapshot. I meant the release branch of AFP, that Gerwin made a few days ago. See also: