Opened 17 years ago
Last modified 11 years ago
#93 new defect
Propagate position information in errors to make available to interface
Reported by: | David Aspinall | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 4:prover-isabelle | Keywords: | |
Cc: |
Description
Some exceptions in Isabelle already carry position information. However, this is lost when output is dumped. We want to make this information available as PGIP location attributes.
Change History (3)
comment:1 Changed 17 years ago by
Milestone: | PG-Eclipse-1.1.0 → PG-Eclipse-1.0.7 |
---|
comment:2 Changed 16 years ago by
Note: See
TracTickets for help on using
tickets.
In post-Isabelle2007, any transaction may retrieve source position information from the execution context, using Position.thread_data. The content is of type Position.T, which will eventually also hold proper transaction identification, along with more precise source indication (with columns counted according to Isabelle symbols).