Many compatibility updates, bug fixes, rearrangements for compilation.

4 files changed, 112 insertions, 124 deletions

diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el
index 65953162..e0dd6207 100644
--- a/isar/isabelle-system.el
+++ b/isar/isabelle-system.el
@@ -1,6 +1,6 @@
-;; isabelle-system.el Interface with Isabelle system
+;; isabelle-system.el --- Interface with Isabelle system
 ;;
-;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall. 
+;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall.
 ;;
 ;; Author:      David Aspinall <da@dcs.ed.ac.uk>
 ;; Maintainer:  Proof General maintainer <proofgen@dcs.ed.ac.uk>
@@ -11,6 +11,11 @@
 ;; --------------------------------------------------------------
 ;;
 
+;;; Code:
+(eval-when-compile
+  (require 'proof-site)			; compile for isar (defpgdefault, etc)
+  (proof-ready-for-assistant 'isar))
+
 (require 'proof)			; for proof-assistant-symbol, etc.
 (require 'proof-syntax)			; for proof-string-match
 
@@ -32,7 +37,7 @@
 ;;; ================ Extract Isabelle settings ================
 
 (defcustom isa-isatool-command
-  (or (getenv "ISATOOL") 
+  (or (getenv "ISATOOL")
       (proof-locate-executable "isatool")
       ;; FIXME: use same mechanism as isabelle-program-name below.
       (let ((possibilities
@@ -53,7 +58,7 @@
   "Command to invoke Isabelle tool 'isatool'.
 XEmacs should be able to find `isatool' if it is on the PATH when
 started.  Then several standard locations are attempted.
-Otherwise you should set this, using a full path name here for reliable 
+Otherwise you should set this, using a full path name here for reliable
 working."
   :type 'file
   :group 'isabelle)
@@ -88,7 +93,7 @@ with full path."
       (substring s 0 -1))))
 
 (defun isa-getenv (envvar &optional default)
-  "Extract an environment variable setting using the `isatool' program.
+  "Extract environment variable ENVVAR setting using the `isatool' program.
 If the isatool command is not available, try using elisp's getenv
 to extract the value from Emacs' environment.
 If there is no setting for the variable, DEFAULT will be returned"
@@ -106,8 +111,8 @@ If there is no setting for the variable, DEFAULT will be returned"
 ;;; ======= Interaction with System using Isabelle tools =======
 ;;;
 
-(defcustom isabelle-program-name 
-  (if (fboundp 'proof-running-on-win32)	
+(defcustom isabelle-program-name
+  (if proof-running-on-win32
       "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\"
     (proof-locate-executable "isabelle" t
 			     '("/usr/local/Isabelle/bin/"
@@ -118,14 +123,14 @@ If there is no setting for the variable, DEFAULT will be returned"
 
 The default value except when running under Windows is \"isabelle\",
 which will get expanded using PATH if possible, or in a number
-of standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc). 
+of standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc).
 
 The default value when running under Windows is:
 
   C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\
 
-This expects SML/NJ in C:\\sml and Isabelle images in C:\Isabelle.  
-The logic image name is tagged onto the end.  
+This expects SML/NJ in C:\\sml and Isabelle images in C:\Isabelle.
+The logic image name is tagged onto the end.
 
 NB: The Isabelle settings mechanism or the environment variable
 ISABELLE will always override this setting."
@@ -136,7 +141,7 @@ ISABELLE will always override this setting."
   "Set from `isabelle-program-name', has name of logic appended sometimes.")
 
 (defun isabelle-command-line ()
-  "Make proper command line for running Isabelle"
+  "Make proper command line for running Isabelle."
   (let*
       ;; The ISABELLE and PROOFGENERAL_LOGIC values (as set when run
       ;; under the interface wrapper script) indicate that we should
@@ -161,22 +166,22 @@ ISABELLE will always override this setting."
 
 (defun isabelle-choose-logic (logic)
   "Adjust isabelle-prog-name and proof-prog-name for running LOGIC."
-  (interactive 
-   (list (completing-read 
+  (interactive
+   (list (completing-read
 	  "Use logic: "
-	  (mapcar 'list (cons "Default" 
+	  (mapcar 'list (cons "Default"
 			      isabelle-logics-available)))))
   ;; a little bit obnoxious maybe (but maybe what naive user would expect)
   ;; (customize-save-variable 'isabelle-chosen-logic logic)
   (if (proof-shell-live-buffer)
       (error "Can't change logic while Isabelle is running, please exit process first!"))
-  (customize-set-variable 'isabelle-chosen-logic 
+  (customize-set-variable 'isabelle-chosen-logic
 			  (unless (string-equal logic "Default") logic))
   (setq isabelle-prog-name (isabelle-command-line))
   (setq proof-prog-name isabelle-prog-name)
   ;; Settings are potentially different between logics, and
   ;; so are Isar keywords.  Set these to nil so they get
-  ;; automatically re-initialised.  
+  ;; automatically re-initialised.
   ;; FIXME: Isar keywords change not handled yet.
   (setq proof-assistant-settings nil)
   (setq proof-menu-settings nil))
@@ -184,7 +189,7 @@ ISABELLE will always override this setting."
 (defun isa-tool-list-logics ()
   "Generate a list of available object logics."
   (if (isa-set-isatool-command)
-      (delete "" (split-string 
+      (delete "" (split-string
 		  (isa-shell-command-to-string
 		   (concat isa-isatool-command " findlogics")) "[ \t]"))))
 
@@ -209,7 +214,7 @@ passed to isa-tool-doc-command, DOCNAME will be viewed."
 	  (mapcan
 	   (function (lambda (docdes)
 		       (if (proof-string-match "^[ \t]+\\(\\S-+\\)[ \t]+" docdes)
-			   (list (list 
+			   (list (list
 				  (substring docdes (match-beginning 1) (match-end 1))
 				  (substring docdes (match-end 0)))))))
 	   (split-string docs "\n"))))))
@@ -224,10 +229,10 @@ passed to isa-tool-doc-command, DOCNAME will be viewed."
 ;   (comint-send-eof))
 
 (defconst isabelle-verbatim-regexp "\\`\^VERBATIM: \\(\\(.\\|\n\\)*\\)\\'"
-  "Regexp matching internal marker for verbatim command output")
+  "Regexp matching internal marker for verbatim command output.")
 
 (defun isabelle-verbatim (str)
-  "Mark internal command for verbatim output"
+  "Mark internal command STR for verbatim output."
   (concat "\^VERBATIM: " str))
 
 
@@ -244,7 +249,7 @@ for you, you should disable this behaviour."
 (defcustom isabelle-logics-available (isa-tool-list-logics)
   "*List of logics available to use with Isabelle.
 If the `isatool' program is available, this is automatically
-generated with the lisp form `(isa-tool-list-logics)'."
+generated with the Lisp form `(isa-tool-list-logics)'."
   :type (list 'string)
   :group 'isabelle)
 
@@ -262,7 +267,7 @@ until Proof General is restarted."
 	       '(const :tag "Unset (use default)" nil)))
   :group 'isabelle)
 
-(defconst isabelle-docs-menu 
+(defconst isabelle-docs-menu
   (let ((vc '(lambda (docdes)
 	       (vector (car (cdr docdes))
 		       (list 'isa-view-doc (car docdes)) t))))
@@ -276,12 +281,12 @@ until Proof General is restarted."
   (setq isabelle-logics-menu-entries
 	(cons "Logics"
 	      (append
-	       '(["Default" 
+	       '(["Default"
 		  (isabelle-choose-logic nil)
 		  :active (not (proof-shell-live-buffer))
 		  :style radio
 		  :selected (not isabelle-chosen-logic)])
-	       (mapcar (lambda (l) 
+	       (mapcar (lambda (l)
 		   (vector l (list 'isabelle-choose-logic l)
 			   :active '(not (proof-shell-live-buffer))
 			   :style 'radio
@@ -289,7 +294,7 @@ until Proof General is restarted."
 		       isabelle-logics-available)))))
 
 (defvar isabelle-time-to-refresh-logics t
-  "Non-nil if we should refresh the logics list")
+  "Non-nil if we should refresh the logics list.")
 
 (defun isabelle-logics-menu-refresh ()
   "Refresh isabelle-logics-menu-entries, returning new entries."
@@ -299,9 +304,9 @@ until Proof General is restarted."
       (progn
 	(setq isabelle-logics-available (isa-tool-list-logics))
 	(isabelle-logics-menu-calculate)
-	(if proof-running-on-Emacs21 
+	(if (not (featurep 'xemacs))
 	    ;; update the menu manually
-	    (easy-menu-add-item proof-assistant-menu nil 
+	    (easy-menu-add-item proof-assistant-menu nil
 				isabelle-logics-menu-entries))
 	(setq isabelle-time-to-refresh-logics nil) ;; just done it, don't repeat!
 	(run-with-timer 2 nil ;; short delay to avoid doing this too often
@@ -313,22 +318,22 @@ until Proof General is restarted."
   (cdr isabelle-logics-menu-entries))
 
 ;; Functions for GNU Emacs only to update logics menu
-(if proof-running-on-Emacs21
+(if (not (featurep 'xemacs))
 (defun isabelle-menu-bar-update-logics ()
-  ;; standard check we're being invoked
+  "Update logics menu."
   (and (current-local-map)
-       (keymapp (lookup-key (current-local-map) 
+       (keymapp (lookup-key (current-local-map)
  			    (vector 'menu-bar (intern proof-assistant))))
        (isabelle-logics-menu-refresh))))
 
-(if proof-running-on-Emacs21
+(if (not (featurep 'xemacs))
     (add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics))
 
 
 (defvar isabelle-logics-menu-entries (isabelle-logics-menu-calculate))
 
-(defvar isabelle-logics-menu 
-   (if proof-running-on-XEmacs
+(defvar isabelle-logics-menu
+   (if (featurep 'xemacs)
        (cons (car isabelle-logics-menu-entries)
 	     (list :filter 'isabelle-logics-menu-filter)) ;; generates menu on click
      isabelle-logics-menu-entries)
@@ -373,17 +378,17 @@ until Proof General is restarted."
 ;;
 
 (eval-after-load "x-symbol-isar"
- ;; Add x-symbol tokens to isa-completion-table and rebuild
- ;; internal completion table if completion is already active
-'(progn
-   (defpgdefault completion-table
-     (append (proof-ass completion-table)
-	     (mapcar (lambda (xsym) (nth 2 xsym))
-		     x-symbol-isar-table)))
-   (setq proof-xsym-font-lock-keywords
-	 x-symbol-isar-font-lock-keywords)
-   (if (featurep 'completion)
-       (proof-add-completions))))
+  ;; Add x-symbol tokens to isa-completion-table and rebuild
+  ;; internal completion table if completion is already active
+  '(progn
+     (defpgdefault completion-table
+       (append isar-completion-table
+	       (mapcar (lambda (xsym) (nth 2 xsym))
+		       x-symbol-isar-table)))
+     (setq proof-xsym-font-lock-keywords
+	   x-symbol-isar-font-lock-keywords)
+     (if (featurep 'completion)
+	 (proof-add-completions))))
 
 
 
@@ -413,15 +418,15 @@ the function `pg-remove-specials' can be used instead)."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Context-senstive in-span menu additions 
+;; Context-senstive in-span menu additions
 ;;
 
 (defun isabelle-create-span-menu (span idiom name)
   (if (string-equal idiom "proof")
       (let ((thm (span-property span 'name)))
-	(list (vector 
-	       "Visualise dependencies" 
-	       `(proof-shell-invisible-command 
+	(list (vector
+	       "Visualise dependencies"
+	       `(proof-shell-invisible-command
 		 ,(format "thm_deps %s;" thm))
 	       (not (string-equal thm proof-unnamed-theorem-name)))))))
 
@@ -442,4 +447,4 @@ the function `pg-remove-specials' can be used instead)."
 
 
 (provide 'isabelle-system)
-;; End of isabelle-system.el
+;;; isabelle-system.el ends here
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 98f5798a..8bd908b4 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -9,6 +9,8 @@
 ;; $Id$
 ;;
 
+(require 'cl)				; remove-if, remove-if-not
+
 (require 'proof-syntax)
 (require 'isar-keywords)
 
@@ -35,7 +37,7 @@
          ?\( "()1"
          ?\) ")(4")
    (cond
-    (proof-running-on-XEmacs
+    ((featurep 'xemacs)
      ;; We classify {* sequences *} as comments, although
      ;; they need to be passed as command args as text.
      ;; NB: adding a comment sequence b seems to break
@@ -49,7 +51,7 @@
     ;;(?\{ "(}1")
     ;;(?\} "){4")
     ;;(?\* ". 23"))
-    (proof-running-on-Emacs21
+    ((not (featurep 'xemacs))
      '(?\{ "(}1b"
        ?\} "){4b"
        ?\* ". 23n"))))
@@ -460,7 +462,7 @@ matches contents of quotes for quoted identifiers.")
 
 (defun isar-undos (i)
   (if (> i 0) (concat "undos_proof " (int-to-string i) ";")
-    proof-no-command))
+    nil))
 
 (defun isar-cannot-undo (cmd)
   (concat "cannot_undo \"" cmd "\";"))
diff --git a/isar/isar.el b/isar/isar.el
index 1c3f86c1..a3d2629f 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -1,9 +1,9 @@
-; isar.el	  Major mode for Isabelle/Isar proof assistant
+; isar.el --- Major mode for Isabelle/Isar proof assistant
 ;; Copyright (C) 1994-2004 LFCS Edinburgh.
 ;;
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
-;; Maintainers:   David Aspinall, Stefan Berghofer
+;; Maintainers:   David Aspinall, Makarius, Stefan Berghofer
 ;;
 ;; Authors:       David Aspinall <David.Aspinall@ed.ac.uk>
 ;;   	          Markus Wenzel <wenzelm@in.tum.de>
@@ -14,13 +14,16 @@
 ;; $Id$
 ;;
 
+;;; Code:
 (require 'proof)
 
-;; System code
-(require 'isabelle-system)
+(eval-when-compile
+  (require 'span)
+  (require 'proof-syntax)
+  (proof-ready-for-assistant 'isar))	; compile for isar
 
-;; "Find Theorems" search form
-(require 'isar-find-theorems)
+(require 'isabelle-system)		; system code
+(require 'isar-find-theorems)		; "Find Theorems" search form
 
 ;;
 ;; Load syntax
@@ -35,7 +38,7 @@ See -k option for Isabelle interface script."
     ;; Pickup isar-keywords file from somewhere appropriate,
     ;; giving user chance to set name of file, or based on
     ;; name of logic.
-    (isabelle-load-isar-keywords 
+    (isabelle-load-isar-keywords
      (or isar-keywords-name
 	 isabelle-chosen-logic)))
 (require 'isar-syntax)
@@ -53,9 +56,9 @@ See -k option for Isabelle interface script."
 
 ;; Adjust toolbar entries (must be done before proof-toolbar is loaded).
 
-(if proof-running-on-XEmacs
-    (setq isar-toolbar-entries
-	  (remassoc 'qed (remassoc 'goal isar-toolbar-entries))))
+(eval-after-load "pg-custom"
+  '(setq isar-toolbar-entries
+	 (remassoc 'qed (remassoc 'goal isar-toolbar-entries))))
 
 
 (defun isar-strip-terminators ()
@@ -80,10 +83,10 @@ See -k option for Isabelle interface script."
   "Configure generic proof scripting mode variables for Isabelle/Isar."
   (setq
    proof-assistant-home-page    isar-web-page
-   proof-mode-for-script        'isar-mode
+   proof-prog-name		(isabelle-command-line)
    ;; proof script syntax
    proof-terminal-char          ?\;     ; forcibly ends a command
-   proof-script-command-start-regexp 
+   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.
@@ -138,7 +141,7 @@ See -k option for Isabelle interface script."
    proof-find-and-forget-fn     'isar-find-and-forget
    proof-state-preserving-p     'isar-state-preserving-p
    proof-shell-compute-new-files-list 'isar-shell-compute-new-files-list
-   ;; span menu 
+   ;; span menu
    proof-script-span-context-menu-extensions 'isabelle-create-span-menu))
 
 (defun isar-shell-mode-config-set-variables ()
@@ -189,7 +192,7 @@ See -k option for Isabelle interface script."
    proof-shell-eager-annotation-start-length 1
    proof-shell-eager-annotation-start   "\360\\|\362\\|\^AI\\|\^AK"
    proof-shell-eager-annotation-end     "\361\\|\363\\|\^AJ\\|\^AL"
-   ;; see isar-pre-shell-start for proof-shell-trace-output-regexp
+   proof-shell-trace-output-regexp	"\375\\|\^AV"
 
    ;; Isabelle is learning to talk PGIP...
    proof-shell-match-pgip-cmd		"<pgip"
@@ -203,7 +206,7 @@ See -k option for Isabelle interface script."
    proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\\(\361\\|\^AJ\\)"
    proof-shell-theorem-dependency-list-split "\" \""
    proof-shell-show-dependency-cmd "thm %s;"
-   proof-shell-identifier-under-mouse-cmd 
+   proof-shell-identifier-under-mouse-cmd
    '((nil     "thm %s;")
      (string  "term \"%s\";")
      (comment "term \"%s\";"))
@@ -218,7 +221,7 @@ See -k option for Isabelle interface script."
      ;; next string could be: "[\350-\377]", but that's buggy with XEmacs 21.5 (beta)
      "×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|8\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ")
 
-   pg-subterm-help-cmd			"term %s" 
+   pg-subterm-help-cmd			"term %s"
 
    proof-cannot-reopen-processed-files  t
    proof-shell-process-file
@@ -295,7 +298,7 @@ proof-shell-retract-files-regexp."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ;;;
-;;; help menu  
+;;; help menu
 ;;;
 
 ;;; da: how about a `C-c C-a h ?' for listing available keys?
@@ -320,15 +323,15 @@ proof-shell-retract-files-regexp."
 ;; Command menu
 ;;
 
-;; NB: would be nice to query save of the buffer first for these 
+;; NB: would be nice to query save of the buffer first for these
 ;; next two: but only convenient emacs functions offer save for
 ;; all buffers.
 (proof-definvisible isar-cmd-display-draft
  '(format "display_drafts \"%s\"" buffer-file-name)
  [(control d)])
 
-(proof-definvisible isar-cmd-print-draft 
-  '(if (y-or-n-p 
+(proof-definvisible isar-cmd-print-draft
+  '(if (y-or-n-p
 	(format "Print draft of file %s ?" buffer-file-name))
        (format "print_drafts \"%s\"" buffer-file-name)
      (error "Aborted."))
@@ -369,7 +372,7 @@ proof-shell-retract-files-regexp."
 
 ;; undo proof commands
 (defun isar-count-undos (span)
-  "Count number of undos in a span, return the command needed to undo that far."
+  "Count number of undos SPAN, return command needed to undo that far."
   (let
       ((case-fold-search nil)       ;FIXME ??
        (ct 0) str i)
@@ -379,7 +382,7 @@ proof-shell-retract-files-regexp."
              (or (proof-string-match isar-undo-skip-regexp str)
 		 (proof-string-match isar-undo-ignore-regexp str)
                  (setq ct (+ 1 ct))))
-            ((eq (span-property span 'type) 'pbp)  
+            ((eq (span-property span 'type) 'pbp)
              ;; this case for automatically inserted text (e.g. sledgehammer)
              (cond ((not (proof-string-match isar-undo-skip-regexp str))
 		    (setq ct 1)
@@ -404,7 +407,7 @@ proof-shell-retract-files-regexp."
       (cond
        ;; comment, diagnostic, nested proof command: skip
        ;; (da: adding new span types may break this code,
-       ;;  ought to test for type 'cmd before looking at 
+       ;;  ought to test for type 'cmd before looking at
        ;;  str below)
        ;; FIXME: should adjust proof-nesting-depth here.
        ((or (eq (span-property span 'type) 'comment)
@@ -434,15 +437,13 @@ proof-shell-retract-files-regexp."
       (if span (setq span (next-span span 'type))))
     (if (null answers) proof-no-command (apply 'concat answers))))
 
-
-
 (defun isar-goal-command-p (span)
-  "Decide whether argument is a goal or not"
-  (proof-string-match isar-goal-command-regexp 
+  "Decide whether argument SPAN is a goal or not."
+  (proof-string-match isar-goal-command-regexp
 		      (or (span-property span 'cmd) "")))
 
 (defun isar-global-save-command-p (span str)
-  "Decide whether argument really is a global save command"
+  "Decide whether argument SPAN with command STR is a global save command."
   (or
    (proof-string-match isar-global-save-command-regexp str)
    (let ((ans nil) (lev 0) cmd)
@@ -463,10 +464,10 @@ proof-shell-retract-files-regexp."
      (eq ans 'yes))))
 
 (defvar isar-current-goal 1
-  "Last goal that emacs looked at.")
+  "Last goal that Emacs looked at.")
 
 (defun isar-state-preserving-p (cmd)
-  "Non-nil if command preserves the proofstate."
+  "Non-nil if command CMD preserves the proofstate."
   (proof-string-match isar-undo-skip-regexp cmd))
 
 
@@ -489,13 +490,11 @@ proof-shell-retract-files-regexp."
 ;;   Isar shell startup and exit hooks                              ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;borrowed from plastic.el
 (defvar isar-shell-current-line-width nil
   "Current line width of the Isabelle process's pretty printing module.
 Its value will be updated whenever the corresponding screen gets
 selected.")
 
-;borrowed from plastic.el
 (defun isar-shell-adjust-line-width ()
   "Use Isabelle's pretty printing facilities to adjust output line width.
 Checks the width in the `proof-goals-buffer'"
@@ -505,9 +504,8 @@ Checks the width in the `proof-goals-buffer'"
          (save-excursion
            (set-buffer proof-goals-buffer)
            (let ((current-width
-                  ;; Actually, one might sometimes
-                  ;; want to get the width of the proof-response-buffer
-                  ;; instead. Never mind.
+                  ;; Actually, one might want the width of the
+                  ;; proof-response-buffer instead. Never mind.
                   (max 20 (window-width (get-buffer-window proof-goals-buffer t)))))
 
              (if (equal current-width isar-shell-current-line-width) ()
@@ -516,20 +514,12 @@ Checks the width in the `proof-goals-buffer'"
                (setq ans (format "pretty_setmargin %d;" (- current-width 4)))))))
     ans))
 
-(defun isar-pre-shell-start ()
-  (setq proof-prog-name         (isabelle-command-line))
-  (setq proof-mode-for-shell    'isar-shell-mode)
-  (setq proof-mode-for-goals    'isar-goals-mode)
-  (setq proof-mode-for-response 'isar-response-mode)
-  (setq proof-shell-trace-output-regexp "\375\\|\^AV"))
-
-
 ;;
 ;;   Configuring proof output buffer
 ;;
 
 (defun isar-preprocessing ()  ;dynamic scoping of `string'
-  "Insert sync markers - acts on variable STRING by dynamic scoping"
+  "Insert sync markers - acts on variable STRING by dynamic scoping."
   (if (proof-string-match isabelle-verbatim-regexp string)
       (setq string (match-string 1 string))
     (unless (proof-string-match ";[ \t]*\\'" string)
@@ -556,18 +546,17 @@ Checks the width in the `proof-goals-buffer'"
   (isar-init-syntax-table)
   (setq font-lock-keywords isar-font-lock-keywords-1)
   (setq comment-quote-nested nil) ;; can cope with nested comments
-  (proof-config-done)
   (set (make-local-variable 'outline-regexp) isar-outline-regexp)
   (set (make-local-variable 'outline-heading-end-regexp) isar-outline-heading-end-regexp)
   (setq blink-matching-paren-dont-ignore-comments t)
-  (add-hook 'proof-pre-shell-start-hook 'isar-pre-shell-start nil t)
-  (add-hook 'proof-shell-insert-hook 'isar-preprocessing))
+  (add-hook 'proof-shell-insert-hook 'isar-preprocessing)
+  (proof-config-done))
 
 (defun isar-shell-mode-config ()
   "Configure Proof General proof shell for Isabelle/Isar."
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords  
-	(append 
+  (setq font-lock-keywords
+	(append
 	 isar-output-font-lock-keywords-1
 	 (if (boundp 'x-symbol-isar-font-lock-keywords)
 	     x-symbol-isar-font-lock-keywords)))
@@ -576,10 +565,10 @@ Checks the width in the `proof-goals-buffer'"
 
 (defun isar-response-mode-config ()
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords  
-	(append 
+  (setq font-lock-keywords
+	(append
 	 isar-output-font-lock-keywords-1
-	 (if (proof-ass x-symbol-enable)
+	 (if isar-x-symbol-enable
 	     x-symbol-isar-font-lock-keywords)))
   (proof-response-config-done))
 
@@ -587,31 +576,23 @@ Checks the width in the `proof-goals-buffer'"
   (setq pg-goals-change-goal "prefer %s")
   (setq pg-goals-error-regexp proof-shell-error-regexp)
   (isar-init-output-syntax-table)
-  (setq font-lock-keywords  
-	(append 
+  (setq font-lock-keywords
+	(append
 	 isar-goals-font-lock-keywords
-	 (if (proof-ass x-symbol-enable)
+	 (if isar-x-symbol-enable
 	     x-symbol-isar-font-lock-keywords)))
   (proof-goals-config-done))
 
 (defun isar-goalhyplit-test ()
   "Value for `pg-topterm-goalhyplit-fn' (see that variable for documentation)."
   (let ((start (point)))
-    (if (proof-re-search-forward "\377\\|\^AX" nil t) ;; end of literal command (non-standard)
+    (if (proof-re-search-forward
+	 "\377\\|\^AX" nil t) ; end of literal command (non-standard)
 	(progn
 	  (delete-region (match-beginning 0) (match-end 0))
 	  (cons 'lit (buffer-substring start (match-beginning 0)))))))
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Remove isa-mode from auto-mode-alist, 
-;; to allow SML mode to work in preference to isa-mode.
-;;
-
-(setq auto-mode-alist
-      (delete-if 
-       (lambda (strmod) (memq (cdr strmod) '(demoisa-mode)))
-       auto-mode-alist))
-
 (provide 'isar)
+
+;;; isar.el ends here
diff --git a/isar/x-symbol-isar.el b/isar/x-symbol-isar.el
index 4f61d702..9bb3c28e 100644
--- a/isar/x-symbol-isar.el
+++ b/isar/x-symbol-isar.el
@@ -505,10 +505,10 @@ variable `x-symbol-auto-coding-alist' for details."
 ;;
 
 (eval-after-load "isar" ;; allow use outside PG
-  (setq 
-   proof-xsym-activate-command
-   (isar-markup-ml "change print_mode (insert (op =) \"xsymbols\")")
-   proof-xsym-deactivate-command
-   (isar-markup-ml "change print_mode (remove (op =) \"xsymbols\")")))
+  '(setq 
+    proof-xsym-activate-command
+    (isar-markup-ml "change print_mode (insert (op =) \"xsymbols\")")
+    proof-xsym-deactivate-command
+    (isar-markup-ml "change print_mode (remove (op =) \"xsymbols\")")))
 
 (provide 'x-symbol-isar)