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

On Sun, 26 Jul 2009, Christian Doczkal wrote:

of "(op *)" are valid instances of Isabelle input. Maybe
this helps to find out what the problem is.


ML {*
 (op *)

*** Outer lexical error: missing end of verbatim text at    (op *) ...
*** Outer syntax error: ML source expected,
*** but bad input {* was found
*** Outer lexical error: missing end of verbatim text at    (op *) ...

Considering the second and the fact that it seems to work in XEmacs my
question would be whether PG relies on emacs parsing to determine what
part of the theory to send to the isabelle process? (I have no clue how
this works)

From the Emacs point of view both {* ... *} and (* ... *) can count as
comment syntax. It depends on the Emacs version how they interact or nest, but most of the time it will just break down.

The deeper problem is manifold. XEmacs is hardly maintained anymore, and Proof General support of it is diminished in recent PG 3.7.x versions. In PG 4.0, if it is ever released, there will be only support for recent GNU Emacsen.


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