Custom Query (361 matches)
Results (19 - 21 of 361)
| Ticket | Owner | Reporter | Resolution | Summary |
|---|---|---|---|---|
| #69 | fixed | PGMarkerMethods: skip spaces in document before error marker start | ||
| Description |
If error marker has been set by us based on command from document, spaces should be skipped which, if present, appear before start of command text proper. Test case: (* this is a comment *) lemma "!" |
|||
| #92 | duplicate | Attempt recovery from XML parse errors in PGIP main loop | ||
| Description |
Isabelle exits in case of erroneous XML input. It could be made more robust, which, e.g., helps debugging in case of editing XML by hand.
One suggestion is to attempt recovery by scanning for the next
See proof_general_pgip.ML, function |
|||
| #113 | fixed | Coq commands not described in coq/coq-syntax.el | ||
| Description |
Hello, The following commands, given in the "Vernacular Commands Index" in Coq Reference Manual are not listed in coq-commands-db in coq/coq-syntax.el. As a result, they are not highlighted and, more importantly, they are though to be not state preserving and so are not executed by proof-minibuffer-cmd command. About Pwd Search Test The "Check" command is mentioned but it is marked as not state preserving as well. Could you change this? Thank you, Yevgeniy |
|||
