diff options
| -rw-r--r-- | generic/proof-config.el | 38 | ||||
| -rw-r--r-- | generic/proof-shell.el | 40 | ||||
| -rw-r--r-- | isa/isa.el | 6 | ||||
| -rw-r--r-- | isar/isar.el | 7 | ||||
| -rw-r--r-- | lego/lego.el | 4 |
5 files changed, 57 insertions, 38 deletions
diff --git a/generic/proof-config.el b/generic/proof-config.el index 10b539a7..302852dc 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -29,7 +29,7 @@ ;; 6. Goals buffer configuration ;; 7. Splash screen settings ;; 8. X-Symbol support -;; 9. Prover specific settings +;; 9. Prover specific settings [NEW in 3.2 -- using new mechanism] ;; 10. Global constants ;; ;; The user options don't need to be set on a per-prover basis, @@ -1169,19 +1169,28 @@ group. This allows different proof assistants to coexist :type 'string :group 'proof-shell) -;; -;; FIXME: perhaps we should have pre-sync-init and -;; post-sync-init commands? -;; +(defcustom proof-shell-pre-sync-init-cmd nil + "The command for configuring the proof process to gain synchronization. +This command is sent before Proof General's synchronization +mechanism is engaged, to allow customization inside the process +to help gain syncrhonization (e.g. engaging special markup). + +It is better to configure the proof assistant for this purpose +via command line options if possible, in which case this variable +does not need to be set. + +See also `proof-shell-init-cmd'." + :type '(choice string (const nil)) + :group 'proof-shell) + (defcustom proof-shell-init-cmd "" "The command for initially configuring the proof process. -This command is sent to the process as soon as it starts up, -perhaps in order to configure it for Proof General or to -print a welcome message. -Note that it is sent before Proof General's synchronization -mechanism is engaged (in case the command engages it). It -is better to configure the proof assistant via command -line options if possible." +This command is sent to the process as soon as syncrhonization is gained +(when an annotated prompt is first recognized). It can be used to configure +the proof assistant in some way, or print a welcome message +(since output before the first prompt is discarded). + +See also `proof-shell-pre-sync-init-cmd'." :type '(choice string (const nil)) :group 'proof-shell) @@ -1818,7 +1827,6 @@ Proof General." (match-end 0)) nil "(C) LFCS, University of Edinburgh, 2000." - "D. Aspinall, H. Goguen, T. Kleymann, D. Sequiera" nil nil " Please send problems and suggestions to proofgen@dcs.ed.ac.uk, @@ -1989,13 +1997,13 @@ for prover specific settings." (proof-defasscustom menu-entries nil "Extra entries for proof assistant specific menu. -A list of menu items [NAME CALLBACK ...]. See the documentation +A list of menu items [NAME CALLBACK ENABLER ...]. See the documentation of `easy-menu-define' for more details." :type 'sexp) (proof-defasscustom help-menu-entries nil "Extra entries for help submenu for proof assistant specific help menu. -A list of menu items [NAME CALLBACK ...]. See the documentation +A list of menu items [NAME CALLBACK ENABLER ...]. See the documentation of `easy-menu-define' for more details." :type 'sexp) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 2452d78d..8cd93f17 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1043,11 +1043,12 @@ proof-shell-exec-loop, to process the next item." (insert string) - ;; Advance the proof-marker. This means that any output received - ;; up til now but not processed by the proof-shell-filter will be - ;; lost! We must be careful to synchronize with the process - ;; before using proof-shell-insert. - (set-marker proof-marker (point)) + ;; Advance the proof-marker, if synchronization has been gained. + ;; A null marker position indicates that synchronization is not + ;; yet gained. (NB: Any output received before syncrhonization is + ;; gained is ignored!) + (unless (null (marker-position proof-marker)) + (set-marker proof-marker (point))) ;; FIXME: possible improvement. Make for post 3.0 releases ;; in case of problems. @@ -1449,7 +1450,8 @@ This is a subroutine of proof-shell-filter." (let ((pt (point)) (end t) lastend start) (goto-char (marker-position proof-shell-urgent-message-scanner)) (while (and end - (re-search-forward proof-shell-eager-annotation-start nil 'end)) + (re-search-forward proof-shell-eager-annotation-start + nil 'end)) (setq start (match-beginning 0)) (if (setq end (re-search-forward proof-shell-eager-annotation-end nil t)) @@ -1580,7 +1582,9 @@ however, are always processed; hence their name)." (progn (set-marker proof-marker (point)) ;; The first time a prompt is seen we ignore any - ;; output that occured before it. Process the + ;; output that occured before it, assuming that + ;; corresponds to uninteresting startup messages. + ;; We process the ;; action list to remove the first item if need ;; be (proof-shell-init-cmd sent if ;; proof-shell-config-done). @@ -1623,11 +1627,11 @@ however, are always processed; hence their name)." proof-shell-annotated-prompt-regexp nil t) (progn (backward-char (- (match-end 0) (match-beginning 0))) - ;; FIXME: decoding x-symbols here is perhaps a bit + ;; NB: decoding x-symbols here is perhaps a bit ;; expensive; moreover it leads to problems ;; processing special characters as annotations ;; later on. So no fontify or decode. - ;; (proof-fontify-region startpos (point)) + ;; (proof-fontify-region startpos (point)) (setq string (buffer-substring startpos (point))) (goto-char (point-max)) (proof-shell-filter-process-output string)))) @@ -1883,13 +1887,19 @@ processing." (add-hook 'kill-buffer-hook 'proof-shell-kill-function t t) (set-process-sentinel proc 'proof-shell-bail-out) - ;; Flush pending output from startup - ;; (it gets hidden from the user) - (accept-process-output proc 1) + ;; Pre-sync initialization command. This is necessary + ;; for proof assistants which change their output modes + ;; only after some initializations. + (if proof-shell-pre-sync-init-cmd + (proof-shell-insert proof-shell-pre-sync-init-cmd 'init-cmd)) - ;; Send intitialization command and wait for it to be - ;; processed. Also ensure that proof-action-list is - ;; initialised. + ;; Flush pending output from startup (it gets hidden from the user) + ;; while waiting for the prompt to appear + (while (null (marker-position proof-marker)) + (accept-process-output proc 1)) + + ;; Send main intitialization command and wait for it to be + ;; processed. Also ensure that proof-action-list is initialised. (setq proof-action-list nil) (if proof-shell-init-cmd (proof-shell-invisible-command proof-shell-init-cmd t)) @@ -182,11 +182,11 @@ and script mode." ;; FIXME: temporary hack for almost enabling/disabling printing. ;; Also for setting default values. + proof-shell-pre-sync-init-cmd "ProofGeneral.init false;" proof-shell-init-cmd (concat (isabelle-set-default-cmd) - "val pg_saved_gl = ref (!goals_limit); fun proofgeneral_enable_pr () = goals_limit:= !pg_saved_gl; fun proofgeneral_disable_pr() = (pg_saved_gl := (if (!goals_limit)>0 then !goals_limit else !pg_saved_gl); goals_limit := 0); ProofGeneral.init false;") + "val pg_saved_gl = ref (!goals_limit); fun proofgeneral_enable_pr () = goals_limit:= !pg_saved_gl; fun proofgeneral_disable_pr() = (pg_saved_gl := (if (!goals_limit)>0 then !goals_limit else !pg_saved_gl); goals_limit := 0);") ; FIXME improved version for Isabelle99-1: - ;proof-shell-init-cmd (concat (isabelle-set-default-cmd) - ; "ProofGeneral.init false;") + ;proof-shell-init-cmd (isabelle-set-default-cmd) proof-shell-restart-cmd "ProofGeneral.isa_restart();" proof-shell-quit-cmd "quit();" diff --git a/isar/isar.el b/isar/isar.el index 408f6628..afc4dcc9 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -275,11 +275,8 @@ ;; initial command configures Isabelle/Isar by modifying print ;; functions, restoring settings saved by Proof General, etc. - proof-shell-init-cmd (concat - (isar-verbatim - "ProofGeneral.init true;") - "\n" - (isabelle-set-default-cmd)) + proof-shell-pre-sync-init-cmd (isar-verbatim "ProofGeneral.init true;") + proof-shell-init-cmd (isabelle-set-default-cmd) proof-shell-restart-cmd "ProofGeneral.restart;" proof-shell-quit-cmd (isar-verbatim "quit();") 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 |