[isabelle] Jedit and export_code



Hi List,

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:
  be
  benchmar

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
name.

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?


Best,
  Peter







This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.