diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-25 18:28:34 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-25 18:28:34 +0000 |
| commit | 1c7cc9e1525baf65117d814573c29d974614fe4b (patch) | |
| tree | 60dfaeb4f6f8b0c7602c7b6bf4ad743e57600abd /lego | |
| parent | 7b59d83391e45b11cd19081eab4096395d6c57b4 (diff) | |
Patch for synchronization problem in Coq, perhaps others.
Diffstat (limited to 'lego')
| -rw-r--r-- | lego/lego.el | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/lego/lego.el b/lego/lego.el index 02f2ada0..10577c7a 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -63,6 +63,9 @@ "Acknowledge end of processing import declarations.") (defconst lego-process-config + ;; da: I think "Configure AnnotateOn;" is only included here for + ;; safety since there is a bug in LEGO which turns it off + ;; inadvertently sometimes. "Init XCC; Configure PrettyOn; Configure AnnotateOn;" "Command to initialise the LEGO process. @@ -445,6 +448,7 @@ We assume that module identifiers coincide with file names." proof-shell-result-end "\372 End Pbp result \373" proof-shell-start-goals-regexp "\372 Start of Goals \373" proof-shell-end-goals-regexp "\372 End of Goals \373" + proof-shell-pre-sync-init-cmd "Configure AnnotateOn;" proof-shell-init-cmd lego-process-config proof-shell-restart-cmd lego-process-config proof-analyse-using-stack nil |