From 1c7cc9e1525baf65117d814573c29d974614fe4b Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 25 May 2000 18:28:34 +0000 Subject: Patch for synchronization problem in Coq, perhaps others. --- lego/lego.el | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'lego') 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 -- cgit v1.2.3