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

Reply via email to