Re: [isabelle] [install] font-problem



You're probably using an unsupported version of XEmacs that has BETA VERSION stamped on the splash screen? You'll have worse problems than this with recent betas that have been put into Linux distros: I regularly have segfaults during Dired sessions and buffer save C-x C-s sometimes saves empty files. GNU Emacs gives a better experience these days.

This problem turns out to be because a regular expression match replacement fails (even though the match succeeds; presumably a bug in the regexp engine). Here's a new version of isar.el which has a clumsy workaround. There will be a new development version of PG available soon which includes it.

 - David.


Sven Schneider wrote:
Hey,

I have a little problem:
in the *goal* Buffer every variable has an additional
prefix and an additional postfix.

If the variable is colored green then
the prefix is an i with an accent aigu and
the postfix is an e with an accent grave.

If the variable is colored blue then
both accents are accent grave.

This seems to be some font-problem.

I would appreciate any help to resolve this problem!

bye!

Sven


; 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
;;
;; Authors:       David Aspinall <David.Aspinall at ed.ac.uk>
;;   	          Markus Wenzel <wenzelm at in.tum.de>
;;
;; Contributors:  David von Oheimb, Sebastian Skalberg
;;
;;
;; $Id: isar.el,v 8.29 2007/03/03 15:28:20 da Exp $
;;

(require 'proof)

;; System code
(require 'isabelle-system)

;;
;; Load syntax
;;
(defcustom isar-keywords-name nil
  "Specifies a theory-specific keywords setting to use with Isar.
See -k option for Isabelle interface script."
  :type 'string
  :group 'isabelle-isar)

(or (featurep 'isar-keywords)
    ;; 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 
     (or isar-keywords-name
	 isabelle-chosen-logic)))
(require 'isar-syntax)


;; Completion table for Isabelle/Isar identifiers
(defpgdefault completion-table isar-keywords-major)

(defcustom isar-web-page
  "http://isabelle.in.tum.de/Isar/";
  "URL of web page for Isabelle/Isar."
  :type 'string
  :group 'isabelle-isar)


;; 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))))


(defun isar-strip-terminators ()
  "Remove explicit Isabelle/Isar command terminators `;' from the buffer."
  (interactive)
  (save-excursion
    (goto-char (point-min))
    (while (proof-search-forward ";" (point-max) t)
      (if (not (proof-buffer-syntactic-context))
	  (progn
	    (delete-backward-char 1)
	    (or (proof-looking-at ";\\|\\s-\\|$")
		(insert " ")))))))


(defun isar-markup-ml (string)
  "Return marked up version of ML command STRING for Isar."
  (format "ML_command {* %s *};" string))


(defun isar-mode-config-set-variables ()
  "Configure generic proof scripting mode variables for Isabelle/Isar."
  (setq
   proof-assistant-home-page    isar-web-page
   proof-mode-for-script        'isar-mode
   ;; proof script syntax
   proof-terminal-char          ?\;     ; forcibly ends a command
   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
   proof-script-comment-start          isar-comment-start
   proof-script-comment-end            isar-comment-end
   proof-script-comment-start-regexp   isar-comment-start-regexp
   proof-script-comment-end-regexp     isar-comment-end-regexp
   proof-string-start-regexp    isar-string-start-regexp
   proof-string-end-regexp      isar-string-end-regexp

   ;; Next few used for func-menu and recognizing goal..save regions in
   ;; script buffer.
   proof-save-command-regexp    isar-save-command-regexp
   proof-goal-command-regexp    isar-goal-command-regexp
   proof-goal-with-hole-regexp  isar-named-entity-regexp
   proof-goal-with-hole-result	2
   proof-save-with-hole-regexp  nil
   proof-script-next-entity-regexps isar-next-entity-regexps
   proof-script-imenu-generic-expression isar-generic-expression
   imenu-syntax-alist isar-script-syntax-table-alist

   proof-indent-enclose-offset  (- proof-indent)
   proof-indent-open-offset     0
   proof-indent-close-offset    0
   proof-indent-any-regexp      isar-indent-any-regexp
;   proof-indent-inner-regexp    isar-indent-inner-regexp
   proof-indent-enclose-regexp  isar-indent-enclose-regexp
   proof-indent-open-regexp     isar-indent-open-regexp
   proof-indent-close-regexp    isar-indent-close-regexp

   ;; proof engine commands
   proof-showproof-command      "pr"
   proof-goal-command           "lemma \"%s\""
   proof-save-command           "qed"
   proof-context-command        "print_context"
   proof-info-command           "welcome"
   proof-kill-goal-command      "ProofGeneral.kill_proof"
   proof-find-theorems-command  "find_theorems %s"
   proof-shell-start-silent-cmd "disable_pr"
   proof-shell-stop-silent-cmd  "enable_pr"
   ;; command hooks
   proof-goal-command-p         'isar-goal-command-p
   proof-really-save-command-p  'isar-global-save-command-p
   proof-count-undos-fn         'isar-count-undos
   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 
   proof-script-span-context-menu-extensions 'isabelle-create-span-menu))


(defun isar-shell-mode-config-set-variables ()
  "Configure generic proof shell mode variables for Isabelle/Isar."
  (setq
   pg-subterm-first-special-char	?\350
   proof-shell-wakeup-char              nil
   proof-shell-annotated-prompt-regexp  "^\\w*[>#] \372\\|^\\w*[>#] \^AS"

   ;; This pattern is 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\"")

   ;; Escapes for filenames inside ML strings.
   ;; We also make a hack for a bug in Isabelle, by switching from
   ;; backslashes to forward slashes if it looks like we're running
   ;; on Windows.
   proof-shell-filename-escapes
   (if (fboundp 'win32-long-filename)   ; rough test for XEmacs on win32
       ;; Patterns to unixfy names.
       ;; Jacques Fleuriot's patch in ML does this too: ("^[a-zA-Z]:" . "")
       ;; But I'll risk leaving drive names in, not sure how to replace them.
       '(("\\\\" . "/") ("\"" . "\\\""))
     ;; Normal case: quotation for backslash, quote mark.
     '(("\\\\" . "\\\\") ("\""   . "\\\"")))

   proof-shell-proof-completed-regexp   nil     ; n.a.
   proof-shell-interrupt-regexp         "\364\\*\\*\\* Interrupt\\|\^AM\\*\\*\\* Interrupt"
   proof-shell-error-regexp             "\364\\*\\*\\*\\|\^AM\\*\\*\\*"
   proof-shell-abort-goal-regexp        nil     ; n.a.

   ;; 
   pg-next-error-regexp	  "\\((line \\([0-9]+\\) of \"[^\"]+\")\\)"
   pg-next-error-filename-regexp "\\((line [0-9]+ of \"\\([^\"]+\\)\")\\)"

   ;; matches names of assumptions
   proof-shell-assumption-regexp        isar-id

   proof-shell-start-goals-regexp       "\366\n\\|\^AO\n"
   proof-shell-end-goals-regexp         "\367\\|\^AP"

   ;; FIXME: next one is needed for backward compatibility.  
   ;; Would be nice to remove this somehow else, it's only used for 
   ;; Isar and pre-PGIP.  One way would be to hack the 
   ;; (now obsolete) defpacustom calls.
   proof-assistant-setting-format       
   (unless isa-supports-pgip 'isar-markup-ml)

   proof-shell-init-cmd			nil
   proof-shell-restart-cmd              "ProofGeneral.restart"

   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

   ;; Isabelle is learning to talk PGIP...
   proof-shell-match-pgip-cmd		"<pgip"
   proof-shell-issue-pgip-cmd		
	(if isa-supports-pgip 'isabelle-process-pgip nil)

   ;; 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 \"\\(.*\\)\"\\(\361\\|\^AJ\\)"
   proof-shell-theorem-dependency-list-split "\" \""
   proof-shell-show-dependency-cmd "thm %s;"
   proof-shell-identifier-under-mouse-cmd 
   '((nil     "thm %s;")
     (string  "term \"%s\";")
     (comment "term \"%s\";"))

   ;; Allow font-locking for output based on hidden annotations, see
   ;; isar-output-font-lock-keywords-1
   pg-use-specials-for-fontify		t
   pg-special-char-regexp               ;; should be: "[\200-\377]\\|\^A[A-Z]"
   ;; da: the character range here fails to match (actually, fails
   ;; to match-replace) in xemacs 21.5 betas, so I'm listing the 
   ;; characters instead, which works.
   ;; This should probably be tuned to the ones actually used by Isabelle
   "?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\|?\\| \\|¡\\|¢\\|£\\|¤\\|¥\\|¦\\|§\\|¨\\|©\\|ª\\|«\\|¬\\|­\\|®\\|¯\\|°\\|±\\|²\\|³\\|´\\|µ\\|¶\\|·\\|¸\\|¹\\|º\\|»\\|¼\\|½\\|¾\\|¿\\|À\\|Á\\|Â\\|Ã\\|Ä\\|Å\\|Æ\\|Ç\\|È\\|É\\|Ê\\|Ë\\|Ì\\|Í\\|Î\\|Ï\\|Ð\\|Ñ\\|Ò\\|Ó\\|Ô\\|Õ\\|Ö\\|×\\|Ø\\|Ù\\|Ú\\|Û\\|Ü\\|Ý\\|Þ\\|ß\\|à\\|á\\|â\\|ã\\|ä\\|å\\|æ\\|ç\\|è\\|é\\|ê\\|ë\\|ì\\|í\\|î\\|ï\\|ð\\|ñ\\|ò\\|ó\\|ô\\|õ\\|ö\\|÷\\|ø\\|ù\\|ú\\|û\\|ü\\|ý\\|þ\\|ÿ\\|[A-Z]"
   pg-after-fontify-output-hook	        'pg-remove-specials
   pg-subterm-help-cmd			"term %s" 

   proof-cannot-reopen-processed-files  t
   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 \"\\(.*\\)\""
   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\"")
  (add-hook 'proof-activate-scripting-hook 'isar-activate-scripting))


;;;
;;; Theory loader operations
;;;

(defun isar-remove-file (name files cmp-base)
  (if (not files) nil
    (let*
        ((file (car files))
         (rest (cdr files))
         (same (if cmp-base (string= name (file-name-nondirectory file))
                 (string= name file))))
      (if same (isar-remove-file name rest cmp-base)
        (cons file (isar-remove-file name rest cmp-base))))))

(defun isar-shell-compute-new-files-list (str)
  "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))
       (base-name (file-name-nondirectory name)))
    (if (string= name base-name)
        (isar-remove-file name proof-included-files-list t)
      (isar-remove-file (file-truename name) proof-included-files-list nil))))

(defun isar-activate-scripting ()
  "Make sure the Isabelle/Isar toplevel is in a sane state."
  (proof-cd-sync))


;;
;;   Define the derived modes
;;
(eval-and-compile
(define-derived-mode isar-shell-mode proof-shell-mode
   "Isar shell" nil
   (isar-shell-mode-config)))

(eval-and-compile
(define-derived-mode isar-response-mode proof-response-mode
  "response" nil
  (isar-response-mode-config)))

(eval-and-compile                       ; to define vars for byte comp.
(define-derived-mode isar-goals-mode proof-goals-mode
  "proofstate" nil
  (isar-goals-mode-config)))

(eval-and-compile                       ; to define vars for byte comp.
(define-derived-mode isar-mode proof-mode
  "Isar script" nil
  (isar-mode-config)))



;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   Code that's Isabelle/Isar specific                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;;;
;;; help menu  
;;;

;;; da: how about a `C-c C-a h ?' for listing available keys?

;;; NB: definvisible must come after derived modes because uses
;;; isar-mode-map
(proof-definvisible isar-help-antiquotations "print_antiquotations" [h A])
(proof-definvisible isar-help-attributes "print_attributes" [h a])
(proof-definvisible isar-help-cases "print_cases" [h c])
(proof-definvisible isar-help-claset "print_claset" [h C])
(proof-definvisible isar-help-commands "print_commands" [h o])
(proof-definvisible isar-help-facts "print_facts" [h f])
(proof-definvisible isar-help-syntax "print_syntax" [h i])
(proof-definvisible isar-help-induct-rules "print_induct_rules" [h I])
(proof-definvisible isar-help-methods "print_methods" [h m])
(proof-definvisible isar-help-simpset "print_simpset" [h S])
(proof-definvisible isar-help-binds "print_binds" [h b])
(proof-definvisible isar-help-theorems "print_theorems" [h t])
(proof-definvisible isar-help-trans-rules "print_trans_rules" [h T])

;;
;; Command menu
;;

;; 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 
	(format "Print draft of file %s ?" buffer-file-name))
       (format "print_drafts \"%s\"" buffer-file-name)
     (error "Aborted."))
  [(control p)])

(proof-definvisible isar-cmd-refute	"refute" [r])
(proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])

(defpgdefault menu-entries
  (append
   (list isabelle-logics-menu)
   (list
    (cons "Commands"
          (list
           ["refute"             isar-cmd-refute         t]
           ["quickcheck"         isar-cmd-quickcheck     t]
	   ["display draft"	 isar-cmd-display-draft  t])))
   (list
    (cons "Show me ..."
          (list
           ["cases"              isar-help-cases          t]
           ["facts"              isar-help-facts          t]
           ["term bindings"      isar-help-binds          t]
	   "----"
           ["classical rules"    isar-help-claset         t]
           ["induct/cases rules" isar-help-induct-rules   t]
           ["simplifier rules"   isar-help-simpset        t]
           ["theorems"           isar-help-theorems       t]
           ["transitivity rules" isar-help-trans-rules    t]
	   "----"
           ["antiquotations"     isar-help-antiquotations t]
           ["attributes"         isar-help-attributes     t]
           ["commands"           isar-help-commands       t]
           ["inner syntax"       isar-help-syntax         t]
           ["methods"            isar-help-methods        t])))))

;; undo proof commands
(defun isar-count-undos (span)
  "Count number of undos in a span, return the command needed to undo that far."
  (let
      ((case-fold-search nil)       ;FIXME ??
       (ct 0) str i)
    (while span
      (setq str (or (span-property span 'cmd) ""))
      (cond ((eq (span-property span 'type) 'vanilla)
             (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)  ;FIXME dead code?
             ;; this case probably redundant for Isabelle, unless
             ;; we think of some nice ways of matching non-undoable
             ;; commands.
             (cond ((not (proof-string-match isar-undo-skip-regexp str))
                    (setq i 0)
                    (while (< i (length str))
                      (if (= (aref str i) proof-terminal-char)
                          (setq ct (+ 1 ct)))
                      (setq i (+ 1 i))))
                   (t nil))))
      (setq span (next-span span 'type)))
    (isar-undos ct)))

;; begin keyword
(defun isar-detect-begin (span)
  "Detect the begin keyword within a command span"
  (let ((found nil)
	(start (span-start span))
	(end (span-end span)))
    (save-excursion
      (goto-char start)
      (while (and (not found) (proof-search-forward isar-keyword-begin end t))
	(or (proof-buffer-syntactic-context) (setq found t))))
    found))

;; command nesting
(defun isar-command-nested (span)
  "Determine theory command nesting"
  (let ((nesting 0) str)
    (while span
      (setq str (or (span-property span 'cmd) ""))
      (cond
       ;; end
       ((proof-string-match isar-end-regexp str)
	(decf nesting))
       ;; begin
       ((or (proof-string-match isar-theory-start-regexp str)
	    (isar-detect-begin span))
	(incf nesting)))
      (setq span (prev-span span 'type)))
    (> nesting 0)))

;; undo theory commands
(defun isar-find-and-forget (span)
  "Return commands to be used to forget SPAN."
  (let (str ans answers)
    (while span
      (setq str (or (span-property span 'cmd) ""))
      (setq ans nil)
      (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 
       ;;  str below)
       ;; FIXME: should adjust proof-nesting-depth here.
       ((or (eq (span-property span 'type) 'comment)
	    (eq (span-property span 'type) 'proverproc)
	    (eq (span-property span 'type) 'proof); da: needed?
            (proof-string-match isar-undo-skip-regexp str)
            (proof-string-match isar-undo-ignore-regexp str)))
       ;; finished goal: undo
       ((eq (span-property span 'type) 'goalsave)
        (setq ans isar-undo))
       ;; open goal: skip and exit
       ((proof-string-match isar-goal-command-regexp str)
        (setq span nil))
       ;; nested end: undo
       ((and (proof-string-match isar-end-regexp str)
	     (isar-command-nested span))
        (setq ans isar-undo))
       ;; not undoable: fail and exit 
       ;; [da: this is an odd case: it issues cannot_undo command to Isar,
       ;;  which immediately generates an error, I think it's a bit confusing
       ;; for the user]
       ((and (proof-string-match isar-undo-fail-regexp str))
        (setq answers nil)
        (setq ans (isar-cannot-undo str))
        (setq span nil))
       ;; theory: remove and exit
       ((proof-string-match isar-undo-remove-regexp str)
        (setq ans (isar-remove (match-string 2 str)))
        (setq span nil))
       ;; else: undo
       (t
        (setq ans isar-undo)))
      (if ans (setq answers (cons ans answers)))
      (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 
		      (or (span-property span 'cmd) "")))

(defun isar-global-save-command-p (span str)
  "Decide whether argument really is a global save command"
  (or
   (proof-string-match isar-global-save-command-regexp str)
   (let ((ans nil) (lev 0) cmd)
     (while (and (not ans) span (setq span (prev-span span 'type)))
       (setq cmd (or (span-property span 'cmd) ""))
       (cond
        ;; comment: skip
        ((eq (span-property span 'type) 'comment))
        ;; local qed: enter block
        ((proof-string-match isar-save-command-regexp cmd)
         (setq lev (+ lev 1)))
        ;; local goal: leave block, or done
        ((proof-string-match isar-local-goal-command-regexp cmd)
         (if (> lev 0) (setq lev (- lev 1)) (setq ans 'no)))
        ;; global goal: done
        ((proof-string-match isar-goal-command-regexp cmd)
         (setq ans 'yes))))
     (eq ans 'yes))))

(defvar isar-current-goal 1
  "Last goal that emacs looked at.")

(defun isar-state-preserving-p (cmd)
  "Non-nil if command preserves the proofstate."
  (proof-string-match isar-undo-skip-regexp cmd))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   Commands specific to isar                                      ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(proof-defshortcut isar-bold      "\\<^bold>%p" [(control b)])
(proof-defshortcut isar-local     "\\<^loc>%p" [(control c)])
(proof-defshortcut isar-super     "\\<^sup>%p" [(control u)])
(proof-defshortcut isar-sub       "\\<^sub>%p" [(control l)])
(proof-defshortcut isar-longsuper "\\<^bsup>%p\\<^esup>" [u])
(proof-defshortcut isar-longsub   "\\<^bsub>%p\\<^esub>" [l])
(proof-defshortcut isar-idsub     "\\<^isub>%p" [(control i)])
(proof-defshortcut isar-raw       "\\<^raw:%p>" [(control r)])
(proof-defshortcut isar-antiquote "@{text \"%p\"}" [(control a)])


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;   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'"
  (let ((ans ""))
    (and (buffer-live-p proof-goals-buffer)
         (proof-shell-live-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.
                  (max 20 (window-width (get-buffer-window proof-goals-buffer t)))))

             (if (equal current-width isar-shell-current-line-width) ()
               (setq isar-shell-current-line-width current-width)
               (set-buffer proof-shell-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"
  (if (proof-string-match isabelle-verbatim-regexp string)
      (setq string (match-string 1 string))
    (unless (proof-string-match ";[ \t]*\\'" string)
      (setq string (concat string ";")))
    (setq string (concat
                  "\\<^sync>"
                  (isar-shell-adjust-line-width)
                  ;; da: this was an attempted hack to deal with ML files,
                  ;; unfortunately Isar complains about not seeing a theory
                  ;; command first: ML_setup illegal at first line
                  ;; Another failure is that: (* comment *) foo;
                  ;; ignores foo.  This could be fixed by scanning for
                  ;; comment end in proof-script.el's function
                  ;; proof-segment-upto-cmdstart (which becomes even more
                  ;; Isar specific, then...)
                  ;; (if (proof-string-match "\\.ML$" (buffer-name proof-script-buffer))
                  ;;    (format "ML_command {* %s *};" string)
                  ;;    string)
                  (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string)
                  " \\<^sync>;"))))

(defun isar-mode-config ()
  (isar-mode-config-set-variables)
  (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))

(defun isar-shell-mode-config ()
  "Configure Proof General proof shell for Isabelle/Isar."
  (isar-init-output-syntax-table)
  (setq font-lock-keywords  
	(append 
	 isar-output-font-lock-keywords-1
	 (if (boundp 'x-symbol-isabelle-font-lock-keywords)
	     x-symbol-isabelle-font-lock-keywords)))
  (isar-shell-mode-config-set-variables)
  (proof-shell-config-done))

(defun isar-response-mode-config ()
  (isar-init-output-syntax-table)
  (setq font-lock-keywords  
	(append 
	 isar-output-font-lock-keywords-1
	 (if (proof-ass x-symbol-enable)
	     x-symbol-isabelle-font-lock-keywords)))
  (proof-response-config-done))

(defun isar-goals-mode-config ()
  ;; FIXME: next two broken, of course, as is PBP everywhere except LEGO.
  (setq pg-goals-change-goal "show %s.")
  (setq pg-goals-error-regexp proof-shell-error-regexp)
  (isar-init-output-syntax-table)
  (setq font-lock-keywords  
	(append 
	 isar-goals-font-lock-keywords
	 (if (proof-ass x-symbol-enable)
	     x-symbol-isabelle-font-lock-keywords)))
  (proof-goals-config-done))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; 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) '(isa-mode demoisa-mode)))
       auto-mode-alist))

(provide 'isar)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.