Timeline
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 …
Feb 25, 2007:
- 1:49 PM Ticket #83 (Fix script parsing to produce reliable and speedy <parseresult> outputs) created by
- See Pure/ProofGeneral?/parsing.ML. This is an absolutely essential …
- 1:12 PM Ticket #82 (Isabelle symbols: harmonise Isabelle.sym, x-symbol-isabelle.el and ...) created by
- * Isabelle.sym should be a superset of x-symbol-isabelle.el and …
- 1:03 PM Ticket #81 (Investigate use of Computer Modern Unicode font) created by
- Computer Modern Unicode may give a more uniform (across platforms) …
- 12:56 PM Ticket #80 (Improve symbols/character display: allow superscript, subscript (and ...) created by
- X-Symbol in Proof General Emacs allows superscripting and subscripting …
- 12:34 PM Ticket #79 (Improve symbols: support table inclusions; add Mac and Windows overrides) created by
- Present Isabelle.sym file works well on Linux/Fedora? Core 6. We …
- 12:32 PM Ticket #78 (Preferences: support dynamically computed defaults) created by
- The preference mechanism should support dynamically computed defaults. …
Feb 24, 2007:
Feb 23, 2007:
- 1:14 PM Ticket #77 (Partitioning: fix for correct lexical syntax of Isar) created by
- Lexical syntax fixes required. We can fix these first in main Java …
Feb 22, 2007:
Feb 21, 2007:
- 12:54 PM Ticket #76 (Add Prove-As-You-Type option) created by
- This is an idea for an updated version of the "electric terminator" …
- 11:46 AM Ticket #75 (Proof Script Editor context menu improvements) created by
- The context menu (right-click) in the proof script editor needs some …
Feb 19, 2007:
- 1:55 PM AboutTrac created by
- 1:32 PM Ticket #74 (Coq: bug in electric terminator: typing '.' in comment causes comment ...) created by
- When I type a '.' within a comment, the comment is sent to Coq and …
Feb 17, 2007:
- 5:54 PM Ticket #63 (Improve symbols: fill out default table, add ascii-symbol completion) closed by
- fixed: Both of these added now. New Isabelle symbol table is: …
- 12:48 PM Ticket #73 (Enhancements for Proof Objects view) created by
- Some possible improvements to the Proof Objects view are: * Make …
Note: See TracTimeline
for information about the timeline view.
