Opened 13 years ago
Last modified 12 years ago
#385 accepted defect
Isabelle theorem dependencies display broken
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | PG-Emacs-4.3 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description
Isabelle output format has changed so proof-shell-theorem-dependency-list-regexp no longer matches.
Change History (3)
comment:1 Changed 13 years ago by
| Status: | new → accepted |
|---|
comment:2 Changed 13 years ago by
| Milestone: | PG-Emacs-4.1 → PG-Emacs-4.2 |
|---|---|
| Priority: | major → minor |
comment:3 Changed 12 years ago by
| Milestone: | PG-Emacs-4.2 → PG-Emacs-4.3 |
|---|
Note: See
TracTickets for help on using
tickets.
Problem: theorem names are now given with dotted prefixes, which don't match local names in buffer.
Makarius says:
These names emerge here:
http://isabelle.in.tum.de/repos/isabelle-release/file/79dae6b7857d/src/Pure/ProofGeneral/proof_general_pgip.ML#l263
The whole thing with Thm.get_name_hint is only an approximation anyway. One could make it even more crude by applying Long_Name.base_name.
It is probably better to maintain these qualified names on the PG side, and compare only the base names with the names that are guessed from the sources.