Opened 16 years ago

Closed 16 years ago

#214 closed defect (fixed)

Processing of buffer sensitive to Unicode option

Reported by: Clemens Ballarin Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-3.7.1
Component: 2:pg-emacs Keywords:
Cc:

Description

Issue where processing a buffer with Isabelle works if Unicode Tokens option disabled, but fails if enabled. The problem appears to be related to sub/superscripts.

Problem manifests with file "HOL/Algebra/Group.thy" from Isabelle repository. Error message

* Illegal reference to implicit structure #1 * The error(s) above occurred in axiom "nat_pow_def" * At command "defs".

when attempting to process line 35.

The following configuration was used:

GNU Emacs 22.2.1 (i386-apple-darwin8.11.1, Carbon Version 1.6.0) of 2008-04-02 on seijiz.local

Proof General cvs of 7 July 2008

Isabelle cvs of 7 Jully 2008

-- Clemens

Change History (1)

comment:1 Changed 16 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Now fixed in CVS. Thanks to Simon Winwood for identifying failure point.

Note: See TracTickets for help on using tickets.