Summary of Changes for Proof General 2.2 from 2.1 ------------------------------------------------- Generic Changes --------------- * [XEmacs only] New function control-button1 (proof-mouse-track-insert) copies individual commands (highlighted regions) from an open proof. When a proof is closed, it behaves as mouse-track-insert (default XEmacs behaviour of control-button1). * New function C-c C-f (proof-find) to invoke some prover-specific mechanism to search for theories. * [XEmacs only] Toolbar has five new buttons (State, Context, Info, Command, Help) which invoke commands previously available on keys/menus. Also a new "Find" button for proof-find. * [XEmacs only] Toolbar enablers have been added. Buttons are automatically enabled or disabled as appropriate. This requires XEmacs 20.4 or better for reliable working. * Menus and keybindings have been reorganized. Now keybindings invoke same functions as toolbar. * Terminal string now automatically added to command for C-c C-v * Cleaned up example files so all demonstrate same theorem "conj_comms". Would be nice to add more theorems to compare scripts/proofs in different systems. Please send in example scripts! * Shorter buffer names for convenience. * Removed transparent gif (text logo) from splash screen because XEmacs can't display it nicely. * Documentation updates. Coq Changes ----------- * Set proof-{qed,save}-commands so the toolbar functions work. Isabelle and Isar Changes ------------------------- * Tweaks for input syntax. * Recognize goals of the old form val prems = goal ... Only in the developers' release ------------------------------- * Provisional instantiation of Proof General for Plastic (http://www.dur.ac.uk/CARG/plastic.html) by Paul Callaghan