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



OK, some tests:

> 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 *) ...

I can't really make sense of the error message
----------------------------------------------------------------------

text {* @{text "(op *)"} *}

I can't see any complete commands to process!

Remark: everything following in the theory file (except antiquotations)
is highlighted in the same color as HOL Terms (just as "%x. x" in term
"%x. x")

----------------------------------------------------------------------

text {* s @{term {*(op *)*} } foo *}

*** missing closing brace of antiquotation at term {*(op ...
*** At command "text".

Remark: Cursor jumps to the "}" right before the foo 


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)

I hope this helps

Can someone reproduce this? 

-- 
Gruß
Christian Doczkal

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



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