Makarius wrote:
I would say it is virtually impossible to experiment with new commands in Proof General. One needs to produce isabelle-keywords.el in batch mode first, and then continue interactively.
My standard workaround is to edit isar-keywords.el manually, ignoring the WARNING IN CAPITAL LETTERS. This is OK for local experiments. I typically first copy the file to my .isabelle, so I cannot commit it by accident.
Alex _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev