diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-08 13:06:10 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1998-12-08 13:06:10 +0000 |
| commit | 25b0c93440b4a3dbe46b8abd81c99a78490913ef (patch) | |
| tree | 6345379f6aa956da936327dd583e46c613a4b206 /lego | |
| parent | 10b6051134193eef64cdb84e42b009bef3ad1863 (diff) | |
Added support for proof-shell-restart-cmd
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/lego/lego.el b/lego/lego.el index 30acd07e..47a72861 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -59,8 +59,13 @@ (cons 'insert "Imports done!")))) "Acknowledge end of processing import declarations.") -(defconst lego-process-config "Configure PrettyOn; Configure AnnotateOn;" - "Command to enable pretty printing of the LEGO process.") +(defconst lego-process-config + "Init XCC; Configure PrettyOn; Configure AnnotateOn;" + "Command to initialise the LEGO process. + +Initialises empty context and prepares XCC theory. +Enables pretty printing. +Activates extended printing routines required for Proof General.") (defconst lego-pretty-set-width "Configure PrettyWidth %s; " "Command to adjust the linewidth for pretty printing of the LEGO @@ -474,6 +479,7 @@ We assume that module identifiers coincide with file names." proof-shell-start-goals-regexp "\372 Start of Goals \373" proof-shell-end-goals-regexp "\372 End of Goals \373" proof-shell-init-cmd lego-process-config + proof-shell-restart-cmd lego-process-config proof-analyse-using-stack nil proof-shell-process-output-system-specific lego-shell-process-output lego-shell-current-line-width nil |