Change log for PG Eclipse

This is the file CHANGE_LOG.txt from the Proof General plugin package ed.inf.proofgeneral.

 Eclipse Proof General -- Developers' Change Log
$Id: PGEclipseChangeLog.txt,v 1.2 2007/06/27 14:45:49 DavidAspinall Exp $
The bug list has been moved to BUG_LIST.txt.
The change log lists the most recent edits first.
This file has not been maintained since Nov 06: 
check CVS ChangeLog for commit messages instead.

See also wiki page which documents user-oriented fixes required:


2006 Nov 22 (DA)
- Repairs and reorganisation of locked script management.
- Remove writing to prefHelpContexts.xml.

2006 Nov 20
- Completed updates to Eclipse 3.2 compatibility

2006 Nov 01
- Massive reorganisation
  > Applied CVS $id$ headers to all files for better tracking
  > Moved all miscellaneous packages into a content-oriented
    package in the ed.inf.utils parent package.

2006 Oct 31
- Numerous small updates to use Java 1.5 code.
- Many updates to use Eclipse 3.2 code.
- Beginning packaging into ed.inf.util

2006 Oct 30
- New prover detection searches user's path for prover file
  > Much better feedback when prover is not available.
  > Avoid spurious warnings if prover gets fixed
- more general SessionManager changes
  > Type-checked much of this class
  > Lots of new documentation
- added ed.inf.util class
  > some general classes here
  > silly tabulation class imported from my attic
  > aiming to integrate relevant classes from 'winterstein' and 'heneveld'

2006 Oct 27
- Restructured documents some more.  Removed javadocs from repository.
- Added ant build file
  > so far targets are javadoc and tpwrapper, two relatively common tasks
- Modernised (for 3.2) the customswt package
- Improved feedback when prover is not available.

2006 Oct 23 (GD)
- Updated test theories for Isabelle 2006.

2006 Oct 19 (GD)
- restructured documents in root of repository.
- Performed initial testing.

2006 Oct 17,18 (DA)
- Added new proof script wizard and property page for proof scripts (currently spurious)
- Blast a pile of warnings: import (not really important) and static access (good to fix)
- Remove, not used/empty (unless Lucas/someone has tweaked version?)
- Some cleanups of markers: use platform marker classes (textmarker, taskmarker, problemmarker) and
  add priority and severity levels.  Get rid of annoying modal dialog for parse warnings.
- Workaround for 3.2 startup issue: PGColorProvider caused NullPointerException trying to get pref. store.
  Now seems to work without org.eclipse.runtime.compatibility. 
- Fix for editor activation
- Cleanups for packaging: use default named jar file (.) instead of proofgeneral.jar, document
  problem with plugin based product in devel-docs/howto/make-release.txt
- Tweaks to welcome page.
- Many more issues added to

2006 Oct 12,13 (DA)
- Move ProofGeneralPlugin to 3.2 API, try to replace org.eclipse.core.runtime.compatibility with org.eclipse.core.runtime
- Removed PGPlatformRunnable, I don't think this is wanted (unless it was for 
  Alex's standalone stuff -- but comments suggest it is broken anyway).
- Removed EclipseVersionCompatibility and inlined the fix

2006 Oct 07 (DA)
- Some simplifications to preference mechanism and updates for 3.2 API; 
  remove non-standard file attribute. More to do, see note at top of

2006 Oct 05 (DA)
- fix Help menu actions to open internal browser in editor window for wiki
- use automatically generated build version number qualifier
- rearrange and fix up icons (icons/star48.xpm should be moved to 
  icons/branding on product rebuild)

2006 Oct 03 (DA)
- bump version number to test update site
- add TODO.txt documenting priority fixes to get a more usable system

2006 Oct 02 (DA)
- more tweaks to packaging: renamed product here to avoid confusion
- user visible fixes documented in CHANGES.txt

2006 Oct 01 (DA), packaging tweaks and cleanups/moving in repostitory; 
                  more branding; attempts towards released version as 1.0.1.

- made update site:
  (update project and features are in CVS repository under eclipse/)
- manifest added for OSGi framework in Eclipse 3.2
- name change: this is "Proof General Eclipse" or PG Eclipse for short (no slash!)
- version numbers: use plugin version as main version number; elsewhere 1.0[.x]
- icon source files moved to icon-src; added redrawn star in various sizes, branding
- documents renamed devel-docs to make clear they're not for users
- content dir for package intro added (but no working intro yet)
- various defunct files removed, notes on bug fixes and bugs remaining
- my experience with this code is that real use is still very difficult because
  of too many glitches and bugs in the interface: we should work to erradicate them!  

2006 Sep 9 (AH)

MINOR fixes
- Added test to wrap HTML widget text in <html> tag with meta for using UTF-8
  (needed since we display unicode which is not usually the default in
  external browsers such as Mozilla)
- changed \<and> to be &, not && (since && didn't parse but & does)
- added extra space after replacements since \<exists>x. became EXx., not EX x.

2006 Aug 24 (DA), minor fixes for Eclipse 3.2

- EclipseVersionCompatibility: small change for 3.2 release version
- PGSourceViewier avoid null pointer exception when visiting file outside
- Fixes to imports (a couple of broken imports commented out)
- move pointers to old wiki to point to new wiki, remove some pointers
  for pages which haven't been written yet.  Other minor documentation
  changes  [I'm a bit dubious about hard-coding all these doc wiki links 
  in the application, it would be better to include snapshots here once 
  some documentation exists, with a single outside link.]

2006 Jan 2 (AH)

MINOR fixes
- Symbols will display as the shortcut if unicode is unavailable or unset;
  unset is useful for things like \<Colon> for types which is output by isabelle 
  but we'd rather show ::  ... and crazily, Isabelle doesn't recognise \<Colon>!
  I also removed the combination long arrows since they often don't line up;
  the right thing to do is use chars from Unicode Supplemental Arrows A range
  (eg U+27F9) but the Japanese font Y.OzFontN is the only free one I've found
  that includes it correctly; and unfortunatley the "Fixed" font includes a 
  crap version which my system picks up (I emailed the FreeSans developers to
  ask them to include it in a future release.)
- ProverKnowledge uses a list of names all pointing to same record;
  includes fully-qualified names and completion works with them, eg HOL.i<ctrl+space>;
  can refresh all local entries to get things like primrecs (needs manual command)
- changed colours to be like Emacs PG (if this is a problem, i apologise; it was
  *really* irritating me especially since it is difficult to read through red
  and other users also commented they didn't like it, so i thought it would be worth doing)

2005 Dec 19 (AH)

MINOR fixes
- fixed bug where editor scrolled to top on save (workaround, it rescrolls to where it was)
- SessionManager uses a list to track fired events (more efficient than launched threads and calling notifyAll,
  especially when lots of events generated/queued)
- added "\<bar>" as symbol
- SendCommandAction runs more in FG, so is faster
- improved Document scroll routine and optimised offset-update routines, so "next" and auto are faster;
  on "next", behaviour is to scroll to change but leave cursor where it was,
  unless cursor was inside commant; on "auto", behaviour is not to scroll or move cursor
  unless processing passes cursor location, in which both more with processing
  (can be a little unfamiliar at first, but i think this is desired behaviour)
- improved xml-repair so it is much faster

2005 Dec 14  (AH)

MAJOR fixes
- workaround for isabelle bug that it puts things like \<equiv> in XML output
  (gets replaced by \&lt;equiv&gt;); PG attempts to correct for unescaped xml chars <, >, and &
  (and it does a pretty good job, thanks to regex support in java!)
- fixed bug where parse results would get flummoxed when symbols were used;
  parse results are now reconciled modulo symbols, and it seems to work well now 
  even when symbols are on
- support for accessing a prover programmatically, ie without eclipse open (eg. testing, and AH feature wizard);
  see test/src/StandaloneProverExample

MINOR fixes (recent)

- content assist autocomplete proposals (Ctrl+Space) seemed to stop working; 
  needed action def id set in ProofScriptEditor
- Path for PG plugin wasn't always being found correctly, now it is (better at least)
- ProverKnowledge correctly combines lazy-load definitions with preloaded definitions;
  and it handles long method descriptions (eg "subst")
- Isabelle2005 changes
  - thms_of is hidden in PureThy, fixed access for ProverKnowledge
  - ProverState recognises handshake symbol events (doesn't do anything but no longer gives error)
- using .cvsignore files to filter out some files i have locally but aren't useful to others
- comments in plugin.xml and EclipseVersionCompatibility to aid with Eclipse 3.2 migration (if and when desired)

MISCELANEOUS:  these (very minor) changes were made in my codebase ages ago,
but I didn't merge them at the time (conflicts); i think dan also fixed some of these;

i include them here for the sake of completeness:
- used to get sluggish after lots of use, fixed inefficiency in 
   output view, seems better now
- clean up "confused proof" message (for unnamed lemmas, display lemma; 
   for bad state say incomplete); Dan also changed this
- prover knowledge messages are better
- prover knowledge no longer gets confused on unnamed lemmas
- prover knowledge will now report on all theorems of a given name, 
   not just the first
- PGProverAction has one more overridable post-init function
- fixed error where Display.async(SessionManager.unlockAll) was called after eclipse classloaders closed
- removed manifest .MF file; as this seems to prevent exporting plugin classes
- Ctrl+R still sometimes conflicts with "Run to line" (should be using contexts... maybe installed wrong?;
  seems fixed now, by whom I don't know)

2005 July 08  (Dan?)

   Some work done in the SessionManager package (startSession changed slightly).
   Changed the behaviour of ProverState.onUndo... methods to handle nested proofs.
   The symbol support is better in several ways.
See cvs comments for more details

1 jun 05, MINOR CHANGES (AH):
- added context/scope for key bindings (was causing error when added as plugin)
- fixed prover knowledge grab (changed as result of theory output change), also subst method is multiline (breaks)

9 may 05, AH

- changed Outline model to include collapsible subsections
- files can be changed after 'end'
- added "ProverStandalone" interface for using a Prover without loading Eclipse (requires basic Eclipse jars but not DLL's);
  see its main method for illustration
- fixed some queueing thread-sync problems, robust send/wait functionality in SendCommandResponseAction
- cleaned up display routines, mainly by dropping outdated display updates in OutputViews (must faster)
- ProverKnowledge learns about new items in current file, and gets tactic/method info

full change list:
- added ProverKnowledge for current theory items (using SendCommandResponseAction)
- refactored CommandQueued and CommandQueuedWithValues
- created ProverStandalone for running text-based commands
- improved new GetCommandResponseAction to allow ownership sessions
- prover knowledge parses theory in fg, then commands in bg once things are quiet
- ProverKnowledge gets updated as new items are parsed, including axioms and definitions
- ProverKnowledge updates the tooltip for any marker (could get confused on same-name markers)
- prover state model info gets set on success (except undo commands), added getLastResponse() method
- exceptions display more nicely, and accept a parameter for whether just to silently display the log view
- latest output view shows errors alongside state
- errors during send next and goto show in log, not in dialog, latest output is activated
- outline view refreshes better
- OutputViews update less often in big runs
- outline collapses more, into subsections; status shows currectly
- fixed undoall
- fixed bug where actions could get stuck on interruption
- fixed undo all (wouldn't retract theories properly)
- changed undo behaviour so as not to rely on scripting containers
- open definition on right click acts on current location
- info about active tactics
- don't switch to error view if:  either we show error dialogs or are in latest output view
- fixed many bad location exceptions
- ProverKnowledge loads info about active tactics (using print_methods (theory))
- hover looks for valid words (excluding parens and quotes), but autocomplete didn't (does now)
- some Isabelle versions use pgmltext elements (now recognised in ProverKnowledge)
- action set (menu and toolbar) only appears in PGPerspective
- interrupt sends killall -2 signal

2 may 05, -ah


- added live prover knowledge as tooltips
- fixed lots of parsing errors

minor bug fixes:

- Isabelle can occasionally give buggy XML (if sending complex ML commands with quotes and raw chars); 
  SessMgr used to wait forever trying to parse that, now it has shortcuts & errors, 
  it's also faster on incomplete xml
- commands used to go funny on error; now they always wait for a CmdProc to reset (even if there is a CmdCausedError)
- GetCommandResponseAction is now available, for sending a command in a background thread,
  when the TP is available, and waiting for output, behaving nicely on interrupt
  [use eg GCRA.getDefault().doCommand("ML {* thm \"sym\" *}"); ]
- ProverKnowledge gets a list of all axioms and theorems (takes about 1s, uses low-ish level ML)
- static option to use prover knowledge or not in ProofGeneralPlugin
- autocompletion includes prover knowledge items
- added tooltips/help for code completion proposals
- added html capabilities to tooltips (copied Eclipse's internal HTMLTextPresenter); help now also showed for auto-completion
- minor clean-ups in UndoAction, fixes in UndoAll where it got notified too many times
- now we send a CommandSucceeded event before the CommandProcessed if it succeeds
- now we don't update processed offset until command is processed without error
- goto sets the lock offset immediately
- PGTextHover word-finding now includes numbers
- if user has chosen a logic not for preferences, then updates preferences, 
  they didn't take effect until eclipse restart (fixed by propertyChange method in IsabellePrefsPage)
- tooltip/hover windows can update when the information is loaded (and the window is resized) (UpdateableHTMLTextPresenter)
- fixed error on click where there is no text; now just shows context menu without options
- OpenDefinition only shows in context menu if it is a known term
- clears privateListener on restart/shutdown
- fixed autoSymbolise error where it tried to go back before start of document
- ExternalLazyParser responds better to events (doesn't notify twice on error, responds to shutdown)
- events can take any object as cause
- cause gets set on outgoing events now, too
- ExternalPrivateListener now uses itself as the cause to listen to (it was responding to send command actions)
- interrupt first tries interrupting any paused active firing events
- on parses which cause errors, ExternalLazyParser now stores sensible responses
- GotoAction executes the parsed commands found when there is an error, and THEN throws the error
  (if the error is on a different line to goto target, or if goto was run on a single line)
- parse doc action (and outline view) also uses valid parse information located before an error
- parsing errors tell what line it happened on, can go there
- fixed error where wouldn't scroll if command-sent is run sent after command-processed
- parse all usually runs in bg thread now
- parse all takes ownership
- when parsing for next command, it tries one line, then 4, then 16, then whole doc
  (much faster then adding one line each time); but it's still slow (see separate bug)

2005 Apr 28 -- AH

minor changes:
- added startup monitor (WaitCommandAction), shows an error window if the prover doesn't start in 10s
- updates prover state if process quits unexpectedly (or is killed externally)
- stopSession can now run in background with stopSessionBg 
  (and does, on normal shutdown; also does restart in background on fresh session action)
- PGIPShutdown is sent on shutdown, for viewing and to reset the appropriate actions/buttons
- non-xml messages are handled a bit better, including !!! warnings
- StreamGobbler processes output within its thread (was slower, in the display thread)
- all PGIPEvents now get a cause set (it was only a few, done in SM.pgipEvent(XX))
- error dialogs (eg scripting exception) are now always on top 
  [was visually confusing] -- gets shell from ProofGeneralPlugin activeEditor now
- race issues with generation of CommandCausedErrorEvent (would sometimes happen after
  CommandProcessed, so commands couldn't know whether they succeeded); now always sent 
  after Ready and before CommandProcessed, but only if the error came from the prover;
  (or if the event is cancelled).  not sure if this is desired behaviour, but it is more
  sensible than the old way.  [see note in bug list about documenting/discussing this]
- choose logic params have been fixed some (also an error where it could become permanently disabled);
  still slightly hacked (see separate bug for that)

2005 Apr 24 -- AH

minor changes:
- Choose Tool allows specifying a PGPluginTool class (for quick and dirty extensions -- not included in code base, let me know if you want)
- EclipseMethods has a messagePromptDialog method which prompts for a string
- qUndo sends the cause

2005 Apr 20 -- AH

- event firing model is synchronized to preserve order
- dialog and menu option to select logics (ChooseLogic...) and CWD
- uses a thread pool, kills unusued threads on stopSession
- scrolls in window on next and undo (see ProofGeneralPlugin.SCROLL_ON_NEXT_COMMAND)
- actions are properly synced with prover and each other (ie goto now works)

minor changes:
- comments are now stepped through individually (see ProofGeneral.STEP_COMMENTS)
- undoitem wasn't recognised in my code (set to use ProofGeneral.undo as spurious command, incl on lit comments); see ProofGeneralPlugin.SEND_OLD_STYLE_UNDO
- static instance avail of ProofGeneral and PreferenceStore, for use outside Eclipse
- markers (eg theory/lemma) caused eclipse errors (shown in log), changed so id is recorded just as pgmarker/theorem/etc 
  (the is prepended automatically), and set super type of pgmarker to be core resources marker
- support in pgip2html.Converter for text conversion (partial, should live elsewhere :);
  also dodgy attempt to clean up escaped XML (probably can be removed)
- lots of places, UI code switched to run in UI thread
- Session Log and Latest Output perspective names were reversed in their ShowXXX classes
- got rid of "retract script" message on shutting down
- force switch message no longer displayed on shutdown (PGPlugin has better isShuttingDown method)
- ActivateScriptAction close now has boolean semantics (instead of throwing an error)
- when disposing an editor and calling ActivateScriptAction--retract, the document was not passed, so the new editor not the old was being used!
- scripting in a new file when an old is active is a bit smarter 
  about checking whether old really is active (eg okay to swap if finished or not started);
  activeCheck does this
- session log wasn't getting all its info [setText call in wrong thread, and data gets lost by different threads]
- non-xml messages ruined state, eg. 'Warning -- increasing stack'; now they are displayed and discarded
- parser checks if command avail fast; also, better error checking
- external lazy parser would deadlock on interrupt, then resumes when we don't want it to; now it catches CommandCausedError
- parsing was off by one sometimes; fixed so Parser doesn't ignore ' and " chars (which was causing this error)
- session manager now generates an object for prover commands (CommandQueued, containing DocElement and cause)
  with preFire and postFire methods called before relevant events fired
  (eg for setting temporary a privateListener setting, better than setting static field in sm)
- session manager now uses seq/refSeq lookup activeCommandLookup to find commands (and other minor queueing/syncing changes)
- quick clicks (eg Next Next) messed up communications, now PGAction implements a run-singly option, waits for responses
- toolbar buttons can now be enabled (at least after their first use they can be)
- new enablement mechanism for PGAction, based on prover ownership, other items
- allows setting a single prover owner in session manager (strongly recommended to use this in new methods)
- sends a "prover clear" message when queues are all empty, prover not busy, and prover not owned
  (used to update enablement of buttons)
- sends InternalEvent.ProverClear after it has all other PGIPEvents have fired
- "goto" (undoAll, sendAll) was screwy; now it works (proper command syncing)  [may still be the odd error, but not usu fatal ??]
- PGProverAction sets a constant value for the document within a single command run
Topic revision: r2 - 27 Jun 2007 - 14:45:49 - DavidAspinall
This site is powered by the TWiki collaboration platformCopyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback
This Wiki uses Cookies