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 David Aspinall

Milestone: PG-Eclipse-1.1.0PG-Eclipse-1.0.7

comment:2 Changed 16 years ago by Makarius

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

comment:3 Changed 11 years ago by David Aspinall

Milestone: PG-Eclipse-1.0.7

Milestone PG-Eclipse-1.0.7 deleted

Note: See TracTickets for help on using tickets.