Opened 17 years ago
Last modified 11 years ago
#134 assigned enhancement
Generalise lexing to better match Isar syntax
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description (last modified by )
We should generalise lexing to better match Isar's syntax rules. These are rather complex so we may be satisfied for now with an approximation (ultimately and unfortunately: prover-specific Java code to fine-tune). The PGIP lexicalstructure element can be tweaked to match. Tricky part here is allowing some update on-the-fly.
Change History (3)
comment:1 Changed 17 years ago by
| Status: | new → assigned |
|---|
comment:2 Changed 16 years ago by
| Description: | modified (diff) |
|---|---|
| Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.0.7 |
comment:3 Changed 11 years ago by
| Milestone: | PG-Eclipse-1.0.7 |
|---|
Note: See
TracTickets for help on using
tickets.
Milestone PG-Eclipse-1.0.7 deleted