Custom Query (361 matches)
Results (31 - 33 of 361)
| Ticket | Resolution | Summary | Owner | Reporter |
|---|---|---|---|---|
| #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 |
|||
| #103 | fixed | Add ASCII markup communication for Coq (fix UTF8 stream/FAQ no.1) | ||
| Description |
Coq still uses the troublesome UTF-8 prefix character that causes the "hang" in FAQ no.1. It should use an ASCII markup instead, like Isabelle's -mASCII flag. |
|||
| #109 | fixed | Missing output from Coq | ||
| Description |
Dear Proof General developers, In Coq, the identity tactic, idtac, is also used to print its arguments, for example, for debugging purposes. However, I don't see the output of idtac either in the *goals* or in the *response* buffer. For example, I don't see any output after executing the following script: Goal True. idtac "Hello!". Is there a way to correct this? Thank you, Yeveniy Makarov Emacs : GNU Emacs 21.4.1 (i386-redhat-linux-gnu, X toolkit, Xaw3d scroll bars) of 2006-03-07 on hs20-bc1-6.build.redhat.com Package: Proof General current state: ============== (setq proof-general-version "Proof General Version 3.6pre061027. Released by da." proof-assistant "Coq" ) |
|||
