Remove proof-shell-prompt-pattern, no longer used.

16 files changed, 6 insertions, 46 deletions

diff --git a/acl2/acl2.el b/acl2/acl2.el
index a3e4fadd..da745d06 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.el
@@ -35,7 +35,6 @@
  proof-shell-error-regexp	 
  "^Error: \\|Error in TOP-LEVEL: \\|\\*\\*\\*\\* FAILED \\*\\*\\*"
  proof-shell-interrupt-regexp    "Correctable error: Console interrupt."
- proof-shell-prompt-pattern      "ACL2[ !]*>+"
 
  proof-shell-quit-cmd            ":q"	 ;; FIXME: followed by C-d.
  proof-shell-restart-cmd	 ":q\n:q\n:q\n(lp)\n"    ;; FIXME: maybe not?
diff --git a/ccc/ccc.el b/ccc/ccc.el
index 77544f85..0fdf77de 100644
--- a/ccc/ccc.el
+++ b/ccc/ccc.el
@@ -31,7 +31,6 @@
  proof-undo-n-times-cmd          "undo_steps %s;"
  proof-auto-multiple-files       nil 
  proof-shell-cd-cmd              "cd \"%s\""
- proof-shell-prompt-pattern      "^\\(CCC\\|^HOL-CASL\\) > "
  proof-shell-interrupt-regexp    "Interrupt"
  proof-shell-start-goals-regexp  "^No subgoals\\|^[0-9]* subgoals\\|^Wts:"
  proof-shell-end-goals-regexp    "val it"
diff --git a/coq/coq.el b/coq/coq.el
index f6b2e67f..a7048ced 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -979,7 +979,6 @@ To be used in `proof-shell-classify-output-system-specific'."
 
 (defun coq-shell-mode-config ()
   (setq 
-   proof-shell-prompt-pattern coq-shell-prompt-pattern
    proof-shell-cd-cmd coq-shell-cd
    proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\""   . "\\\""))
    proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp
diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el
index f5957f2d..4baae53d 100644
--- a/demoisa/demoisa-easy.el
+++ b/demoisa/demoisa-easy.el
@@ -50,7 +50,6 @@
  proof-undo-n-times-cmd          "pg_repeat undo %s;"
  proof-auto-multiple-files       t
  proof-shell-cd-cmd              "cd \"%s\""
- proof-shell-prompt-pattern      "[ML-=#>]+>? "
  proof-shell-interrupt-regexp    "Interrupt"
  proof-shell-start-goals-regexp  "Level [0-9]"
  proof-shell-end-goals-regexp    "val it"
diff --git a/demoisa/demoisa.el b/demoisa/demoisa.el
index ed3aa8e1..70886a85 100644
--- a/demoisa/demoisa.el
+++ b/demoisa/demoisa.el
@@ -93,7 +93,6 @@
   (setq
    proof-shell-annotated-prompt-regexp   "^\\(val it = () : unit\n\\)?\\(ML\\)?> "
    proof-shell-cd-cmd			"cd \"%s\""
-   proof-shell-prompt-pattern		"([ML-=#>]+>? "
    proof-shell-interrupt-regexp         "Interrupt"
    proof-shell-error-regexp		"\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
    proof-shell-start-goals-regexp	"Level [0-9]"
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 4ffeb659..b85cb0fd 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1612,13 +1612,6 @@ Codes above this character can have special meaning to Proof General,
 and are stripped from the prover's output strings.
 Leave unset if no special characters are being used.
 @end defvar
-@c TEXI DOCSTRING MAGIC: proof-shell-prompt-pattern
-@defvar proof-shell-prompt-pattern 
-Proof shell's value for comint-prompt-pattern, which see.@*
-NB!! This pattern is just for interaction in comint (shell buffer).
-You don't really need to set it.  The important one to set is
-@samp{@code{proof-shell-annotated-prompt-regexp}}, which see.
-@end defvar
 @c TEXI DOCSTRING MAGIC: proof-shell-annotated-prompt-regexp
 @defvar proof-shell-annotated-prompt-regexp 
 Regexp matching a (possibly annotated) prompt pattern.
@@ -3917,7 +3910,6 @@ Proof General.
  proof-undo-n-times-cmd          "pg_repeat undo %s;"
  proof-auto-multiple-files       t
  proof-shell-cd-cmd              "cd \"%s\""
- proof-shell-prompt-pattern      "[ML-=#>]+>? "
  proof-shell-interrupt-regexp    "Interrupt"
  proof-shell-start-goals-regexp  "Level [0-9]"
  proof-shell-end-goals-regexp    "val it"
@@ -4036,7 +4028,6 @@ Proof General.
   (setq
    proof-shell-annotated-prompt-regexp   "^\\(val it = () : unit\n\\)?ML>? "
    proof-shell-cd-cmd			"cd \"%s\""
-   proof-shell-prompt-pattern		"[ML-=#>]+>? "
    proof-shell-interrupt-regexp         "Interrupt"
    proof-shell-error-regexp		"\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
    proof-shell-start-goals-regexp	"Level [0-9]"
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 7db11cba..b0612661 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1078,14 +1078,6 @@ Normally error messages cause a beep.  Set this to nil to prevent that."
 ;; 5b. Regexp variables for matching output from proof process.
 ;;
 
-(defcustom proof-shell-prompt-pattern nil
-   "Proof shell's value for `comint-prompt-pattern', which see.
-NB!! This pattern is just for interaction in comint (shell buffer).
-You don't really need to set it.  The important one to set is
-`proof-shell-annotated-prompt-regexp', which see."
-   :type 'regexp
-   :group 'proof-shell)
-
 ;; FIXME da: replace this with wakeup-regexp or prompt-regexp?
 ;; May not need next variable.
 (defcustom proof-shell-wakeup-char nil
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 0b6f2ce9..cc41b123 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1822,11 +1822,8 @@ Error messages are displayed as usual."
 
   (buffer-disable-undo)
 
-  ;; comint customisation. 
+  ;; scomint customisation. 
 
-  (if proof-shell-prompt-pattern
-      (setq scomint-prompt-regexp proof-shell-prompt-pattern))
- 
   (setq scomint-output-filter-functions '(proof-shell-filter))
 
   ;; Proof marker is initialised in filter to first prompt found
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 0ca652c8..bd36a7d3 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -12,11 +12,11 @@
 (require 'proof-config)			; proof-case-fold-search
 (require 'proof-compat)			; proof-buffer-syntactic-context
 
-(defun proof-ids-to-regexp (l)
+(defsubst proof-ids-to-regexp (l)
   "Maps a non-empty list of tokens `l' to a regexp matching any element"
   (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>"))
 
-(defun proof-anchor-regexp (e)
+(defsubst proof-anchor-regexp (e)
   "Anchor (\\`) and group the regexp E."
   (concat "\\`\\(" e "\\)"))
 
@@ -25,7 +25,7 @@
   "A regular expression that never matches anything")
 
 
-(defun proof-regexp-alt (&rest args)
+(defsubst proof-regexp-alt (&rest args)
   "Return the regexp which matches any of the regexps ARGS."
   ;; see regexp-optn (NB: but that is for strings, not regexps)
   (let ((res ""))
diff --git a/hol98/hol98.el b/hol98/hol98.el
index 9990b600..653bbcb8 100644
--- a/hol98/hol98.el
+++ b/hol98/hol98.el
@@ -33,7 +33,6 @@
  proof-auto-multiple-files       t
  proof-shell-cd-cmd              "FileSys.chDir \"%s\""
  proof-shell-filename-escapes    '(("\\\\" . "\\\\") ("\""   . "\\\""))
- proof-shell-prompt-pattern      "^[->] "
  proof-shell-interrupt-regexp    "Interrupted"
  proof-shell-start-goals-regexp  
  (proof-regexp-alt "Proof manager status" 
diff --git a/isar/isar.el b/isar/isar.el
index bfe635d0..bd2216b4 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -161,9 +161,6 @@ See -k option for Isabelle interface script."
    proof-shell-wakeup-char              nil
    proof-shell-annotated-prompt-regexp  "^\\w*[>#] \^AS"
 
-   ;; just for comint.
-   proof-shell-prompt-pattern           "^\\w*[>#] "
-
    ;; for issuing command, not used to track cwd in any way.
    proof-shell-cd-cmd		(isar-markup-ml "ThyLoad.add_path \"%s\"")
 
diff --git a/lclam/lclam.el b/lclam/lclam.el
index 9b9be6d8..5d5c180b 100644
--- a/lclam/lclam.el
+++ b/lclam/lclam.el
@@ -56,7 +56,6 @@
   (setq
    proof-shell-annotated-prompt-regexp "^lclam:" 
    proof-shell-cd-cmd                  nil
-   proof-shell-prompt-pattern          nil
    proof-shell-interrupt-regexp        nil
    proof-shell-error-regexp            nil
    proof-shell-start-goals-regexp      nil
diff --git a/lego/lego.el b/lego/lego.el
index 896309f0..bdd1dd6f 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -99,9 +99,6 @@ Activates extended printing routines required for Proof General.")
 (defvar lego-prog-name "lego"
   "*Name of program to run as lego.")
 
-(defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+"
-  "*The prompt pattern for the inferior shell running lego.")
-
 (defvar lego-shell-cd "Cd \"%s\";"
   "*Command of the inferior process to change the directory.") 
 
@@ -384,8 +381,7 @@ We assume that module identifiers coincide with file names."
 	  proof-included-files-list))))
 
 (defun lego-shell-mode-config ()
-  (setq proof-shell-prompt-pattern lego-shell-prompt-pattern
-        proof-shell-cd-cmd lego-shell-cd
+  (setq proof-shell-cd-cmd lego-shell-cd
         proof-shell-abort-goal-regexp lego-shell-abort-goal-regexp
         proof-shell-proof-completed-regexp lego-shell-proof-completed-regexp
         proof-shell-error-regexp lego-error-regexp
diff --git a/phox/phox.el b/phox/phox.el
index 8244edb7..d4dfc0a3 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -152,7 +152,6 @@
   "Configure Proof General shell for PhoX."
   (setq
    ;proof-shell-cd-cmd              "cd \"%s\""
-   proof-shell-prompt-pattern      "\\(>phox> \\)\\|\\(%phox% \\)"
    proof-shell-annotated-prompt-regexp  "\\(>phox> \\)\\|\\(%phox% \\)"
    proof-shell-interrupt-regexp    "Interrupt"
    proof-shell-start-goals-regexp  "^\\(Here \\(are\\|is\\) the goal\\)\\|\\([0-9]+ new goals?\\)\\|\\([0-9]+ goals? possibly instanced\\)"
diff --git a/plastic/plastic.el b/plastic/plastic.el
index e15f708b..b02d2065 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -121,9 +121,6 @@
 		(setenv "PLASTIC_TEST" (concat plastic-base "/test"))
 	)))
 
-(defvar plastic-shell-prompt-pattern "^\\(LF>[ \201]*\\)+"
-  "*The prompt pattern for the inferior shell running plastic.")
-
 (defvar plastic-shell-cd 
   (concat plastic-lit-string " &S ECHO no cd ;\n")
   "*Command of the inferior process to change the directory.") 
@@ -457,8 +454,7 @@ We assume that module identifiers coincide with file names."
 
 
 (defun plastic-shell-mode-config ()
-  (setq proof-shell-prompt-pattern plastic-shell-prompt-pattern
-        proof-shell-cd-cmd plastic-shell-cd
+  (setq proof-shell-cd-cmd plastic-shell-cd
         proof-shell-abort-goal-regexp plastic-shell-abort-goal-regexp
         proof-shell-proof-completed-regexp plastic-shell-proof-completed-regexp
         proof-shell-error-regexp plastic-error-regexp
diff --git a/twelf/twelf.el b/twelf/twelf.el
index 82b32e7e..07590ea9 100644
--- a/twelf/twelf.el
+++ b/twelf/twelf.el
@@ -52,7 +52,6 @@
 
  proof-auto-multiple-files       t
  proof-shell-cd-cmd              "OS.chDir %s"
- proof-shell-prompt-pattern      "%% OK %%\n"
  proof-shell-interrupt-regexp    "interrupt"
 
  proof-shell-annotated-prompt-regexp "%% [OA][KB]O?R?T? %%\n"