Removed dead code

3 files changed, 7 insertions, 30 deletions

diff --git a/coq.el b/coq.el
index b24d4d21..5f80207d 100644
--- a/coq.el
+++ b/coq.el
@@ -3,6 +3,9 @@
 ;; Author: Healfdene Goguen and Thomas Kleymann
 
 ;; $Log$
+;; Revision 2.1  1998/09/03 11:07:07  da
+;; Removed dead code
+;;
 ;; Revision 2.0  1998/08/11 11:39:20  da
 ;; Renamed <file>-fontlock to <file>-syntax
 ;;
@@ -160,10 +163,6 @@
 (defconst coq-interrupt-regexp "Interrupted"
   "Regexp corresponding to an interrupt")
 
-(defvar coq-save-query t
-  "*If non-nil, ask user for permission to save the current buffer before
-  processing a module.")
-
 (defvar coq-default-undo-limit 100
   "Maximum number of Undo's possible when doing a proof.")
 
@@ -176,9 +175,6 @@
 (defvar coq-prog-name "coqtop -emacs"
   "*Name of program to run as Coq.")
 
-(defvar coq-shell-working-dir ""
-  "The working directory of the coq shell")
-
 (defvar coq-shell-prompt-pattern (concat "^" proof-id " < ")
   "*The prompt pattern for the inferior shell running coq.")
 
diff --git a/isa.el b/isa.el
index ceeae833..ccecdfaa 100644
--- a/isa.el
+++ b/isa.el
@@ -41,8 +41,8 @@ no regular or easily discernable structure.")
      "http://www.cl.cam.ac.uk/Research/HVG/isabelle.html"
     ;; proof script syntax
     proof-terminal-char	 ?\;		; ends a proof
-    proof-comment-start	"(*"		; comment in a proof
-    proof-comment-end		"*)"		; 
+    proof-comment-start		"(*"	; comment in a proof
+    proof-comment-end		"*)"	; 
     ;; proof engine output syntax
     proof-save-command-regexp   isa-save-command-regexp
     proof-save-with-hole-regexp isa-save-with-hole-regexp
@@ -52,8 +52,8 @@ no regular or easily discernable structure.")
     ;; proof engine commands
     proof-prf-string		"pr()"
     proof-ctxt-string		"the_context();" 
-    proof-help-string
-     "print \"No in-built help for Isabelle.\"" ; FIXME: proof.el should allow nil
+    proof-help-string ; could be version 
+     "print \" in-built help for Isabelle.\"" ; FIXME: proof.el should allow nil
     ;; command hooks
     proof-goal-command-p	'isa-goal-command-p
     proof-count-undos-fn	'isa-count-undos
@@ -100,17 +100,6 @@ no regular or easily discernable structure.")
     "Table of settings for configuration of proof shell mode to Isabelle.")
 
 
-;; =========================================================================
-;; FIXME: THESE TWO ARE DEAD?
-(defvar isa-save-query t
-  "*If non-nil, ask user for permission to save the current buffer before
-  processing a module.")
-
-(defvar isa-shell-working-dir ""
-  "The working directory of the isabelle shell")
-;; =========================================================================
-
-
 ;; ===== outline mode
 
 ;;; FIXME: test and add more things here
diff --git a/lego.el b/lego.el
index b8a398e1..30a1e389 100644
--- a/lego.el
+++ b/lego.el
@@ -21,10 +21,6 @@
   "*The name of the LEGO module which inherits all other modules of the
   library.")
 
-(defvar lego-save-query t
-  "*If non-nil, ask user for permission to save the current buffer before
-  processing a module.")
-
 (defvar lego-help-menu-list
   '(["The LEGO Reference Card" (w3-fetch lego-www-refcard) t]
     ["The LEGO library (WWW)" (w3-fetch lego-library-www-page)  t])
@@ -98,9 +94,6 @@
 (defvar lego-prog-name "lego"
   "*Name of program to run as lego.")
 
-(defvar lego-shell-working-dir ""
-  "The working directory of the lego shell")
-
 (defvar lego-shell-prompt-pattern "^\\(Lego>[ \201]*\\)+"
   "*The prompt pattern for the inferior shell running lego.")
 
@@ -424,7 +417,6 @@
 
 ;; hooks and callbacks
 
-  (add-hook 'proof-shell-exit-hook 'lego-zap-line-width nil t)
   (add-hook 'proof-pre-shell-start-hook 'lego-pre-shell-start nil t)
   (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width))