Timeline
May 28, 2007:
- 4:25 PM DeletingTicketSpam edited by
- (diff)
- 4:24 PM DeletingTicketSpam created by
- 4:19 PM WikiStart edited by
- (diff)
May 25, 2007:
- 3:03 PM Ticket #116 (Coq syntax highlighting: identifiers starting with "fun" are wrongly ...) closed by
- fixed: Here's a test case: […] This has been fixed in CVS head now. …
May 23, 2007:
- 1:43 PM Ticket #116 (Coq syntax highlighting: identifiers starting with "fun" are wrongly ...) created by
- In my Coq file, identifiers beginning with "fun" have the "fun" in …
May 11, 2007:
May 10, 2007:
- 11:49 PM Ticket #115 (Isabelle find-theorems form) created by
- Contribution from Tjark Weber: We have a tested and (hopefully) …
- 10:21 PM Ticket #114 (Spurious "replaced xyz occurrences" messages) closed by
- fixed: Fixed in CVS head now. This was a bug in PG introduced when fixing …
May 8, 2007:
- 3:57 PM Ticket #114 (Spurious "replaced xyz occurrences" messages) created by
- I keep getting "Replaced xyz occurrences" in the xemacs minibuffer …
Apr 26, 2007:
- 7:29 PM Ticket #113 (Coq commands not described in coq/coq-syntax.el) closed by
- fixed: Done, thank you for signaling this. Be aware that Check is available …
Apr 24, 2007:
- 5:26 PM Ticket #113 (Coq commands not described in coq/coq-syntax.el) created by
- Hello, The following commands, given in the "Vernacular Commands …
Apr 23, 2007:
- 10:21 AM Ticket #111 (Centering the goal window on the right part of the goals) closed by
- fixed: Replying to bertot: > In coq, when doing large proofs, …
- 10:00 AM Ticket #110 (Search Rewrite and Search About queries for Proof General/Coq) closed by
- fixed
Apr 16, 2007:
- 1:29 PM Ticket #109 (Missing output from Coq) closed by
- fixed: OK, this should be fixed. When Coq outputs a message followed by the …
Apr 5, 2007:
- 6:20 PM Ticket #112 (Filter out control characters in shell buffer or copy from shell buffer) created by
- Any idea how I can get rid of the characters such as Ú that appear in …
Mar 23, 2007:
- 1:24 PM Ticket #111 (Centering the goal window on the right part of the goals) created by
- In coq, when doing large proofs, the goals window tends to not be …
- 9:28 AM Ticket #110 (Search Rewrite and Search About queries for Proof General/Coq) created by
- The options "Search Rewrite ..." and "Search About ..." do not work in …
Mar 19, 2007:
- 10:14 AM WikiStart edited by
- (diff)
- 10:06 AM Ticket #109 (Missing output from Coq) created by
- Dear Proof General developers, In Coq, the identity tactic, idtac, is …
Mar 18, 2007:
- 12:15 PM Ticket #108 (Support proof object searching via search dialog) created by
- As a supplement to the IdView?, we may support proof object searching …
- 12:13 PM Ticket #107 (Support text file searching with symbol encoding/decoding) created by
- Text file search should support symbol decoding (tokenisation) in …
- 12:05 PM Ticket #8 (Cleanup active script handling in actions) closed by
- fixed: This is pretty much fixed now, although further refactoring of …
- 12:04 PM Ticket #106 (Add support for status area message responses) created by
- PGIP normalresponses with the area set to be "status" should be …
- 11:36 AM Ticket #6 (Add code folding for proof scripts) closed by
- fixed: Good basic support for code folding has now been added. It is enabled …
Mar 17, 2007:
- 4:33 PM Ticket #105 (Preference handling refactor: add description text preferences, use ...) created by
- Preference files use name attribute both for lookup of preferences and …
- 11:52 AM Ticket #104 (Add preference listener to ProofScriptDocument) created by
- This can usefully monitor several kinds of preference changes, e.g. …
- 11:50 AM Ticket #103 (Add ASCII markup communication for Coq (fix UTF8 stream/FAQ no.1)) closed by
- fixed: This has actually been provided a while ago, as coq-utf-safe.
Mar 12, 2007:
- 10:27 PM Ticket #103 (Add ASCII markup communication for Coq (fix UTF8 stream/FAQ no.1)) created by
- Coq still uses the troublesome UTF-8 prefix character that causes the …
Mar 10, 2007:
- 6:32 PM Ticket #102 (Simplify message model according to new RNC, change Isabelle to match) created by
- Some further discussion maybe required, but proposal in draft RNC for …
- 6:32 PM Ticket #101 (Add scriptreplace and menu choice interaction) created by
- * We have messages for (statically) configuring prover operations and …
- 4:59 PM Ticket #100 (Make sure that large volumes of data can be handled by all parts of ...) created by
- This is the old problem of too much output "choking" * In some …
- 4:53 PM Ticket #99 (Reliable interrupts) created by
- 4:49 PM Ticket #84 (Remove double-quoted XML output from term display) closed by
- fixed
- 4:48 PM Ticket #98 (PGML changes: complete update for PGML 2.0) created by
- This will come from * tokenised input (theory presentation) * …
- 4:02 PM Ticket #97 (Add Pretty.markup to parse tree output) created by
- This will allow several things: * Markup on constants as well as …
- 3:25 PM Ticket #96 (Start/stop quiet: disable these and use statedisplay instead) created by
- Small change in
proof_general_pgip.ML: disable printing by default, … - 3:24 PM Ticket #95 (Refine spuriouscmd into two: destructivecmd and diagnosticcmd) created by
- Makarius notes that spuriouscmd cannot be pruned from scripts because …
- 2:43 PM Ticket #94 (Selecting print mode via interface) created by
- Should we have some way of automatically configuring the output …
- 9:30 AM Ticket #93 (Propagate position information in errors to make available to interface) created by
- Some exceptions in Isabelle already carry position information. …
- 9:27 AM Ticket #92 (Attempt recovery from XML parse errors in PGIP main loop) created by
- Isabelle exits in case of erroneous XML input. It could be made more …
Mar 2, 2007:
- 11:38 PM Ticket #91 (PGML: add markup for subscript, superscript, bold, ...) created by
- PGML does not have this markup. Subscript and superscript, at least, …
Feb 28, 2007:
- 1:52 PM Ticket #90 (Folding Improvements) created by
- Some desirable folding improvements are: 1. Check heuristic for …
- 1:40 PM Ticket #89 (Remove tabs from Isabelle source files (theories, at least)) created by
- The default tab width in Emacs is 8, in Eclipse it is 4. This messes …
Feb 27, 2007:
- 9:05 PM Ticket #88 (Buffer invisibility spec bug with Emacs 22) created by
- [Reported by Michaël Cadilhac] I'm an Emacs22 user of Proof General, …
- 8:32 PM Ticket #87 (Add support for indentation in proof script editor) created by
- Indentation can be controlled by either or both of: * …
- 1:39 PM Ticket #86 (Fix parse edit offset) created by
- Editing document sets the parse edit offset, the position from which …
- 1:37 PM Ticket #85 (Outline view improvements) created by
- Some possible enhancements to the outline view: 1. fix hiding of …
- 1:13 PM Ticket #78 (Preferences: support dynamically computed defaults) closed by
- fixed: I've now added a simpler mechanism for allowing OS-specific preference …
- 12:54 PM Ticket #36 (Split stream for console into input/output and give input a different ...) closed by
- fixed: Above comment seems inaccurate:
org.eclipse.ui.console.IOConsole… - 10:30 AM Ticket #84 (Remove double-quoted XML output from term display) created by
- The current Isabelle CVS version displays goals correctly but …
Note: See TracTimeline
for information about the timeline view.
