[isabelle-dev] Isabelle/jEdit: non-trivial theory merge

[Makarius]

On Mon, 12 Mar 2012, Makarius wrote:

> There is still no proper support for redefining Isar commands in the 
> running session.  So I would say the above is the normal consequence of 
> redefining 'function' in one theory while another one already reparses 
> an older version of it.  Thus the resulting transaction is from a 
> different theory (different version with the same name).
>
> Isabelle/8f3bb485f628 tries to make it a bit less erratic: commands are 
> always parsed dynamically.

Some more substantial refinements are in Isabelle/9ff441f295c2.  This 
means sessions like HOL or ZF should now be editable with Isabelle/jEdit 
without worries.  (A little bit of fine-tuning is still coming.)


 	Makarius