Custom Query (361 matches)

Filters
 
Or
 
  
 
Columns

Show under each result:


Results (91 - 93 of 361)

Ticket Resolution Summary Owner Reporter
#376 fixed Enable and complete testing of parser cache, add to user options menu David Aspinall David Aspinall
Description

PG has a cache available to reduce the amount of parsing that takes place in the buffer. It hasn't been comprehensively tested yet so is disabled by default. Enable it with (setq proof-use-parser-cache t).

#330 fixed Error raised by proof-issue-goal and proof-issue-save David Aspinall Erik Martin-Dorel
Description

When I run the function proof-issue-goal or proof-issue-save (e.g. by clicking on proof-toolbar-goal or proof-toolbar-qed), the requested command is well executed, except that the following error is raised:

progn: Wrong type argument: integer-or-marker-p, t

The bug is reproducible with the current CVS version of PG, with GNU-Emacs-23.2.1 & Coq-8.2pl2.

I think this bug comes from the presence of "(goto-char" at the end of proof-issue-new-command.

Kind regards, Erik.

#164 wontfix Error with GNU Emacs 21.4.1/C-c C-BS David Aspinall David Aspinall
Description

I'm going through the "walkthrough example in Isabelle/Isar?" in section 2.1 of the user manual. When I come to the bit about backing up with C-c C-BS, emacs gives the error "wrong type argument: listp, #<overlay from 74 to 92 in Walkthrough.thy>". The same happens if I choose Undo Step or Delete Step from the menu.

Playing around further, if I get to the line "then obtain B and A .." and then press C-c C-RET, I get a similar error "error in process filter: Wrong type argument: listp #<overlay..>". After this, if I try to choose "Restart Scripting" from the menu, emacs hangs.

I tried this with both ProofGeneral 3.6 and 3.7 and Isabelle2005 under emacs 21.4.1. Any help would be greatly appreciated.

Note: See TracQuery for help on using queries.