Re: [isabelle] unexpected behaviour of user defined command in jedit



user has little control over the scheduling of command execution. One
workaround is to define your commands beforehand and build an image in
batch mode that is then used as starting point for the editor session.

This is no problem -- I anyway wanted to provide my commands by a precompiled image.

Thanks for your help,

Matthias





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