[isabelle] A trick with code generation from jEdit



Hi people out there,

Writing

  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.