proof-general - Emacs interface for proof assistants

	Commit message (Collapse)	Author	Age
*	Add proof-forget-id command and make top_thm discard the goalstack.	David Aspinall	2012-02-08
\|
*	Improve handling of undo, implementing pg_kill and pg_undo.	David Aspinall	2012-02-08
\|
*	More progress with Prooftree. Basic trees produced. Undoing needs work.	David Aspinall	2012-02-08
\|
*	Adjust global state idea, it is supposed to count down as well as up...	David Aspinall	2012-02-08
\|
*	Bump year	David Aspinall	2012-02-07
\|
*	Get a little bit further with proof tree.	David Aspinall	2012-02-07
\|
*	Load pg_tactics, fix proof-undo-n-times-cmd again.	David Aspinall	2012-02-07
\|
*	Borrow syntax keywords from caml-mode if available. Typo in undo-n-times.	David Aspinall	2012-02-07
\|
*	Use right HOL system	David Aspinall	2012-02-07
\|
*	Attempt to rebind failwith, which fails, with...errors	David Aspinall	2012-02-07
\|
*	Fix compile	David Aspinall	2012-02-07
\|
*	New pseudo instances to help tool demonstrators in ocaml/ghci (in progress)	David Aspinall	2012-02-07
\|
*	Updated.	David Aspinall	2012-02-07
\|
*	Extend list of provers we compile for	David Aspinall	2012-02-07
\|
*	Pasto	David Aspinall	2012-02-07
\|
*	Start support for both plain and custom top levels (work in progress).	David Aspinall	2012-02-07
\|
*	Cleanup	David Aspinall	2012-02-07
\|
*	Set version tag for new release.	David Aspinall	2012-02-06
\|
*	Cleaning some code.	Pierre Courtieu	2012-02-01
\|
*	Quick fix of a regression introduced by my last commit. Looking for a	Pierre Courtieu	2012-02-01
\| \| \| \|	better fix.
*	Fixed command end recognition in presence of operators of the form .+	Pierre Courtieu	2012-02-01
\| \| \| \|	+. is not accepted yet.
*	make sure extra modes available	David Aspinall	2012-01-23
\|
*	Draft symbol handling	David Aspinall	2012-01-23
\|
*	Rename goalstate file for pg	David Aspinall	2012-01-20
\|
*	Rename file	David Aspinall	2012-01-20
\|
*	Hint about changing prompt	David Aspinall	2012-01-20
\|
*	Temporary commit to share file, this is work in progress for Prooftree	David Aspinall	2012-01-19
\|
*	Add file from Mark	David Aspinall	2012-01-19
\|
*	Patch needed temporarily to avoid rebuild of Prooftree	David Aspinall	2012-01-19
\|
*	Typo	David Aspinall	2012-01-19
\|
*	Update documentation	David Aspinall	2012-01-19
\|
*	Added some detail on the indentation limitation in the CHANGE.	Pierre Courtieu	2012-01-18
\|
*	Fixed a small bug in indentation (ter repetita). Bullets are indented	Pierre Courtieu	2012-01-18
\| \| \| \|	correctly provided that the precedence - > + > * is respected.
*	Fixed a small bug in indentation (bis repetita).	Pierre Courtieu	2012-01-18
\|
*	Fixed a small bug in indentation.	Pierre Courtieu	2012-01-18
\|
*	lower cpu utilization of splash screen, see Debian bug #642048	Hendrik Tews	2012-01-14
\|
*	Set version tag for new release.	David Aspinall	2012-01-12
\|
*	Fix typo, mention HOL Light	David Aspinall	2012-01-12
\|
*	Adjust license to CC-BY-SA-3	David Aspinall	2012-01-11
\|
*	Set version tag for new release.	David Aspinall	2012-01-10
\|
*	Tweak message and display model, in particular, make sure that when a	David Aspinall	2012-01-10
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	response appears above a goals output, the goals output is displayed second, so it is the one that remains visible to the user in the default 2-pane mode. This works with output like this in HOL Light: Warning: Free variables in goal: A, B val it : goalstack = 1 subgoal (1 total) ... and similar cases in Isabelle and Coq. The fix involves some ugly messing with the flags for clearing the response buffer (see `pg-response-maybe-erase'). This could surely be streamlined.
*	Note about make -j for parallel compilation	David Aspinall	2012-01-10
\|
*	Emphasise importance of Trac	David Aspinall	2012-01-10
\|
*	Mention critical Emacs bug which destroys characters in certain	David Aspinall	2012-01-10
\| \| \| \|	compiles of Emacs 23.2. See Trac#409.
*	Add documentation for proof-shell-trace-output-regexp (Trac #432) and	David Aspinall	2012-01-10
\| \| \| \|	proof-shell-interactive-prompt-regexp (ref Trac #430)
*	Support proof-shell-interactive-prompt-regexp, ref Trac #430	David Aspinall	2012-01-10
\|
*	Improve configuration for HOL Light. Allow goals display to be prefixed by ↵	David Aspinall	2012-01-09
\| \| \| \|	ignored junk (val it : goalstack =).
*	proof-shell-start-goals-regexp: shy match to avoid introducing match group	David Aspinall	2012-01-09
\|
*	proof-shell-end-goals-regexp doc: fix inaccuracy, goals always start	David Aspinall	2012-01-09
\| \| \| \|	at start of proof-shell-start-goals-regexp.
*	Make configuration settings. Tweak error regexp.	David Aspinall	2012-01-06
\|