#262 |
make jobserver unavailable
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#281 |
Odd unicode abbreviations, notably |>
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#289 |
Drawback of command wrapping in PG+Isar
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#291 |
3-Panel-mode: Strange buffer switch when loading a theory
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#294 |
Make pg-protected-undo allow in undo in comments of locked region
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#309 |
-p option (Isar interface) does not permit additional parameters to emacs executable
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#310 |
Subscripts in locked region are revealed the moment you finish a lemma
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#311 |
Unicode tokens: cannot select certain fonts from menu
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#316 |
UI glitch: point still jumps about when follow-mode=never move
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#331 |
Coq config for proof-goal-command and proof-save-command
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#340 |
Key binding syntax in proof-splash.el
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#342 |
Distracting error (actually raised by coq-command-at-point)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#343 |
Missing test in proof-store-buffer-win
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#347 |
Slight change in proof-store-buffer-win to enable undo in the Notepad
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#348 |
Need to update in coq-syntax.el the keywords containing the word Local
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#356 |
Coq identifiers are unexpectedly colorized
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#359 |
Fix coq.el bindings (coq-insert-term, proof-store-goals-win, & coq-SearchAbout)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
7:prover-coq
|
#362 |
Proof Completed message for Coq is lost
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.0
|
2:pg-emacs
|
#399 |
dvi target in doc/Makefile.doc missing
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#407 |
proof-undo-and-delete-last-successful-command does not meet spec
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#408 |
Auto compile fails if coq-compile-response-buffer has been killed
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#419 |
Print Fully Explicit option gets out of sync after undoing before point where it was changed
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
7:prover-coq
|
#422 |
Support for entering ellipsis in electric terminator mode
|
David Aspinall
|
enhancement
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#423 |
List customisation variables use wrong widget
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.1
|
2:pg-emacs
|
#466 |
parentheses in comments should not affect indentation level of non-comment code
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#470 |
texinfo 5.1 incompatibility
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#471 |
ProofGeneral.jpg missing in ProofGeneral-4.3pre130510.tgz
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#472 |
texi2pdf loads Proofgeneral.pdf as image
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#473 |
Indentation screwed up by "/." (not by "/ .") in, e.g., [Arguments foo /.]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#474 |
Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning multiple lines
|
courtieu
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#475 |
[exists] tactic causes improper indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#476 |
[Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have indented proof scripts
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#477 |
[Proposition] is not highlighted like [Lemma]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#478 |
[Proof <body term>.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#479 |
[intros ??.] messes up following indentation
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#482 |
[lazymatch] should be highlighted and indented like [match]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#484 |
[Existing Instances] should be highlighted like [Existing Instance]
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#485 |
"Time commands" option offsets the cursor when errors are reported
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#486 |
Disable long indention under quantifiers?
|
courtieu
|
defect
|
minor
|
PG-Emacs-4.3
|
3:pg-broker
|
#487 |
Coq syntax highlighting: Proposition
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#489 |
Electric Terminator mode breaks desktop-save-mode
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#492 |
Proof General: script management confused, couldn't find goal span for save. when evaluating past the bottom of a module that contains a theorem with the same name as the module
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#500 |
Build fails, due to “'isar-markup-ml' is not known to be defined.” (PG 4.2, Mac OS 10.10.2, Aquamacs 3.2)
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#503 |
Some coq output get lost for query processed just after an error stops the queue.
|
David Aspinall
|
defect
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#504 |
Minor fix for coq-is-symbol-or-punct and coq-grab-punctuation-left
|
cpitcla
|
enhancement
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#505 |
Fix indentation of lazymatch in Coq
|
cpitcla
|
enhancement
|
minor
|
PG-Emacs-4.3
|
2:pg-emacs
|
#78 |
Preferences: support dynamically computed defaults
|
David Aspinall
|
enhancement
|
trivial
|
|
1:pg-eclipse
|
#116 |
Coq syntax highlighting: identifiers starting with "fun" are wrongly coloured
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-3.7
|
2:pg-emacs
|
#379 |
Syntax error in ProofGeneral.desktop file
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#394 |
Coq "Library" keyword - incorrect coloring
|
courtieu
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#396 |
error in proof-shell-insert-hook docstring
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#414 |
PG thinks Preterm command is not state-preserving
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
2:pg-emacs
|
#415 |
Wrong file mentioned in installation notes
|
David Aspinall
|
defect
|
trivial
|
PG-Emacs-4.1
|
6:web-and-docs
|