[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
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.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and