diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1998-11-18 13:44:37 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-18 13:44:37 +0000 |
commit | 091e673f1ab4b6588f63fb52f7dc5e965272d595 (patch) | |
tree | 319af1df1a1b83a82303108ddaaefb4a6a2e0356 /isa | |
parent | 322f80462f5f40c413a99d58d9baf2924b0fd170 (diff) |
Added isa-update function. Altered settings.
Diffstat (limited to 'isa')
-rw-r--r-- | isa/isa.el | 32 |
1 files changed, 28 insertions, 4 deletions
@@ -203,12 +203,17 @@ no regular or easily discernable structure." proof-shell-process-file (cons ;; Theory loader output and verbose update() output. - "Reading \"\\(.*\\)\"\\|Not reading \"\\(.*\\)\"" + "Proof General, this file is loaded: \"\\(.*\\)\"" (lambda (str) - (or (match-string 1 str) - (match-string 2 str)))) + (match-string 1 str))) + ;; \\|Not reading \"\\(.*\\)\" + ;; (lambda (str) + ;; (or (match-string 1 str) + ;; (match-string 2 str)))) ;; This is the output returned by a special command to ;; query Isabelle for outdated files. + ;; proof-shell-clear-included-files-regexp + ;; "Proof General, please clear your record of loaded files." proof-shell-retract-files-regexp "Proof General, you can unlock the file \"\\(.*\\)\"" proof-shell-compute-new-files-list 'isa-shell-compute-new-files-list @@ -227,7 +232,7 @@ no regular or easily discernable structure." ;;; So we rely on some hacked versions. ;;; -(defcustom isa-usethy-notopml-command "ProofGeneral.use_thy_and_update \"%s\";" +(defcustom isa-usethy-notopml-command "ProofGeneral.use_thy \"%s\";" "Sent to Isabelle to process theory for this ML file, and all ancestors." :type 'string :group 'isabelle-config) @@ -267,6 +272,25 @@ proof-shell-retract-files-regexp." (remove (file-truename (match-string 1 str)) proof-included-files-list)) +;; +;; Hack for update +;; + +(defcustom isa-update-command "ProofGeneral.update();" + "Sent to Isabelle to re-load theory files as needed and synchronise." + :type 'string + :group 'isabelle-config) + +(defun isa-update () + "Issue an update command to the Isabelle process. +This re-reads any theory files as necessary and resynchronizes +proof-included-files-list." + (interactive) + (save-some-buffers) + (proof-shell-insert isa-update-command)) + + + ;; |