Re: [isabelle] A few questions about Isabelle2013



On 1/15/2013 6:13 AM, Makarius wrote:
On Sat, 12 Jan 2013, Gottfried Barrow wrote:

COMMENTS CONTENT IS PICKIER

I got several errors I didn't get before for stuff that was in comments. I found what it was that made the comments happy.

Guessing and speculating again, it might be just malformed Isabelle symbols: anything starting with \< that is not properly terminated according to the \<foobar> or \<^foobar> syntax.

Here are simplified examples of what was in my comments.

These 5 examples give me an error that I don't get in Isabelle2012:

(* \<...>  *)
   Error: Malformed command syntax

--"\<rbrace>", --"\<lbrace>", --{* \<lbrace> *}, and --{* \<rbrace> *}
   Error: Unbalanced antiquotation block parentheses

The first example fits your description. I haven't used anitquotations, so I don't know why the other four examples give errors. Using any of the other left or right delimiters by themselves don't cause a problem, like using --"\<langle>" doesn't give an error.

I had actually mismatched \<lbrace and "}" in a comment for something like this:

   --{* \<lbrace>an_equation} *}

The left brace is used by itself sometimes in math. I'm not using it like that, so I don't care, at least not today.

Regards,
GB





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