Configuration changes for shell mode revision.

4 files changed, 67 insertions, 81 deletions

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 93ee129a..472d14fa 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -9,8 +9,8 @@
 
 @c
 @c TODO:  
-@c   MMM support, Theorem dependencies, history in script and response
-@c
+@c   MMM support, Theorem dependencies, history in script and response,
+@c   identifier info commands
 
 
 @c
@@ -1460,8 +1460,7 @@ It was constructed with @samp{@code{proof-deftoggle-fn}}.
 @c TEXI DOCSTRING MAGIC: proof-assert-until-point-interactive
 @deffn Command proof-assert-until-point-interactive 
 Process the region from the end of the locked-region until point.@*
-Default action if inside a comment is just process as far as the start of
-the comment.
+If inside a comment, just process until the start of the comment.
 @end deffn
 
 @c TEXI DOCSTRING MAGIC: proof-retract-until-point-interactive
@@ -1525,7 +1524,7 @@ A fixed number of repetitions of this command switches back to
 the same buffer.
 Also move point to the end of the response buffer if it's selected.
 If in three window or multiple frame mode, display two buffers.
-The idea of this function is to change the window->buffer mapping 
+The idea of this function is to change the window->buffer mapping
 without adjusting window layout.
 @end deffn
 
@@ -2132,9 +2131,8 @@ with the proof assistant rather than sending commands via the
 minibuffer, @pxref{Proof assistant commands}.
 
 Although the proof shell is usually hidden from view, it is run in a
-buffer which provides the usual full editing and history facilities of
-Emacs shells (see the package @file{comint.el} distributed with your
-version of Emacs). You can switch to it using the menu:
+buffer which you can use to interact with the prover if necessary.  You
+can switch to it using the menu:
 
 @lisp
   Proof-General -> Buffers -> Shell
@@ -2884,7 +2882,7 @@ A fixed number of repetitions of this command switches back to
 the same buffer.
 Also move point to the end of the response buffer if it's selected.
 If in three window or multiple frame mode, display two buffers.
-The idea of this function is to change the window->buffer mapping 
+The idea of this function is to change the window->buffer mapping
 without adjusting window layout.
 @end deffn
 
@@ -2963,7 +2961,7 @@ The default value is @code{t}.
 @defopt proof-electric-terminator-enable 
 If non-nil, use electric terminator mode.@*
 If electric terminator mode is enabled, pressing a terminator will
-automatically issue @samp{@code{proof-assert-next-command}} for convenience,
+automatically issue @samp{proof-assert-next-command} for convenience,
 to send the command straight to the proof process.  If the command
 you want to send already has a terminator character, you don't
 need to delete the terminator character first.  Just press the
@@ -2993,10 +2991,9 @@ The default value is @code{t}.
 @defopt proof-allow-undo-in-read-only 
 Whether Proof General allows text undo in the read-only region.@*
 If non-nil, undo will allow altering of processed text.
-If nil, undo history is cut at first edit
-of processed text.
+If nil, undo is blocked if the next undo is in processed text.
 
-The default value is @code{t}.
+The default value is @code{nil}.
 @end defopt
 
 @c This one removed: proof-auto-retract
diff --git a/isar/isar.el b/isar/isar.el
index 58391efd..9fc3b079 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -158,7 +158,6 @@ See -k option for Isabelle interface script."
   "Configure generic proof shell mode variables for Isabelle/Isar."
   (setq
 
-   proof-shell-wakeup-char              nil
    proof-shell-annotated-prompt-regexp  "^\\w*[>#] \^AS"
 
    ;; for issuing command, not used to track cwd in any way.
@@ -188,7 +187,7 @@ See -k option for Isabelle interface script."
    ;; matches names of assumptions
    proof-shell-assumption-regexp        isar-id
 
-   proof-shell-start-goals-regexp       "\^AO\n"
+   proof-shell-start-goals-regexp       "\^AO"
    proof-shell-end-goals-regexp         "\^AP"
 
    proof-shell-init-cmd			nil
@@ -199,36 +198,37 @@ See -k option for Isabelle interface script."
    proof-shell-eager-annotation-end     "\^AJ\\|\^AL"
    proof-shell-strip-output-markup	'isar-strip-output-markup
 
-   ;; Isabelle is learning to talk PGIP...
-   proof-shell-match-pgip-cmd		"<pgip"
-   proof-shell-issue-pgip-cmd		'isabelle-process-pgip
-
-   ;; Some messages delimited by eager annotations
-   proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
-   proof-shell-clear-goals-regexp       "Proof General, please clear the goals buffer."
-
-   ;; Theorem dependencies.
-   ;; NB: next regex anchored at end with eager annot end
-   proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\^AJ\\)"
-   proof-shell-theorem-dependency-list-split "\" \""
-   proof-shell-show-dependency-cmd "thm %s;"
-
    pg-special-char-regexp               "\^A[0-9A-Z]"
-
    pg-subterm-help-cmd			"term %s"
-
    proof-cannot-reopen-processed-files  t
+
+   ;; Urgent messages delimited by eager annotations
+   proof-shell-clear-response-regexp    
+   "\^AIProof General, please clear the response buffer."
+   proof-shell-clear-goals-regexp       
+   "\^AIProof General, please clear the goals buffer."
+   proof-shell-theorem-dependency-list-regexp 
+   "\^AIProof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\^AJ\\)"
+   proof-shell-retract-files-regexp
+   "\^AIProof General, you can unlock the file \"\\(.*\\)\"\^AJ"
    proof-shell-process-file
    (cons
     ;; Theory loader output
-    "Proof General, this file is loaded: \"\\(.*\\)\""
-    (lambda (str)
-      (match-string 1 str)))
-   proof-shell-retract-files-regexp
-   "Proof General, you can unlock the file \"\\(.*\\)\""
+    "\^AIProof General, this file is loaded: \"\\(.*\\)\"\^AJ"
+    (lambda () (match-string 1)))
+   proof-shell-match-pgip-cmd		"\^AI<pgip"
+
+   ;; configuration for these
+   proof-shell-issue-pgip-cmd		'isabelle-process-pgip
+
+   proof-shell-theorem-dependency-list-split "\" \""
+   proof-shell-show-dependency-cmd	"thm %s;"
+
    proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list
-   proof-shell-inform-file-processed-cmd "ProofGeneral.inform_file_processed \"%s\""
-   proof-shell-inform-file-retracted-cmd "ProofGeneral.inform_file_retracted \"%s\""))
+   proof-shell-inform-file-processed-cmd 
+   "ProofGeneral.inform_file_processed \"%s\""
+   proof-shell-inform-file-retracted-cmd 
+   "ProofGeneral.inform_file_retracted \"%s\""))
 
 
 ;;;
@@ -264,12 +264,12 @@ See -k option for Isabelle interface script."
       (if same (isar-remove-file name rest cmp-base result)
 	(isar-remove-file name rest cmp-base (cons file result))))))
 
-(defun isar-shell-compute-new-files-list (str)
+(defun isar-shell-compute-new-files-list ()
   "Compute the new list of files read by the proof assistant.
 This is called when Proof General spots output matching
 `proof-shell-retract-files-regexp'."
   (let*
-      ((name (match-string 1 str))
+      ((name (match-string 1))
        (base-name (file-name-nondirectory name)))
     (if (string= name base-name)
 	(isar-remove-file name proof-included-files-list t nil)
@@ -392,8 +392,7 @@ This is called when Proof General spots output matching
 (defun isar-count-undos (span)
   "Count number of undos SPAN, return command needed to undo that far."
   (let
-      ((case-fold-search nil)       ;FIXME ??
-       (ct 0) str i)
+      ((ct 0) str i)
     (while span
       (setq str (or (span-property span 'cmd) ""))
       (cond ((eq (span-property span 'type) 'vanilla)
@@ -540,11 +539,6 @@ Checks the width in the `proof-goals-buffer'"
 ;; Shell mode command adjusting
 ;;
 
-(defconst isar-nonwrap-regexp
-  ;; FIXME: approx: should only match at start or after terminator
-  (regexp-opt (append (list "ProofGeneral.process_pgip")
-		      isar-undo-commands)))
-
 (defun isar-string-wrapping (string)
   (concat
    "\""
@@ -554,34 +548,36 @@ Checks the width in the `proof-goals-buffer'"
     string)
    "\""))
 
-(defun isar-positions-of (buffer span)
-  (let (line)
+(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 #274
+	  ;; defer column: too tricky for now, see trac #277
 	  ; (setq column (current-column))
-	  (setq line (line-number-at-pos (point)))))
+	  (setq line (line-number-at-pos (point)))
+	  (setq file (or (buffer-file-name) (buffer-name)))))
     (concat
      "("
      (proof-splice-separator
       ", "
       (list
-       (if (and buffer (buffer-file-name buffer))
-	   (format "\"file\"=%s"
-		   (isar-string-wrapping (buffer-file-name buffer))))
-       (if line   (format "\"line\"=\"%d\"" line))))
-       ;(if column (format "\"column\"=\"%d\"" column))))
+       (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 (not (proof-string-match isar-nonwrap-regexp string))
+  (if (and scriptspan (eq proof-shell-busy 'advancing))
+      ;; use Isabelle.command around script commands
       (concat
        "Isabelle.command "
-       (isar-positions-of proof-script-buffer scriptspan)
+       (isar-positions-of scriptspan)
        (isar-string-wrapping string))
     (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string)))
 
diff --git a/lego/lego.el b/lego/lego.el
index fe73c017..9dc7dd47 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -368,16 +368,12 @@ The directory and extension is stripped of FILENAME before the test."
   (equal module
 	 (file-name-sans-extension (file-name-nondirectory filename))))
 
-(defun lego-shell-compute-new-files-list (str)
-  "Function to update `proof-included-files list'.
+(defun lego-shell-compute-new-files-list ()
+  "Function to update `proof-included-files-list'.
+Value for `proof-shell-compute-new-files-list', which see.
 
-It needs to return an up to date list of all processed files. Its
-output is stored in `proof-included-files-list'. Its input is the
-string of which `lego-shell-retract-files-regexp' matched a
-substring.
-
-We assume that module identifiers coincide with file names."
-  (let ((module (match-string 1 str)))
+For LEGO, we assume that module identifiers coincide with file names."
+  (let ((module (match-string 1)))
     (cdr (member-if
 	  (lambda (filename) (lego-equal-module-filename module filename))
 	  proof-included-files-list))))
@@ -414,9 +410,9 @@ We assume that module identifiers coincide with file names."
 
 	proof-shell-process-file
 	(cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]"
-	  (lambda (str) (let ((match (match-string 2 str)))
-			  (if (equal match "") match
-			    (concat (file-name-sans-extension match) ".l")))))
+	  (lambda () (let ((match (match-string 2)))
+		       (if (equal match "") match
+			 (concat (file-name-sans-extension match) ".l")))))
 
 	proof-shell-retract-files-regexp
 	"forgot back through Mark \"\\(.*\\)\""
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 7707ee56..5a7a7f03 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -437,16 +437,12 @@ The directory and extension is stripped of FILENAME before the test."
   (equal module
 	 (file-name-sans-extension (file-name-nondirectory filename))))
 
-(defun plastic-shell-compute-new-files-list (str)
+(defun plastic-shell-compute-new-files-list ()
   "Function to update `proof-included-files list'.
+Value for `proof-shell-compute-new-files-list', which see.
 
-It needs to return an up to date list of all processed files. Its
-output is stored in `proof-included-files-list'. Its input is the
-string of which `plastic-shell-retract-files-regexp' matched a
-substring.
-
-We assume that module identifiers coincide with file names."
-  (let ((module (match-string 1 str)))
+For Plastic, we assume that module identifiers coincide with file names."
+  (let ((module (match-string 1)))
     (cdr (member-if
 	  (lambda (filename) (plastic-equal-module-filename module filename))
 	  proof-included-files-list))))
@@ -487,9 +483,10 @@ We assume that module identifiers coincide with file names."
 
 	proof-shell-process-file
 	(cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]"
-	  (lambda (str) (let ((match (match-string 2 str)))
-			  (if (equal match "") match
-			    (concat (file-name-sans-extension match) ".l")))))
+	      (lambda () (let ((match (match-string 2)))
+			      (if (equal match "") match
+				(concat 
+				 (file-name-sans-extension match) ".lf")))))
 
 	proof-shell-retract-files-regexp "forgot back through Mark \"\\(.*\\)\""
 	proof-shell-font-lock-keywords plastic-font-lock-keywords-1