Experimental changes to queue several commands at once and to allow pre-processing of commands when they're queued from script

15 files changed, 275 insertions, 237 deletions

diff --git a/bin/proofgeneral b/bin/proofgeneral
index a661adaf..718e9d5f 100644
--- a/bin/proofgeneral
+++ b/bin/proofgeneral
@@ -20,7 +20,7 @@
 # NB: no trailing backslash here!
 # On Mac, maybe:
 # /Applications/Emacs.app/Contents/MacOS/Emacs/site-lisp/ProofGeneral
-PGHOMEDEFAULT=$HOME/ProofGeneral
+PGHOMEDEFAULT=/usr/share/emacs-snapshot/site-lisp/ProofGeneral
 
 NAME=`basename $0`
 
diff --git a/etc/development-tips.txt b/etc/development-tips.txt
index 066b98a0..d8b766cd 100644
--- a/etc/development-tips.txt
+++ b/etc/development-tips.txt
@@ -32,6 +32,18 @@ proof-assistant symbol (proof-ass), they will produce the wrong result
 be used to avoid this and optimise compilation.  Byte compiler also
 optimises some conditionals that appear constant, be wary.
 
+Finally, the compiler will warn over-eagerly (and ususally spuriously)
+about unknown functions.  Adding extra requires can get these to go
+away, but watch out for introducing cycles in the require graphs.
+
+Rough dependency graph:
+
+
+proof-autoloads -> 
+        pg-vars -> proof-site  -> pg-vars
+           
+
+
 
 Some Emacs Resources
 ====================
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index 76fb230d..9bbcc2ab 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -336,7 +336,8 @@ The prover command is processed via pg-pbrpm-run-command."
        (span-set-property span 'type 'pbp)
        (span-set-property span 'cmd command)
        (proof-start-queue (proof-unprocessed-begin) (point)
-			  (list (list span command 'proof-done-advancing))))))
+			  (list (list span (list command)
+				      'proof-done-advancing))))))
 
 ;;--------------------------------------------------------------------------;;
 ;; Click Informations extractors
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 94400d1a..7ceb0d66 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -34,7 +34,6 @@
 (declare-function pg-response-message "pg-response")
 (declare-function proof-segment-up-to "proof-script") 
 
-
 ;;; Code:
 (defalias 'pg-pgip-debug   'proof-debug)
 (defalias 'pg-pgip-error   'error)
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 798fb440..4db4e813 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -1,17 +1,17 @@
 ;;; proof-autoloads.el --- automatically extracted autoloads
 ;;
 ;;; Code:
-(if (featurep 'proof-autoloads) (error "Already loaded"))
 
+(if (featurep 'proof-autoloads) (error "Already loaded"))
+  
 (provide 'proof-autoloads)
 
-;;;***
 
 ;;;### (autoloads (bufhist-exit bufhist-init bufhist-mode) "bufhist"
-;;;;;;  "../lib/bufhist.el" (19110 10300))
+;;;;;;  "../lib/bufhist.el" (19109 19688))
 ;;; Generated autoloads from ../lib/bufhist.el
 
-(autoload 'bufhist-mode "bufhist" "\
+(autoload (quote bufhist-mode) "bufhist" "\
 Minor mode retaining an in-memory history of the buffer contents.
 
 Commands:\\<bufhist-minor-mode-map>
@@ -24,7 +24,7 @@ Commands:\\<bufhist-minor-mode-map>
 
 \(fn &optional ARG)" t nil)
 
-(autoload 'bufhist-init "bufhist" "\
+(autoload (quote bufhist-init) "bufhist" "\
 Initialise a ring history for the current buffer.
 The history will be read-only unless READWRITE is non-nil.
 For read-only histories, edits to the buffer switch to the latest version.
@@ -32,7 +32,7 @@ The size defaults to `bufhist-ring-size'.
 
 \(fn &optional READWRITE RINGSIZE)" t nil)
 
-(autoload 'bufhist-exit "bufhist" "\
+(autoload (quote bufhist-exit) "bufhist" "\
 Stop keeping ring history for current buffer.
 
 \(fn)" t nil)
@@ -41,15 +41,15 @@ Stop keeping ring history for current buffer.
 
 ;;;### (autoloads (holes-insert-and-expand holes-abbrev-complete
 ;;;;;;  holes-mode holes-set-make-active-hole) "holes" "../lib/holes.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19108 1539))
 ;;; Generated autoloads from ../lib/holes.el
 
-(autoload 'holes-set-make-active-hole "holes" "\
+(autoload (quote holes-set-make-active-hole) "holes" "\
 Make a new hole between START and END or at point, and make it active.
 
 \(fn &optional START END)" t nil)
 
-(autoload 'holes-mode "holes" "\
+(autoload (quote holes-mode) "holes" "\
 Toggle Holes minor mode.
 With arg, turn Outline minor mode on if arg is positive, off otherwise.
 
@@ -139,7 +139,7 @@ undoing on holes cannot make holes re-appear.
 
 \(fn &optional ARG)" t nil)
 
-(autoload 'holes-abbrev-complete "holes" "\
+(autoload (quote holes-abbrev-complete) "holes" "\
 Complete abbrev by putting holes and indenting.
 Moves point at beginning of expanded text.  Put this function as
 call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will
@@ -147,7 +147,7 @@ become holes.
 
 \(fn)" nil nil)
 
-(autoload 'holes-insert-and-expand "holes" "\
+(autoload (quote holes-insert-and-expand) "holes" "\
 Insert S, expand it and replace #s and @{]s by holes.
 
 \(fn S)" nil nil)
@@ -155,10 +155,10 @@ Insert S, expand it and replace #s and @{]s by holes.
 ;;;***
 
 ;;;### (autoloads (maths-menu-mode) "maths-menu" "../lib/maths-menu.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19106 28183))
 ;;; Generated autoloads from ../lib/maths-menu.el
 
-(autoload 'maths-menu-mode "maths-menu" "\
+(autoload (quote maths-menu-mode) "maths-menu" "\
 Install a menu for entering mathematical characters.
 Uses window system menus only when they can display multilingual text.
 Otherwise the menu-bar item activates the text-mode menu system.
@@ -169,16 +169,16 @@ This mode is only useful with a font which can display the maths repertoire.
 ;;;***
 
 ;;;### (autoloads (proof-associated-windows proof-associated-buffers)
-;;;;;;  "pg-assoc" "pg-assoc.el" (19110 10300))
+;;;;;;  "pg-assoc" "pg-assoc.el" (19113 30030))
 ;;; Generated autoloads from pg-assoc.el
 
-(autoload 'proof-associated-buffers "pg-assoc" "\
+(autoload (quote proof-associated-buffers) "pg-assoc" "\
 Return a list of the associated buffers.
 Some may be dead/nil.
 
 \(fn)" nil nil)
 
-(autoload 'proof-associated-windows "pg-assoc" "\
+(autoload (quote proof-associated-windows) "pg-assoc" "\
 Return a list of the associated buffers windows.
 Dead or nil buffers are not represented in the list.
 
@@ -187,10 +187,10 @@ Dead or nil buffers are not represented in the list.
 ;;;***
 
 ;;;### (autoloads (proof-goals-config-done) "pg-goals" "pg-goals.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19113 30030))
 ;;; Generated autoloads from pg-goals.el
 
-(autoload 'proof-goals-config-done "pg-goals" "\
+(autoload (quote proof-goals-config-done) "pg-goals" "\
 Initialise the goals buffer after the child has been configured.
 
 \(fn)" nil nil)
@@ -198,7 +198,7 @@ Initialise the goals buffer after the child has been configured.
 ;;;***
 
 ;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;;  "pg-pgip" "pg-pgip.el" (19110 13559))
+;;;;;;  "pg-pgip" "pg-pgip.el" (19113 32911))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload (quote pg-pgip-process-packet) "pg-pgip" "\
@@ -222,7 +222,7 @@ Send an <askprefs> message to the prover.
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
 ;;;;;;  pg-response-message pg-response-display-with-face pg-response-maybe-erase
 ;;;;;;  proof-response-config-done proof-response-mode) "pg-response"
-;;;;;;  "pg-response.el" (19112 23312))
+;;;;;;  "pg-response.el" (19113 30031))
 ;;; Generated autoloads from pg-response.el
 
 (autoload (quote proof-response-mode) "pg-response" "\
@@ -279,10 +279,10 @@ See `pg-next-error-regexp'.
 ;;;***
 
 ;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19106 28181))
 ;;; Generated autoloads from pg-thymodes.el
 
-(autoload 'pg-defthymode "pg-thymodes" "\
+(autoload (quote pg-defthymode) "pg-thymodes" "\
 Define a Proof General mode for theory files.
 Mode name is SYM-mode, named NAMED.  BODY is the body of a setq and
 can define a number of variables for the mode, viz:
@@ -306,76 +306,76 @@ All of these settings are optional.
 ;;;;;;  pg-response-buffers-hint pg-slow-fontify-tracing-hint proof-electric-terminator-enable
 ;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
 ;;;;;;  proof-goto-point proof-script-new-command-advance) "pg-user"
-;;;;;;  "pg-user.el" (19110 10300))
+;;;;;;  "pg-user.el" (19113 33162))
 ;;; Generated autoloads from pg-user.el
 
-(autoload 'proof-script-new-command-advance "pg-user" "\
+(autoload (quote proof-script-new-command-advance) "pg-user" "\
 Move point to a nice position for a new command.
 Assumes that point is at the end of a command.
 
 \(fn)" t nil)
 
-(autoload 'proof-goto-point "pg-user" "\
+(autoload (quote proof-goto-point) "pg-user" "\
 Assert or retract to the command at current position.
 Calls `proof-assert-until-point' or `proof-retract-until-point' as
 appropriate.
 
 \(fn)" t nil)
 
-(autoload 'proof-define-assistant-command "pg-user" "\
+(autoload (quote proof-define-assistant-command) "pg-user" "\
 Define FN (docstring DOC) to send BODY to prover, based on CMDVAR.
 BODY defaults to CMDVAR, a variable.
 
 \(fn FN DOC CMDVAR &optional BODY)" nil (quote macro))
 
-(autoload 'proof-define-assistant-command-witharg "pg-user" "\
+(autoload (quote proof-define-assistant-command-witharg) "pg-user" "\
 Define command FN to prompt for string CMDVAR to proof assistant.
 CMDVAR is a variable holding a function or string.  Automatically has history.
 
 \(fn FN DOC CMDVAR PROMPT &rest BODY)" nil (quote macro))
 
-(autoload 'proof-electric-terminator-enable "pg-user" "\
+(autoload (quote proof-electric-terminator-enable) "pg-user" "\
 Make sure the modeline is updated to display new value for electric terminator.
 
 \(fn)" nil nil)
 
-(autoload 'pg-slow-fontify-tracing-hint "pg-user" "\
+(autoload (quote pg-slow-fontify-tracing-hint) "pg-user" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload 'pg-response-buffers-hint "pg-user" "\
+(autoload (quote pg-response-buffers-hint) "pg-user" "\
 Not documented
 
 \(fn &optional NEXTBUF)" nil nil)
 
-(autoload 'pg-jump-to-end-hint "pg-user" "\
+(autoload (quote pg-jump-to-end-hint) "pg-user" "\
 Not documented
 
 \(fn)" nil nil)
 
-(autoload 'pg-processing-complete-hint "pg-user" "\
+(autoload (quote pg-processing-complete-hint) "pg-user" "\
 Display hint for showing end of locked region or processing complete.
 
 \(fn)" nil nil)
 
-(autoload 'pg-next-error-hint "pg-user" "\
+(autoload (quote pg-next-error-hint) "pg-user" "\
 Display hint for locating error.
 
 \(fn)" nil nil)
 
-(autoload 'pg-hint "pg-user" "\
+(autoload (quote pg-hint) "pg-user" "\
 Display a hint HINTMSG in the minibuffer, if `pg-show-hints' is non-nil.
 The function `substitute-command-keys' is called on the argument.
 
 \(fn HINTMSG)" nil nil)
 
-(autoload 'proof-imenu-enable "pg-user" "\
+(autoload (quote proof-imenu-enable) "pg-user" "\
 Add or remove index menu.
 
 \(fn)" nil nil)
 
-(autoload 'pg-previous-matching-input-from-input "pg-user" "\
+(autoload (quote pg-previous-matching-input-from-input) "pg-user" "\
 Search backwards through input history for match for current input.
 \(Previous history elements are earlier commands.)
 With prefix argument N, search for Nth previous match.
@@ -383,7 +383,7 @@ If N is negative, search forwards for the -Nth following match.
 
 \(fn N)" t nil)
 
-(autoload 'pg-next-matching-input-from-input "pg-user" "\
+(autoload (quote pg-next-matching-input-from-input) "pg-user" "\
 Search forwards through input history for match for current input.
 \(Following history elements are more recent commands.)
 With prefix argument N, search for Nth following match.
@@ -391,32 +391,32 @@ If N is negative, search backwards for the -Nth previous match.
 
 \(fn N)" t nil)
 
-(autoload 'pg-add-to-input-history "pg-user" "\
+(autoload (quote pg-add-to-input-history) "pg-user" "\
 Maybe add CMD to the input history.
 CMD is only added to the input history if it is not a duplicate
 of the last item added.
 
 \(fn CMD)" nil nil)
 
-(autoload 'pg-remove-from-input-history "pg-user" "\
+(autoload (quote pg-remove-from-input-history) "pg-user" "\
 Maybe remove CMD from the end of the input history.
 This is called when the command is undone.  It's only
 removed if it matches the last item in the ring.
 
 \(fn CMD)" nil nil)
 
-(autoload 'pg-clear-input-ring "pg-user" "\
+(autoload (quote pg-clear-input-ring) "pg-user" "\
 Not documented
 
 \(fn)" nil nil)
 
 ;;;***
 
-;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19110
-;;;;;;  10300))
+;;;### (autoloads (pg-xml-parse-string) "pg-xml" "pg-xml.el" (19109
+;;;;;;  19687))
 ;;; Generated autoloads from pg-xml.el
 
-(autoload 'pg-xml-parse-string "pg-xml" "\
+(autoload (quote pg-xml-parse-string) "pg-xml" "\
 Parse string in ARG, same as pg-xml-parse-buffer.
 
 \(fn ARG)" nil nil)
@@ -424,17 +424,17 @@ Parse string in ARG, same as pg-xml-parse-buffer.
 ;;;***
 
 ;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies)
-;;;;;;  "proof-depends" "proof-depends.el" (19110 10300))
+;;;;;;  "proof-depends" "proof-depends.el" (19109 19687))
 ;;; Generated autoloads from proof-depends.el
 
-(autoload 'proof-depends-process-dependencies "proof-depends" "\
+(autoload (quote proof-depends-process-dependencies) "proof-depends" "\
 Process dependencies reported by prover, for NAME in span GSPAN.
 Called from `proof-done-advancing' when a save is processed and
 `proof-last-theorem-dependencies' is set.
 
 \(fn NAME GSPAN)" nil nil)
 
-(autoload 'proof-dependency-in-span-context-menu "proof-depends" "\
+(autoload (quote proof-dependency-in-span-context-menu) "proof-depends" "\
 Make a portion of a context-sensitive menu showing proof dependencies.
 
 \(fn SPAN)" nil nil)
@@ -442,10 +442,10 @@ Make a portion of a context-sensitive menu showing proof dependencies.
 ;;;***
 
 ;;;### (autoloads (proof-easy-config) "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19108 4440))
 ;;; Generated autoloads from proof-easy-config.el
 
-(autoload 'proof-easy-config "proof-easy-config" "\
+(autoload (quote proof-easy-config) "proof-easy-config" "\
 Configure Proof General for proof-assistant using BODY as a setq body.
 The symbol SYM and string name NAME must match those given in
 the `proof-assistant-table', which see.
@@ -455,10 +455,10 @@ the `proof-assistant-table', which see.
 ;;;***
 
 ;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19106 28181))
 ;;; Generated autoloads from proof-indent.el
 
-(autoload 'proof-indent-line "proof-indent" "\
+(autoload (quote proof-indent-line) "proof-indent" "\
 Indent current line of proof script, if indentation enabled.
 
 \(fn)" t nil)
@@ -466,16 +466,16 @@ Indent current line of proof script, if indentation enabled.
 ;;;***
 
 ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19110 10300))
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19113 32972))
 ;;; Generated autoloads from proof-maths-menu.el
 
-(autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
+(autoload (quote proof-maths-menu-set-global) "proof-maths-menu" "\
 Set global status of maths-menu mode for PG buffers to be FLAG.
 Turn on/off menu in all script buffers and ensure new buffers follow suit.
 
 \(fn FLAG)" nil nil)
 
-(autoload 'proof-maths-menu-enable "proof-maths-menu" "\
+(autoload (quote proof-maths-menu-enable) "proof-maths-menu" "\
 Turn on or off maths-menu mode in Proof General script buffer.
 This invokes `maths-menu-mode' to toggle the setting for the current
 buffer, and then sets PG's option for default to match.
@@ -487,8 +487,8 @@ in future if we have just activated it for this buffer.
 ;;;***
 
 ;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main
-;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19112
-;;;;;;  23313))
+;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19113
+;;;;;;  32986))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload (quote proof-menu-define-keys) "proof-menu" "\
@@ -514,15 +514,15 @@ Construct and return PG auxiliary menu used in non-scripting buffers.
 ;;;***
 
 ;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm"
-;;;;;;  "proof-mmm.el" (19110 10300))
+;;;;;;  "proof-mmm.el" (19113 30031))
 ;;; Generated autoloads from proof-mmm.el
 
-(autoload 'proof-mmm-set-global "proof-mmm" "\
+(autoload (quote proof-mmm-set-global) "proof-mmm" "\
 Set global status of MMM mode for PG buffers to be FLAG.
 
 \(fn FLAG)" nil nil)
 
-(autoload 'proof-mmm-enable "proof-mmm" "\
+(autoload (quote proof-mmm-enable) "proof-mmm" "\
 Turn on or off MMM mode in Proof General script buffer.
 This invokes `mmm-mode' to toggle the setting for the current
 buffer, and then sets PG's option for default to match.
@@ -537,7 +537,7 @@ in future if we have just activated it for this buffer.
 ;;;;;;  proof-insert-pbp-command proof-register-possibly-new-processed-file
 ;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
 ;;;;;;  proof-locked-end proof-unprocessed-begin proof-colour-locked)
-;;;;;;  "proof-script" "proof-script.el" (19112 23313))
+;;;;;;  "proof-script" "proof-script.el" (19113 32729))
 ;;; Generated autoloads from proof-script.el
 
 (autoload (quote proof-colour-locked) "proof-script" "\
@@ -621,7 +621,7 @@ finish setup which depends on specific proof assistant configuration.
 ;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
 ;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
 ;;;;;;  proof-shell-available-p proof-shell-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (19112 23489))
+;;;;;;  "proof-shell.el" (19113 32858))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload (quote proof-shell-ready-prover) "proof-shell" "\
@@ -643,7 +643,10 @@ No error messages.  Useful as menu or toolbar enabler.
 \(fn)" nil nil)
 
 (autoload (quote proof-shell-insert) "proof-shell" "\
-Insert STRING at the end of the proof shell, call `scomint-send-input'.
+Insert STRINGS at the end of the proof shell, call `scomint-send-input'.
+
+The ACTION argument is a symbol which is typically the name of a
+callback for when STRING has been processed.
 
 First we call `proof-shell-insert-hook'.  The arguments `action' and
 `scriptspan' may be examined by the hook to determine how to modify
@@ -653,32 +656,32 @@ the command actually sent to the shell.
 Note that the hook is not called for the empty (null) string
 or a carriage return.
 
-Then we strip `string' of carriage returns before inserting it
+Then we strip STRING of carriage returns before inserting it
 and updating `proof-marker' to point to the end of the newly
 inserted text.
 
 Do not use this function directly, or output will be lost.  It is only
-used in `proof-append-alist' when we start processing a queue, and in
+used in `proof-add-to-queue' when we start processing a queue, and in
 `proof-shell-exec-loop', to process the next item.
 
-\(fn STRING ACTION &optional SCRIPTSPAN)" nil nil)
+\(fn STRINGS ACTION &optional SCRIPTSPAN)" nil nil)
 
 (autoload (quote proof-start-queue) "proof-shell" "\
-Begin processing a queue of commands in ALIST.
+Begin processing a queue of commands in QUEUEITEMS.
 If START is non-nil, START and END are buffer positions in the
 active scripting buffer for the queue region.
 
 This function calls `proof-append-alist'.
 
-\(fn START END ALIST)" nil nil)
+\(fn START END QUEUEITEMS)" nil nil)
 
 (autoload (quote proof-extend-queue) "proof-shell" "\
-Extend the current queue with commands in ALIST, queue end END.
+Extend the current queue with QUEUEITEMS, queue end END.
 To make sense, the commands should correspond to processing actions
 for processing a region from (buffer-queue-or-locked-end) to END.
 The queue mode is set to 'advancing
 
-\(fn END ALIST)" nil nil)
+\(fn END QUEUEITEMS)" nil nil)
 
 (autoload (quote proof-shell-wait) "proof-shell" "\
 Busy wait for `proof-shell-busy' to become nil.
@@ -739,10 +742,10 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19109 19687))
 ;;; Generated autoloads from proof-site.el
 
-(autoload 'proof-ready-for-assistant "proof-site" "\
+(autoload (quote proof-ready-for-assistant) "proof-site" "\
 Configure PG for symbol ASSISTANTSYM, name ASSISTANT-NAME.
 If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 
@@ -751,16 +754,16 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 ;;;***
 
 ;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (19110 10300))
+;;;;;;  "proof-splash" "proof-splash.el" (19109 19687))
 ;;; Generated autoloads from proof-splash.el
 
-(autoload 'proof-splash-display-screen "proof-splash" "\
+(autoload (quote proof-splash-display-screen) "proof-splash" "\
 Save window config and display Proof General splash screen.
 If TIMEOUT is non-nil, arrange for a time-out to occur outside this function.
 
 \(fn &optional TIMEOUT)" t nil)
 
-(autoload 'proof-splash-message "proof-splash" "\
+(autoload (quote proof-splash-message) "proof-splash" "\
 Make sure the user gets welcomed one way or another.
 
 \(fn)" t nil)
@@ -768,7 +771,7 @@ Make sure the user gets welcomed one way or another.
 ;;;***
 
 ;;;### (autoloads (proof-splice-separator proof-format) "proof-syntax"
-;;;;;;  "proof-syntax.el" (19112 23313))
+;;;;;;  "proof-syntax.el" (19112 23159))
 ;;; Generated autoloads from proof-syntax.el
 
 (autoload (quote proof-format) "proof-syntax" "\
@@ -786,7 +789,7 @@ Splice SEP into list of STRINGS, ignoring nil entries.
 ;;;***
 
 ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (19112 23313))
+;;;;;;  "proof-toolbar" "proof-toolbar.el" (19113 30032))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload (quote proof-toolbar-setup) "proof-toolbar" "\
@@ -805,7 +808,7 @@ Menu made from the Proof General toolbar commands.
 ;;;***
 
 ;;;### (autoloads (proof-unicode-tokens-set-global proof-unicode-tokens-mode-if-enabled)
-;;;;;;  "proof-unicode-tokens" "proof-unicode-tokens.el" (19112 23355))
+;;;;;;  "proof-unicode-tokens" "proof-unicode-tokens.el" (19113 32888))
 ;;; Generated autoloads from proof-unicode-tokens.el
 
 (autoload (quote proof-unicode-tokens-mode-if-enabled) "proof-unicode-tokens" "\
@@ -822,7 +825,7 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit.
 ;;;***
 
 ;;;### (autoloads (defpacustom proof-defpacustom-fn) "proof-utils"
-;;;;;;  "proof-utils.el" (19112 23313))
+;;;;;;  "proof-utils.el" (19113 33137))
 ;;; Generated autoloads from proof-utils.el
 
 (autoload (quote proof-defpacustom-fn) "proof-utils" "\
@@ -845,10 +848,10 @@ evaluate can be provided instead.
 ;;;***
 
 ;;;### (autoloads (scomint-make scomint-make-in-buffer) "scomint"
-;;;;;;  "../lib/scomint.el" (19110 10300))
+;;;;;;  "../lib/scomint.el" (19113 32626))
 ;;; Generated autoloads from ../lib/scomint.el
 
-(autoload 'scomint-make-in-buffer "scomint" "\
+(autoload (quote scomint-make-in-buffer) "scomint" "\
 Make a Comint process NAME in BUFFER, running PROGRAM.
 If BUFFER is nil, it defaults to NAME surrounded by `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -861,7 +864,7 @@ If PROGRAM is a string, any more args are arguments to PROGRAM.
 
 \(fn NAME BUFFER PROGRAM &optional STARTFILE &rest SWITCHES)" nil nil)
 
-(autoload 'scomint-make "scomint" "\
+(autoload (quote scomint-make) "scomint" "\
 Make a Comint process NAME in a buffer, running PROGRAM.
 The name of the buffer is made by surrounding NAME with `*'s.
 PROGRAM should be either a string denoting an executable program to create
@@ -877,10 +880,10 @@ If PROGRAM is a string, any more args are arguments to PROGRAM.
 ;;;***
 
 ;;;### (autoloads (texi-docstring-magic) "texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19106 28184))
 ;;; Generated autoloads from ../lib/texi-docstring-magic.el
 
-(autoload 'texi-docstring-magic "texi-docstring-magic" "\
+(autoload (quote texi-docstring-magic) "texi-docstring-magic" "\
 Update all texi docstring magic annotations in buffer.
 With prefix arg, no errors on unknown symbols.  (This results in
 @def .. @end being deleted if not known).
@@ -890,10 +893,10 @@ With prefix arg, no errors on unknown symbols.  (This results in
 ;;;***
 
 ;;;### (autoloads (unicode-chars-list-chars) "unicode-chars" "../lib/unicode-chars.el"
-;;;;;;  (19110 10300))
+;;;;;;  (19106 44762))
 ;;; Generated autoloads from ../lib/unicode-chars.el
 
-(autoload 'unicode-chars-list-chars "unicode-chars" "\
+(autoload (quote unicode-chars-list-chars) "unicode-chars" "\
 Insert each Unicode character into a buffer.
 Lets you see which characters are available for literal display
 in your emacs font.
@@ -903,7 +906,7 @@ in your emacs font.
 ;;;***
 
 ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (19112 23313))
+;;;;;;  (19113 34045))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
 (autoload (quote unicode-tokens-encode-str) "unicode-tokens" "\
@@ -915,9 +918,9 @@ Return a unicode encoded version presentation of STR.
 
 ;;;### (autoloads nil nil ("../lib/local-vars-list.el" "../lib/pg-dev.el"
 ;;;;;;  "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
-;;;;;;  "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el"
-;;;;;;  "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-useropts.el"
-;;;;;;  "proof.el" "test.el") (19112 23608 594193))
+;;;;;;  "comptest.el" "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el"
+;;;;;;  "pg-vars.el" "proof-auxmodes.el" "proof-config.el" "proof-faces.el"
+;;;;;;  "proof-useropts.el" "proof.el") (19113 34166 685782))
 
 ;;;***
 
@@ -926,4 +929,5 @@ Return a unicode encoded version presentation of STR.
 ;; no-byte-compile: t
 ;; no-update-autoloads: t
 ;; End:
+
 ;;; proof-autoloads.el ends here
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 360581b9..e80ade04 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1662,10 +1662,19 @@ stripped of carriage returns before being sent.
 Example uses:
 LEGO uses this hook for setting the pretty printer width if
 the window width has changed;
-Plastic uses it to remove literate-style markup from `string'."
+Plastic uses it to remove literate-style markup from `string'.
+
+See also `proof-script-preprocess' which can munge text when
+it is added to the queue of commands."
   :type '(repeat function)
   :group 'proof-shell)
 
+(defcustom proof-script-preprocess nil
+  "Function to pre-process (SPAN STRING) taken from proof script."
+  :type 'function
+  :group 'proof-shell)
+  
+
 (defcustom proof-shell-handle-delayed-output-hook
   '(proof-pbp-focus-on-first-goal)
   "Hooks run after new output has been displayed in goals or response buffer."
diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el
index fdc1f7e0..4195a7dc 100644
--- a/generic/proof-maths-menu.el
+++ b/generic/proof-maths-menu.el
@@ -1,6 +1,6 @@
 ;; proof-maths-menu.el   Support for maths menu mode package
 ;;
-;; Copyright (C) 2007 LFCS Edinburgh / David Aspinall
+;; Copyright (C) 2007, 2009 LFCS Edinburgh / David Aspinall
 ;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 7cb5231e..a79b976a 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -21,6 +21,12 @@
     
 
 
+(eval-when-compile
+  (defvar proof-assistant-menu)	  ; defined by macro in proof-menu-define-specific
+  (defvar proof-mode-map))
+    
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
 ;;; Miscellaneous commands
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 38feb34a..94e677df 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1917,25 +1917,41 @@ This version is used when `proof-script-command-end-regexp' is set."
       ;; Return resulting list
       alist)))
 
-(defun proof-semis-to-vanillas (semis &optional callback-fn)
-  "Convert a sequence of terminator positions to a set of vanilla extents.
+(defun proof-semis-to-vanillas (semis)
+  "Create vanilla extents for SEMIS and a list for the queue.
 Proof terminator positions SEMIS has the form returned by
 the function `proof-segment-up-to'.  The argument list is destroyed.
-Set the callback to CALLBACK-FN or `proof-done-advancing' by default."
-  (let ((ct (proof-queue-or-locked-end))
-	(cb (or callback-fn 'proof-done-advancing))
-	span alist semi)
-    (dolist (semi (nreverse semis))
-      (setq span (span-make ct (nth 2 semi))
-	    ct (nth 2 semi))
-      (if (eq (car semi) 'cmd)
-	  (progn
-	    (span-set-property span 'type 'vanilla)
-	    (span-set-property span 'cmd (nth 1 semi))
-	    (setq alist (cons (list span (nth 1 semi) cb) alist)))
-	(span-set-property span 'type 'comment)
-	(setq alist
-	      (cons (list span nil cb) alist))))  ; was proof-no-command
+The callback in each queue element is `proof-done-advancing'.
+If `proof-script-preprocess' is set, call that function to construct
+the first element of the queue item."
+  (let ((start (proof-queue-or-locked-end))
+	(file  (or (buffer-file-name) (buffer-name)))
+	(cb    'proof-done-advancing)
+	span alist semi item end)
+    (setq semis (nreverse semis))
+    (save-match-data
+      (dolist (semi semis)
+	(setq end (nth 2 semi))
+	(setq span  (span-make start end))
+	(if (eq (car semi) 'cmd)
+	    (progn ;; command span
+	      (let* ((cmd  (nth 1 semi))
+		     (qcmd (if proof-script-preprocess
+			       (funcall proof-script-preprocess
+					file 
+					;; ignore spaces at start of command
+					(+ start (string-match "[^\t\n ]" cmd))
+					end
+					cmd)
+			     (list cmd))))
+		(span-set-property span 'type 'vanilla)
+		(span-set-property span 'cmd cmd)
+		(setq alist (cons (list span qcmd cb) alist))))
+	  ;; ignored text
+	  (span-set-property span 'type 'comment)
+	  (setq alist
+		(cons (list span nil cb) alist))) ; nil was `proof-no-command'
+	(setq start end)))
     (nreverse alist)))
 
 
@@ -2006,7 +2022,8 @@ SEMIS must be a non-empty list, in reverse order (last position first)."
     (span-set-property span 'type 'pbp)
     (span-set-property span 'cmd cmd)
     (proof-start-queue (proof-unprocessed-begin) (point)
-		       (list (list span cmd 'proof-done-advancing)))))
+		       (list (list span (list cmd) 
+				   'proof-done-advancing)))))
 
 ;;;###autoload
 (defun proof-insert-sendback-command (cmd)
@@ -2070,14 +2087,14 @@ others)."
   ;; State of scripting may have changed now
   (run-hooks 'proof-state-change-hook))
 
-(defun proof-setup-retract-action (start end proof-command delete-region)
+(defun proof-setup-retract-action (start end proof-commands delete-region)
   "Make span from START to END which corresponds to retraction.
 Returns retraction action destined for proof shell queue, and make span.
-Action holds PROOF-COMMAND and `proof-done-retracting' callback.
+Action holds PROOF-COMMANDS and `proof-done-retracting' callback.
 Span deletion property set to flag DELETE-REGION."
   (let ((span (span-make start end)))
     (span-set-property span 'delete-me delete-region)
-    (list (list span proof-command 'proof-done-retracting))))
+    (list (list span proof-commands 'proof-done-retracting))))
 
 
 (defun proof-last-goal-or-goalsave ()
@@ -2145,7 +2162,8 @@ up to the end of the locked region."
 	      (setq actions (proof-setup-retract-action
 			     start end
 			     (if (null span) nil ; was: proof-no-command
-			       (funcall proof-count-undos-fn span))
+			       ;; TODO: make proof-count-undos-fn return a list
+			       (list (funcall proof-count-undos-fn span)))
 			     delete-region)
 		    end start))
 	  ;; Otherwise, start the retraction by killing off the
@@ -2157,7 +2175,7 @@ up to the end of the locked region."
 	  (setq proof-nesting-depth (1- proof-nesting-depth))
 	  (setq actions
 		(proof-setup-retract-action (span-start span) end
-					    proof-kill-goal-command
+					    (list proof-kill-goal-command)
 						    delete-region)
 		end (span-start span))))
     ;; Check the start of the target span lies before the end
@@ -2174,7 +2192,8 @@ up to the end of the locked region."
 	      ;; the target span.
 	      (nconc actions (proof-setup-retract-action
 			      start end
-			      (funcall proof-find-and-forget-fn target)
+			      ;; TODO: make `proof-find-and-forget-fn' return a list
+			      (list (funcall proof-find-and-forget-fn target))
 			      delete-region))))
 
     (proof-start-queue (min start end) (proof-locked-end) actions)))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index cb40d0ca..b8def10b 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -36,10 +36,10 @@
   "Marker in proof shell buffer pointing to previous command input.")
 
 (defvar proof-action-list nil
-  "The main queue of things to do, containing spans commands and actions.
+  "The main queue of things to do: spans, commands and actions.
 The value is a list of lists of the form
 
-   (SPAN COMMAND ACTION [FLAGS])
+   (SPAN COMMANDS ACTION [FLAGS])
 
 which is the queue of things to do.  Flags are set for non-standard
 commands (out of script).  They may include
@@ -51,11 +51,11 @@ commands (out of script).  They may include
 If flags are non-empty, other interactive cues will be surpressed.
 \(E.g., printing help messages).
 
-See the functions `proof-start-queue' and `proof-exec-loop'.")
+See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
 
 ;; We record the last output from the prover and a flag indicating its
-;; type, as well as a previous ("delayed") version to display when the
-;; end of the queue is reached or an error or interrupt occurs.
+;; type, as well as a previous ("delayed") version for when the end
+;; of the queue is reached or an error or interrupt occurs.
 ;; 
 ;; See `proof-shell-last-output', `proof-shell-last-prompt' in
 ;; pg-vars.el
@@ -578,26 +578,22 @@ This is a subroutine of `proof-shell-handle-error'."
       (pg-response-maybe-erase t nil)
       (pg-response-display-with-face string append-face)))
 
-
-
 (defsubst proof-shell-strip-output-markup (string &optional push)
   "Strip output markup from STRING.
 Convenience function to call function `proof-shell-strip-output-markup'.
 Optional argument PUSH is ignored."
   (funcall proof-shell-strip-output-markup string))
 
-
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Processing error output
 ;;
 
-(defun proof-shell-handle-error-or-interrupt (flags)
+(defun proof-shell-handle-error-or-interrupt (err-or-int flags)
   "React on an error or interrupt message triggered by the prover.
 
-On entry, `proof-shell-last-output-kind' should be set to 'error
-or 'interrupt, which affects the action taken.
+The argument ERR-OR-INT should be set to 'error or 'interrupt
+which affects the action taken.
 
 For errors, we first flush unprocessed output (usually goals).
 The error message is the (usually) displayed in the response buffer.
@@ -611,7 +607,7 @@ Commands which are not part of regular script management (with
 non-empty flags) will not invoke any of this action."  ; PG4.0 change
   (unless (memq 'no-error-display flags)
     (cond
-     ((eq proof-shell-last-output-kind 'interrupt)
+     ((eq err-or-int 'interrupt)
       (pg-response-maybe-erase t t t) ; force cleaned now & next 
       (proof-shell-handle-error-output
        (if proof-shell-truncate-before-error proof-shell-interrupt-regexp)
@@ -626,8 +622,7 @@ non-empty flags) will not invoke any of this action."  ; PG4.0 change
        (if proof-shell-truncate-before-error proof-shell-error-regexp)
        'proof-error-face)
       (proof-display-and-keep-buffer proof-response-buffer)))
-    (proof-shell-error-or-interrupt-action
-     proof-shell-last-output-kind)))
+    (proof-shell-error-or-interrupt-action err-or-int)))
 
 (defun proof-shell-error-or-interrupt-action (err-or-int)
   (save-excursion
@@ -706,11 +701,11 @@ after a completed proof."
    ;; command with delayed output from this command to handle that!
    ((proof-re-search-forward-safe proof-shell-interrupt-regexp end t)
     (setq proof-shell-last-output-kind 'interrupt)
-    (proof-shell-handle-error-or-interrupt flags))
+    (proof-shell-handle-error-or-interrupt 'interrupt flags))
    
    ((proof-re-search-forward-safe proof-shell-error-regexp end t)
     (setq proof-shell-last-output-kind 'error)
-    (proof-shell-handle-error-or-interrupt flags))
+    (proof-shell-handle-error-or-interrupt 'error flags))
 
    ((proof-re-search-forward-safe proof-shell-result-start end t)
     ;; NB: usually the action list is empty, strange results likely if
@@ -786,8 +781,8 @@ the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*).
 ;;
 
 ;;;###autoload
-(defun proof-shell-insert (string action &optional scriptspan)
-  "Insert STRING at the end of the proof shell, call `scomint-send-input'.
+(defun proof-shell-insert (strings action &optional scriptspan)
+  "Insert STRINGS at the end of the proof shell, call `scomint-send-input'.
 
 The ACTION argument is a symbol which is typically the name of a
 callback for when STRING has been processed.
@@ -804,31 +799,33 @@ Then we strip STRING of carriage returns before inserting it
 and updating `proof-marker' to point to the end of the newly
 inserted text.
 
-Do not use this function directly, or output will be lost.  It is
-only used in `proof-append-alist' when we start processing a
-queue, and in `proof-shell-exec-loop', to process the next item."
-  ;(assert (stringp string) t "proof-shell-insert: expected string argument")
+Do not use this function directly, or output will be lost.  It is only
+used in `proof-add-to-queue' when we start processing a queue, and in
+`proof-shell-exec-loop', to process the next item."
+  (assert (listp strings) nil "proof-shell-insert: expected string argument")
 
   (with-current-buffer proof-shell-buffer
     (goto-char (point-max))
 
-    ;; Hook for munging `string' and other dirty hacks.
-    (run-hooks 'proof-shell-insert-hook)
+    ;; TEMP: next step: preprocess list of strings directly
+    (let ((string (apply 'concat strings))) 
+      ;; Hook for munging `string' and other dirty hacks.
+      (run-hooks 'proof-shell-insert-hook)
 
-    ;; Replace CRs from string with spaces to avoid spurious prompts.
-    (if proof-shell-strip-crs-from-input
-	(setq string (subst-char-in-string ?\n ?\  string t)))
+      ;; Replace CRs from string with spaces to avoid spurious prompts.
+      (if proof-shell-strip-crs-from-input
+	  (setq string (subst-char-in-string ?\n ?\  string t)))
 
-    (insert string)
+      (insert string)
 
-    ;; Advance the proof-marker, if synchronization has been gained.
-    ;; Null marker => no yet synced; output is ignored.
-    (unless (null (marker-position proof-marker))
-      (set-marker proof-marker (point)))
+      ;; Advance the proof-marker, if synchronization has been gained.
+      ;; Null marker => no yet synced; output is ignored.
+      (unless (null (marker-position proof-marker))
+	(set-marker proof-marker (point)))
 
-    (scomint-send-input)
+      (scomint-send-input)
 
-    (setq proof-shell-expecting-output t)))
+      (setq proof-shell-expecting-output t))))
 
 
 ;; ============================================================
@@ -840,8 +837,7 @@ queue, and in `proof-shell-exec-loop', to process the next item."
 (defun proof-shell-action-list-item (cmd callback &optional flags)
   "Return action list entry run CMD with callback CALLBACK and FLAGS.
 The queue entry does not refer to a span in the script buffer."
-  (append (list nil cmd callback) flags))
-
+  (append (list nil (list cmd) callback) flags))
 
 (defun proof-shell-set-silent (span)
   "Callback for `proof-shell-start-silent'.
@@ -867,17 +863,14 @@ track what happens in the proof queue."
    proof-shell-stop-silent-cmd
    'proof-shell-clear-silent))
 
-;; FIXME: could be macro for efficiency improvement in avoiding calculating num
-(defun proof-shell-should-be-silent (num)
+(defsubst proof-shell-should-be-silent (num)
   "Return non-nil if we must switch to silent mode, adding NUM entries to queue."
   (if (and (not proof-full-annotation)
 	   proof-shell-start-silent-cmd)
       (or proof-shell-silent	; already
-	  ;; NB: there is some question here over counting the
-	  ;; proof-action-list, since it could itself contain
-	  ;; silent-on/off commands which should be ignored for
-	  ;; counting, really... also makes cutting lists for advanced
-	  ;; queue processing more tricky.
+	  ;; NB: to be more accurate we should only count number
+	  ;; of scripting items in the list (not e.g. invisibles).
+	  ;; More efficient: keep track of size of queue as modified.
 	  (>= (+ num (length proof-action-list))
 	     proof-shell-silent-threshold))))
 
@@ -892,8 +885,8 @@ track what happens in the proof queue."
   "Insert ITEM from `proof-action-list' into the proof shell."
   (proof-shell-insert (nth 1 item) (nth 2 item) (nth 0 item)))
 
-(defun proof-append-alist (alist &optional queuemode)
-  "Chop off the vacuous prefix of the command queue ALIST and queue it.
+(defun proof-add-to-queue (queueitems &optional queuemode)
+  "Chop off the vacuous prefix of the QUEUEITEMS and queue them.
 For each item with a nil command at the head of the list, invoke its
 callback and remove it from the list.
 
@@ -906,15 +899,15 @@ then QUEUEMODE must match the mode of the queue currently
 being processed."
   (let (item)
     (unless proof-action-list
-      (while (and alist (not (nth 1 (setq item (car alist)))))
+      (while (and queueitems (not (nth 1 (setq item (car queueitems)))))
 	(proof-shell-invoke-callback item)
-	(setq alist (cdr alist))))
+	(setq queueitems (cdr queueitems))))
 
-    (if (and (null alist) (null proof-action-list))
+    (if (and (null queueitems) (null proof-action-list))
 	;; remove the queue (otherwise done in proof-shell-exec-loop)
 	(proof-detach-queue))
 
-    (when (and alist proof-action-list)
+    (when (and queueitems proof-action-list)
       ;; extend existing queue
       ;; internal check: correct queuemode in force if busy
       ;; (should have proof-action-list<>nil -> busy)
@@ -923,8 +916,8 @@ being processed."
 	     (proof-debug 
 	      "proof-append-alist: wrong queuemode detected for busy shell")
 	     (assert (eq proof-shell-busy queuemode))))
-
-      (if (proof-shell-should-be-silent (length alist))
+      ;; See if we should make prover quieten down
+      (if (proof-shell-should-be-silent (length queueitems))
 	  ;; do this ASAP, just after current command (head of queue).
 	  (setq proof-action-list
 		(cons (car proof-action-list)
@@ -932,42 +925,41 @@ being processed."
 			    (cdr proof-action-list)))))
       ;; append to the current queue
       (setq proof-action-list
-	    (nconc proof-action-list alist)))
+	    (nconc proof-action-list queueitems)))
 
-    (when (and alist (not proof-action-list))
+    (when (and queueitems (not proof-action-list))
       ;; start processing a new queue
       (proof-grab-lock queuemode)
       (setq proof-shell-last-output-kind nil)
-      (if (proof-shell-should-be-silent (length alist))
-	  ;;
+      (if (proof-shell-should-be-silent (length queueitems))
 	  (progn
 	    (setq proof-action-list
 		  (list (proof-shell-start-silent-item)))
 	    (setq item (car proof-action-list))))
       (setq proof-action-list
-	    (nconc proof-action-list alist))
+	    (nconc proof-action-list queueitems))
       ;; Really start things going here:
       (proof-shell-insert-action-item item))))
 
 ;;;###autoload
-(defun proof-start-queue (start end alist)
-  "Begin processing a queue of commands in ALIST.
+(defun proof-start-queue (start end queueitems)
+  "Begin processing a queue of commands in QUEUEITEMS.
 If START is non-nil, START and END are buffer positions in the
 active scripting buffer for the queue region.
 
 This function calls `proof-append-alist'."
   (if start
       (proof-set-queue-endpoints start end))
-  (proof-append-alist alist))
+  (proof-add-to-queue queueitems))
 
 ;;;###autoload
-(defun proof-extend-queue (end alist)
-  "Extend the current queue with commands in ALIST, queue end END.
+(defun proof-extend-queue (end queueitems)
+  "Extend the current queue with QUEUEITEMS, queue end END.
 To make sense, the commands should correspond to processing actions
 for processing a region from (buffer-queue-or-locked-end) to END.
 The queue mode is set to 'advancing"
   (proof-set-queue-endpoints (proof-unprocessed-begin) end)
-  (proof-append-alist alist 'advancing))
+  (proof-add-to-queue queueitems 'advancing))
 
 
 (defun proof-shell-exec-loop ()
@@ -999,14 +991,15 @@ The return value is non-nil if the action list is now empty."
 
        ;; invoke callback on just processed command
 ; PG 4.0: do this now *after* pumping the next command out,
-; to parallelize prover and Emacs somewhat
+; to parallelize prover and Emacs somewhat.  Experimental.
 ;      (proof-shell-invoke-callback item)
 
        (setq proof-action-list (cdr proof-action-list))
 
-       ;; slurp comments without sending to prover
+       ;; slurp empty command lists (comments) without sending
        (while (and proof-action-list
 		   (not (nth 1 (setq item (car proof-action-list)))))
+;; PG 4.0: delay this
 ;;	 (proof-shell-invoke-callback item)
 	 (setq cbitems (cons item cbitems))
 	 (setq proof-action-list (cdr proof-action-list)))
@@ -1028,13 +1021,15 @@ The return value is non-nil if the action list is now empty."
        (if proof-shell-interrupt-pending
 	   (progn
 	     (proof-debug "Processed pending interrupt")
-	     (proof-shell-handle-error-or-interrupt flags)))
+	     ;; don't pass in flags: want to see interrupt message
+	     (proof-shell-handle-error-or-interrupt 'interrupt nil)))
 
        (if proof-action-list
 	   ;; send the next command to the process.
 	   (proof-shell-insert-action-item item))
 
        ;; process the callbacks
+;; PG 4.0: process delayed callbacks out-of-order.
        (mapc 'proof-shell-invoke-callback (nreverse cbitems))
 
        (unless proof-action-list	; release lock, cleanup
@@ -1232,7 +1227,7 @@ A subroutine of `proof-shell-process-urgent-message'."
 	   (read-string msg nil
 	    'proof-shell-minibuffer-urgent-interactive-input-history))))
     ;; Always send something, even if read-input was errorful
-    (proof-shell-insert (or input "") 'interactive-input)))
+    (proof-shell-insert (list (or input "")) 'interactive-input)))
 
 
 
@@ -1542,8 +1537,6 @@ i.e., 'goals or 'response."
 
 
 
-
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 7a1ac808..7347ab58 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -53,10 +53,6 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 
-(require 'proof-compat)		        ;
-(require 'bufhist)			; bufhist
-;(require 'proof-syntax)			; syntax utils
-
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Handy macros
@@ -678,6 +674,19 @@ or if the window is the only window of its frame."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
+;; Function for manipulating output
+;;
+
+(defsubst proof-shell-strip-output-markup (string &optional push)
+  "Strip output markup from STRING.
+Convenience function to call function `proof-shell-strip-output-markup'.
+Optional argument PUSH is ignored."
+  (funcall proof-shell-strip-output-markup string))
+
+
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
 ;; Function for submitting bug reports.
 ;;
 
diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index bb565c54..d6fbc926 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -13,13 +13,13 @@
 
 ;;; Code:
 (eval-when-compile
+  (require 'span)		        ; span macros
   (require 'proof-site)			; compile for isar (defpgdefault, etc)
-  (require 'span)
   (proof-ready-for-assistant 'isar))
 
+(require 'cl)			        ; mapcan
 (require 'proof)			; for proof-assistant-symbol, etc.
 (require 'proof-syntax)			; for proof-string-match
-(require 'cl)				; mapcan
 
 
 ;; The isabelle custom group won't have been defined yet.
diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el
index da83aabb..cc5d51d7 100644
--- a/isar/isar-autotest.el
+++ b/isar/isar-autotest.el
@@ -5,6 +5,10 @@
 ;; $Id$
 ;;
 
+(eval-when-compile
+  (require 'proof-utils)
+  (proof-ready-for-assistant 'isar))
+
 (require 'pg-autotest)
 
 (unless noninteractive
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index c1e7f3aa..7eda6ae3 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -15,9 +15,8 @@
 (require 'cl)				; for-loop
 
 (eval-when (compile)
-  (require 'unicode-tokens))	  ; it's loaded dynamically at runtime
-
-(require 'proof-unicode-tokens)
+  (require 'unicode-tokens)	    ; it's loaded dynamically at runtime
+  (require 'proof-unicode-tokens))  ; that file loads us at runtime
 
 ;;
 ;; Customization
diff --git a/isar/isar.el b/isar/isar.el
index 52598abc..c08aa944 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -25,7 +25,8 @@
   (defvar outline-heading-end-regexp nil)
   (defvar comment-quote-nested nil)
   (defvar isar-use-find-theorems-form nil)
-  (proof-ready-for-assistant 'isar))	; compile for isar
+;  (proof-ready-for-assistant 'isar))	; compile for isar
+)
 
 (require 'isabelle-system)		; system code
 (require 'isar-find-theorems)		; "Find Theorems" search form
@@ -96,12 +97,12 @@ See -k option for Isabelle interface script."
    proof-terminal-char          ?\;          ; forcibly ends a command
    proof-electric-terminator-noterminator t  ; don't insert it
    proof-script-command-start-regexp
-
    (proof-regexp-alt
     ;; FIXME: this gets { and } wrong: they must _not_ appear as {* *}
     ;; because that's lexically a kind of comment.
     isar-any-command-regexp
     (regexp-quote ";"))
+
    proof-script-integral-proofs t
    ;; FIXME: use old parser for now to avoid { } problem
    proof-script-use-old-parser  t
@@ -144,6 +145,7 @@ See -k option for Isabelle interface script."
    proof-shell-start-silent-cmd "disable_pr"
    proof-shell-stop-silent-cmd  "enable_pr"
    proof-shell-trace-output-regexp  "\^AI\^AV"
+   proof-script-preprocess      'isar-command-wrapping
    ;; command hooks
    proof-goal-command-p         'isar-goal-command-p
    proof-really-save-command-p  'isar-global-save-command-p
@@ -290,7 +292,8 @@ This is called when Proof General spots output matching
        (base-name (file-name-nondirectory name)))
     (if (string= name base-name)
 	(isar-remove-file name proof-included-files-list t nil)
-      (isar-remove-file (file-truename name) proof-included-files-list nil nil))))
+      (isar-remove-file 
+       (file-truename name) proof-included-files-list nil nil))))
 
 
 ;;
@@ -535,7 +538,8 @@ selected.")
   "Use Isabelle's pretty printing facilities to adjust output line width.
 Checks the width in the `proof-goals-buffer'"
   (let ((ans ""))
-    (and (buffer-live-p proof-goals-buffer)
+    (and (not proof-shell-silent)
+	 (buffer-live-p proof-goals-buffer)
 	 (save-excursion
 	   (set-buffer proof-goals-buffer)
 	   (let ((current-width
@@ -555,54 +559,35 @@ Checks the width in the `proof-goals-buffer'"
 ;; Shell mode command adjusting
 ;;
 
-(defun isar-string-wrapping (string)
+(defsubst isar-string-wrapping (string)
   (concat
    "\""
-   (proof-replace-regexp-in-string
+   (replace-regexp-in-string
     "[\000-\037\"\\\\]"
     (lambda (str) (format "\\\\%03d" (string-to-char str)))
     string)
    "\""))
 
-(defun isar-positions-of (span)
-  (let (line file)
-    (if span
-	(save-excursion
-	  (set-buffer (span-buffer span))
-	  (goto-char (span-start span))
-	  (skip-chars-forward " \t\n")
-	  ;; NB: position is relative to display (narrowing, etc)
-	  ;; defer column: too tricky for now, see trac #277
-	  ; (setq column (current-column))
-	  (setq line (line-number-at-pos (point)))
-	  (setq file (or (buffer-file-name) (buffer-name)))))
-    (concat
-     "("
-     (proof-splice-separator
-      ", "
-      (list
-       (if file
-	   (format "\"file\"=%s" (isar-string-wrapping file)))
-       (if line   
-	   (format "\"line\"=\"%d\"" line))))
-    ;; (if column (format "\"column\"=\"%d\"" column))))
-      ") ")))
-
-(defun isar-command-wrapping (string scriptspan)
-  (if (and scriptspan (eq proof-shell-busy 'advancing))
-      ;; use Isabelle.command around script commands
-      (concat
-       "Isabelle.command "
-       (isar-positions-of scriptspan)
-       (isar-string-wrapping string))
-    (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string)))
+(defsubst isar-positions-of (filename start end)
+  (let ((line (line-number-at-pos start)))
+    (format "(\"file\"=%s, \"line\"=\"%d\") "
+	     (isar-string-wrapping filename) ; cache this?
+	     line)))
 
 (defcustom isar-wrap-commands-singly t
   "Non-nil to use command wrapping around commands sent to Isabelle.
-This slows down interactive processing somewhat."
+This slows down interactive processing slightly."
   :type 'boolean
   :group 'isabelle)
 
+(defun isar-command-wrapping (filename start end string)
+  "A value for `proof-script-preprocess'."
+  (if isar-wrap-commands-singly
+      (list "Isabelle.command "
+	    (isar-positions-of filename start end)
+	    (isar-string-wrapping string))
+    (list (replace-regexp-in-string "\n" "\\\\<^newline>" string))))
+
 (defun isar-preprocessing ()
   "Insert sync markers and other hacks.
 Uses variables `string' and `scriptspan' passed by dynamic scoping."
@@ -613,9 +598,7 @@ Uses variables `string' and `scriptspan' passed by dynamic scoping."
     (setq string (concat
 		  "\\<^sync>; "
 		  (isar-shell-adjust-line-width)
-		  (if isar-wrap-commands-singly
-		      (isar-command-wrapping string scriptspan)
-		    (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string))
+		  string
 		  " \\<^sync>;"))))
 
 ;;