Re: [isabelle] ProofGeneral font-lock-mode and antiquoatations

Thanks a lot Makarius

> This is a known problem of Proof General 3.7.1 running on GNU Emacs. 
> Maybe this helps:

This did indeed solve the problem (merely changing this single file in
PG 3.7.1. 

> Anyway, what is "todays version of FirstSteps.thy"?  I have never heard of 
> such a file in the Isabelle repository. "Yesterdays development snapshot" 
> is also hard to pin down.

OK, I should have been more precise. I was referring tho the file
"FirstSteps.thy" from the Isabelle Documentation Project. 

> With distributed version control (Mercurial), one needs to refer to 
> versions via the official id -- commit dates don't count.  In Isabelle 
> development snapshots this is printed as "welcome" message of 
> isabelle-process or by "isabelle version".

I was referring to:
Isabelle repository snapshot 228905e02350 (23-Jul-2009)

But with font-lock-mode working again it was easy to spot the mistake.
There is only a space missing in "FirstSteps.thy". (diff attached,
referring to rev d6e9fb662d68, in case someone from the IDP reads this)

Thanks a lot, so now I can continue trying to understand the Isabelle

Have a nice weekend. 

Christian Doczkal
<   \mbox{ at {text "(op *)"}}:
>   \mbox{ at {text "(op * )"}}:

Attachment: smime.p7s
Description: S/MIME cryptographic signature

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