[isabelle] A trick with code generation from jEdit

Hi people out there,


  export_code f1 f2 … in SML file "filename"

is tricky from jEdit. As evaluation occurs as you edit, you get multiple files generated in your home directory, as you enter "filename" character by character. Ex. you will get one file named "f" then another named "filen" then finally another named "filename", all with the same content (obviously).

By the way, how do you change the default output directory? Do you have to always provide an absolute full path?

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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