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,


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