[isabelle-dev] Declaration depending on user proofs

[Alexander Krauss]

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