aboutsummaryrefslogtreecommitdiff
path: root/isa
AgeCommit message (Collapse)Author
1999-11-12Display qed message in goals bufferDavid Aspinall
1999-11-11Next round of fixups for font-lock and x-symbol.David Aspinall
1999-11-11Extensive fixes for x-symbol and font-lock.David Aspinall
1999-11-10Removed unsociable key-bindings.David Aspinall
1999-11-09Fixes for x-symbol activation/deactivation stringsDavid Aspinall
1999-11-09Arrange for activate-scripting to not block for interactive calls.David Aspinall
1999-11-08Comments.David Aspinall
1999-11-08Typo.David Aspinall
1999-11-08Changed web page to official one.David Aspinall
Added x-symbol support (moved here from generic/proof-x-symbol)
1999-10-29improved proof-shell-error-regexp;Makarius Wenzel
1999-10-27isa-update-thy-only: 'try' option;Makarius Wenzel
1999-10-26ProofGeneral.inform_file_processed/retracted;Makarius Wenzel
improved proof-shell-compute-new-files-list (more robust);
1999-10-26tuned proof-shell-error-regexp;Makarius Wenzel
1999-10-26isa-keywords-save: removed "result";Makarius Wenzel
isa-keywords-commands: added "ProofGeneral.repeat_undo"; added isa-keywords-proof-commands; added isa-verbatim;
1999-10-22update by DvO;Makarius Wenzel
1999-10-21Changed name of proof-shell-cd-cmd for uniformity.David Aspinall
1999-10-20Add isa-shell-update-thy at the end of proof-activate-scripting-hook.David Aspinall
1999-10-19Added uncaught exception to error-regexpDavid Aspinall
1999-10-19Rename proof-mark-buffer-atomic->proof-complete-buffer-atomic.David Aspinall
1999-10-19Deactivate scripting before retracting a theory file. Fix for DvO's report.David Aspinall
1999-10-15WhitespaceDavid Aspinall
1999-10-15let PROOFGENERAL_ASSISTANTS control isa vs. isar selection;Makarius Wenzel
1999-10-06Fix for state-preserving-pDavid Aspinall
1999-10-06Made new command proof-cd to cd to the directory of the currentDavid Aspinall
buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly.
1999-10-06Turned off C-c C-l; fixed syntax for old result form; proof-showproof-command.David Aspinall
1999-10-06thy mode binding made to match with script modeDavid Aspinall
1999-10-01Renamed some configuration variables for uniformity, see CHANGES.David Aspinall
1999-09-30replaced isa-output-font-lock-terms by isa-output-font-lock-keywords-1;Makarius Wenzel
1999-09-30tuned isa-init-output-syntax-table;Makarius Wenzel
removed isa-binder-regexp (obsolete); remove isa-font-lock-terms; proper isa-output-font-lock-keywords-1;
1999-09-29Enabled hack for proof-shell-leave-annotations-in-outputDavid Aspinall
1999-09-23Added setting for proof-find-theorems-command.David Aspinall
1999-09-22tuned example according to Isabelle style-guide;Makarius Wenzel
1999-09-22improved (?) proof-shell-proof-completed-regexp;Makarius Wenzel
1999-09-21Fix for proof-shell-proof-completed-regexpDavid Aspinall
1999-09-21Adjusted proof-shell-proof-completed-regexp to match against whole ofDavid Aspinall
proofstate output including "No subgoals!" message. Now PG can correctly set the proof-shell-proof-completed flag.
1999-09-13Cleaned up example files so all demonstrate same theorem "conj_comms".David Aspinall
Would be nice to add more theorems to compare scripts in different systems.
1999-09-03added bind_thms;Makarius Wenzel
added no_qed; more tacticals; removed isa-tactics (didn't make much sense); isa-goal-command-regexp accomodates "val ... =" part;
1999-09-03usage: tell PROOFGENERAL_OPTIONS;Makarius Wenzel
-u true by default;
1999-08-29added ALLGOALS;Makarius Wenzel
1999-08-25added qed_spec_mp;Makarius Wenzel
1999-08-23Maintainer addressesDavid Aspinall
1999-08-23fixed comment;Makarius Wenzel
1999-08-23Added font-lock keywords and syntax table setup for buffers displayingDavid Aspinall
Isabelle output.
1999-08-23Improved syntax by copying from isar-syntax.el.David Aspinall
Begun on section for Isabelle output syntax.
1999-08-20Disabled binder regexp font lockingDavid Aspinall
1999-08-20eliminated superficial ';'s;Makarius Wenzel
1999-08-20update by DvO;Makarius Wenzel
1999-08-18proof-shell-start-goals-regexp: include \n;Makarius Wenzel
isa-init-syntax-table moved to isa-syntax.el; improved isa-update-thy-only;
1999-08-18isa-init-syntax-table moved here from isa.el;Makarius Wenzel
1999-08-18replaced 'ProofGeneral' by 'Proof General';Makarius Wenzel