[isabelle] Jedit and export_code
I just typed in Isabelle/jedit:
export_code foo in SML file "benchmarks/foo.sml"
The result is, that it created, in the current folder, the files:
both containing the sml-code. Yep, I'm a slow typer but my machine is
also slow ;).
What probably happened here is that jedit re-processed the line
continuously, and generated all the files while I was still typing the
How to avoid such strange things in jedit, except for trying to
high-speed typing, or adding a line containing only ".xxx" before the
export_code line while typing?
This archive was generated by a fusion of
Pipermail (Mailman edition) and