proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
...
*	Tidy	David Aspinall	2000-06-27
\|
*	Extra note.	David Aspinall	2000-06-22
\|
*	proper function-menu (fume) setup;	Makarius Wenzel	2000-06-16
\|
*	Tuned x-symbol config, moved settings to isabelle-system.el	David Aspinall	2000-06-16
\|
*	Deleted files.	David Aspinall	2000-06-16
\|
*	Note to merge	David Aspinall	2000-06-15
\|
*	new indentation setup;	Makarius Wenzel	2000-06-10
\|
*	proof-shell-error-regexp;	Makarius Wenzel	2000-06-09
\|
*	new indentation setup;	Makarius Wenzel	2000-06-08
\| \| \| \|	completion-table: use isar-keywords-major;
*	new indentation setup;	Makarius Wenzel	2000-06-08
\|
*	isar-keywords-proof-open/close;	Makarius Wenzel	2000-06-08
\|
*	proper indentation;	Makarius Wenzel	2000-06-08
\|
*	Failed attempted hack to support ML files in isar mode (see comments in ↵	David Aspinall	2000-06-07
\| \| \| \|	isar-preprocessing).
*	Allowed ; to terminate a command by including it in regexp for cmdstart	David Aspinall	2000-06-06
\| \| \| \|	Added completion for Isar keywords and X-symbol token names.
*	isar-save-with-hole-regexp: proof-no-regexp;	Makarius Wenzel	2000-06-05
\|
*	proof-indent-commands-regexp: use proof-no-regexp;	Makarius Wenzel	2000-06-05
\| \| \| \| \|	isar-global-save-command-p: more robust wrt. empty prev span (malformed!?); isar-preprocessing: fixed terminator regexp;
*	Removed defunct comments	David Aspinall	2000-06-05
\|
*	Temporary bug fix to solve nil span error message	David Aspinall	2000-06-05
\|
*	replaced isar-verbatim by isabelle-verbatim;	Makarius Wenzel	2000-06-04
\| \| \| \|	added isar-strip-terminators;
*	updated;	Makarius Wenzel	2000-06-04
\|
*	replaced isar-verbatim by isabelle-verbatim;	Makarius Wenzel	2000-06-04
\| \| \| \|	fixed output syntax table;
*	{ } are back;	Makarius Wenzel	2000-06-03
\|
*	Removed now spurious semicolons, 8-).	David Aspinall	2000-06-01
\|
*	Temporarily removed keywords { and } for new parsing mechanism	David Aspinall	2000-06-01
\|
*	Remove setting of proof-segment-up-to	David Aspinall	2000-06-01
\|
*	improved isar-goals-font-lock-keywords;	Makarius Wenzel	2000-05-30
\|
*	isar-preprocessing inserts final terminator if none there.	David Aspinall	2000-05-30
\| \| \| \| \|	Added (defpgdefault script-indent t) to turn on indentation. Added proof-script-command-start-regexp setting.
*	Tweak font lock exprs enough for Example.thy	David Aspinall	2000-05-29
\|
*	Font lock exprs for goals buffer like those in Isabelle	David Aspinall	2000-05-29
\|
*	Set settings format function before calculating initial command. Add hilit ↵	David Aspinall	2000-05-29
\| \| \| \|	for goals buffer
*	Use generic default setting mechanism now. Add isar-markup-ml here.	David Aspinall	2000-05-29
\|
*	Add -- isar -- tag to force mode, and comment to explain.	David Aspinall	2000-05-29
\|
*	isar-any-command-regexp;	Makarius Wenzel	2000-05-26
\|
*	isar-keywords-major;	Makarius Wenzel	2000-05-26
\|
*	Removed spurious code in isar-mode function.	David Aspinall	2000-05-25
\| \| \| \|	Removed defunct key binding of C-c C-l (Overriden with goto-end-of-locked).
*	Patch for synchronization problem in Coq, perhaps others.	David Aspinall	2000-05-25
\|
*	added "done";	Makarius Wenzel	2000-05-24
\|
*	replaced proof-ids-to-regexp by isar-ids-to-regexp, which admits	Makarius Wenzel	2000-05-22
\| \| \| \|	keywords to consist of a single non-word char as well (e.g. { });
*	replaced {{ }} by { };	Makarius Wenzel	2000-05-22
\|
*	isar-verbatim-regexp: include \n;	Makarius Wenzel	2000-05-19
\|
*	re-use isa/interface-setup.el rather than separate isar version;	Makarius Wenzel	2000-05-17
\|
*	Move setting of proof-shell-pre-interrupt-hook to isabelle-system.el	David Aspinall	2000-05-16
\|
*	Modification of proof-shell-init-cmd. Markus, please help...	David Aspinall	2000-05-12
\|
*	Load isabelle-system file shared with Isabelle Proof General.	David Aspinall	2000-05-11
\| \| \| \| \|	Add default settings to proof-shell-init-cmd. Add Isabelle menu to menubar.
*	Default to isa-mode or isar-mode according to first one invoked.	David Aspinall	2000-05-05
\|
*	isar-indent regexps moved to isar-syntax.el;	Makarius Wenzel	2000-04-25
\| \| \| \|	tuned comments;
*	removed unused isar-ids;	Makarius Wenzel	2000-04-25
\| \| \| \|	added isar-indent regexps (from isar.el);
*	removed "simpset" minor keyword;	Makarius Wenzel	2000-04-25
\|
*	added 'hide';	Makarius Wenzel	2000-04-17
\|
*	fixed proof-mode-for-goals;	Makarius Wenzel	2000-04-12
\|