diff options
Diffstat (limited to 'isa/thy-mode.el')
| -rw-r--r-- | isa/thy-mode.el | 1045 |
1 files changed, 1045 insertions, 0 deletions
diff --git a/isa/thy-mode.el b/isa/thy-mode.el new file mode 100644 index 00000000..2bd64345 --- /dev/null +++ b/isa/thy-mode.el @@ -0,0 +1,1045 @@ +;; thy-mode.el - Mode for Isabelle theory files. +;; +;; Copyright (C) 1998 LFCS Edinburgh. +;; Author: David Aspinall <da@dcs.ed.ac.uk> +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; +;; Taken from Isamode, version: 3.6 1998/09/02 11:40:45 +;; +;; $Id$ +;; +;; NAMESPACE management: all functions and variables declared +;; in this file begin with isa-thy- + +(require 'proof-site) +(require 'proof-syntax) +(require 'isa) + +;; In case thy mode was invoked directly or by -*- thy -*- at +;; the start of the file, ensure that Isar mode is used from now +;; on for .thy files. +;; FIXME: be less messy with auto-mode-alist here (remove dups) +(setq auto-mode-alist + (cons '("\\.thy$" . thy-mode) auto-mode-alist)) + +;;; ========== Theory File Mode User Options ========== + +(defcustom thy-heading-indent 0 + "Indentation for section headings." + :type 'integer + :group 'thy) + +(defcustom thy-indent-level 2 + "*Indentation level for Isabelle theory files. An integer." + :type 'integer + :group 'thy) + +(defcustom thy-indent-strings t + "If non-nil, indent inside strings. +You may wish to disable indenting inside strings if your logic uses +any of the usual bracket characters in unusual ways." + :type 'boolean + :group 'thy) + +(defcustom thy-use-sml-mode nil + "*If non-nil, invoke sml-mode inside \"ML\" section of theory files. +This option is left-over from Isamode. Really, it would be more +useful if the script editing mode of Proof General itself could be based +on sml-mode, but at the moment there is no way to do this." + :type 'boolean + :group 'thy) + + +;;; ====== Theory and ML file templates ========================= + +(defcustom thy-sections + ;; NB: preceding white space in templates deleted by indentation alg. + ;; top must come first. + '(("top" . thy-insert-header) + ("classes" . thy-insert-class) + ("default" . thy-insert-default-sort) ; is "default" obsolete? + ("defaultsort" . thy-insert-default-sort) + ("types" . thy-insert-type) + ("typedecl") + ("arities" . thy-insert-arity) + ;; ================================= + ;; These only make sense for HOL. + ;; Ideally we should parameterise these parts on the theory. + ("datatype") ("typedef") + ("inductive") ("coninductive") + ("intrs") ("monos") + ("primrec") ("recdef") + ("rep_datatype") ("distinct") ("induct") + ;; ============================== + ("consts" . thy-insert-const) + ("translations" . "\"\"\t==\t\"\"") + ("axclass") + ("syntax") + ("instance") + ("rules" . thy-insert-rule) + ("defs" . thy-insert-rule) + ("axioms" . thy-insert-rule) + ("use") + ("theory") + ("files") + ("constdefs") + ("oracle") + ("local") + ("locale") + ("nonterminals") + ("setup") + ("global") + ("end") + ("ML")) + "Names of theory file sections and their templates. +Each item in the list is a pair of a section name and a template. +A template is either a string to insert or a function. Useful functions are: + thy-insert-header, thy-insert-class, thy-insert-default-sort, + thy-insert-const, thy-insert-rule. +The nil template does nothing. +You can add extra sections to theory files by extending this variable." + :type '(repeat + (cons string + (choice function + string + (const :tag "no template" nil)))) + :group 'thy) + +(defcustom thy-id-header + "(* + File: %f + Theory Name: %t + Logic Image: %l +*)\n\n" + "*Identification header for .thy and .ML files. +Format characters: %f replaced by filename, %t by theory name, +and %l by the logic image name this file should be read in." + :group 'thy + :type 'string) + +(defcustom thy-template +"%t = %p +\n +classes\n +default\n +types\n +arities\n +consts\n +translations\n +rules\n +end\n +ML\n" +"Template for theory files. +Contains a default selection of sections in a traditional order. +You can use the following format characters: + +`%t' --- replaced by theory name. + +`%p' --- replaced by names of parents, separated by `+' characters." + :group 'thy + :type 'string) + + + +;;; ========== Code ========== + +(defvar thy-mode-map nil) + +(defvar thy-mode-syntax-table nil) ; Shared below. + +(if thy-mode-syntax-table + nil + ;; This is like sml-mode, except: + ;; . is a word constituent (not punctuation). (bad for comments?) + ;; " is a paired delimiter + (setq thy-mode-syntax-table (make-syntax-table)) + (modify-syntax-entry ?\( "()1 " thy-mode-syntax-table) + (modify-syntax-entry ?\) ")(4 " thy-mode-syntax-table) + (modify-syntax-entry ?\\ "\\ " thy-mode-syntax-table) + (modify-syntax-entry ?* ". 23" thy-mode-syntax-table) + (modify-syntax-entry ?_ "w " thy-mode-syntax-table) + (modify-syntax-entry ?\' "w " thy-mode-syntax-table) +; it's annoying to match with quotes from previous strings, +; so this has been removed. +; (modify-syntax-entry ?\" "$ " thy-mode-syntax-table) + (modify-syntax-entry ?. "w " thy-mode-syntax-table)) + +(or thy-mode-map + (let ((map (make-sparse-keymap))) + (define-key map [(control up)] 'thy-goto-prev-section) + (define-key map [(control down)] 'thy-goto-next-section) + (define-key map "\C-c\C-n" 'thy-goto-next-section) + (define-key map "\C-c\C-p" 'thy-goto-prev-section) + (define-key map "\C-c\C-m" 'thy-minor-sml-mode) + (define-key map "\C-c\C-t" 'thy-insert-template) + ;; Disabled for Proof General + ;;(define-key map "\C-c\C-u" 'thy-use-file) + ;;(define-key map "\C-c\C-l" 'thy-raise-windows) + (define-key map "\C-c\C-o" 'thy-find-other-file) + (define-key map "\C-M" 'newline-and-indent) + (define-key map "\C-k" 'thy-kill-line) + (setq thy-mode-map map))) + +(defun thy-add-menus (&optional file) + "Add Proof General and Isabelle menu to current menu bar." + (require 'proof-script) ; Later: proof-menu, autoloaded + (easy-menu-define thy-mode-pg-menu + thy-mode-map + "PG Menu for Isabelle Proof General" + (cons proof-general-name + (append + (list + ;; A couple from the toolbar that make sense here + ;; (also in proof-universal-keys) + ["Issue command" proof-minibuffer-cmd t] + ["Interrupt prover" proof-interrupt-process t]) + (list proof-buffer-menu) + (list proof-help-menu)))) + (easy-menu-define thy-mode-isa-menu + thy-mode-map + "Menu for Isabelle Proof General, theory file mode." + (cons "Theory" + (list + ["Next Section" thy-goto-next-section t] + ["Prev Section" thy-goto-prev-section t] + ["Insert Template" thy-insert-template t] + ["Process Theory" isa-process-thy-file + :active (proof-locked-region-empty-p)] + ["Retract Theory" isa-retract-thy-file + :active (proof-locked-region-full-p)] + ["Next Error" proof-next-error t] + ["Switch to Script" thy-find-other-file t]))) + (easy-menu-add thy-mode-pg-menu thy-mode-map) + (easy-menu-add thy-mode-isa-menu thy-mode-map) + + (if file + (progn (easy-menu-remove thy-mode-deps-menu) + (proof-thy-menu-define-deps file) + (easy-menu-add thy-mode-deps-menu thy-mode-map)))) + + +(defun thy-mode (&optional nomessage) + "Major mode for editing Isabelle theory files. +\\<thy-mode-map> +\\[thy-goto-next-section]\t Skips to the next section. +\\[thy-goto-prev-section]\t Skips to the previous section. + +\\[indent-for-tab-command]\t Indents the current line. + +\\[thy-insert-template]\t Inserts a template for the file or current section. + +If thy-use-sml-mode is non-nil, \\<thy-mode-map>\\[thy-minor-sml-mode] \ +invokes sml-mode as a minor mode +in the ML section. This is done automatically by \ +\\[indent-for-tab-command]. + +The style of indentation for theory files is controlled by these variables: + thy-heading-indent + thy-indent-level + thy-indent-strings +- see individual variable documentation for details. + +Here is the full list of theory mode key bindings: +\\{thy-mode-map}" + (interactive) + (kill-all-local-variables) + (setq major-mode 'thy-mode) + (setq mode-name "Theory") + (use-local-map thy-mode-map) + (thy-add-menus) + + (set-syntax-table thy-mode-syntax-table) + (make-local-variable 'indent-line-function) + (setq indent-line-function 'thy-indent-line) + (make-local-variable 'comment-start) ; Following lines as in sml-mode + (setq comment-start "(* ") ; . + (make-local-variable 'comment-end) ; . + (setq comment-end " *)") ; . + (setq comment-start-skip "(\\*+[ \t]?") ; . + (setq font-lock-keywords + thy-mode-font-lock-keywords) + + ;; Toolbar: needs alteration for non-scripting mode! + ;; (if (featurep 'proof-toolbar) + ;; (proof-toolbar-setup)) + ;; + + + (run-hooks 'thy-mode-hook) + (force-mode-line-update) + (if (null nomessage) + (message + (substitute-command-keys + "Isabelle theory-file mode. Use \\[thy-insert-template] to insert templates; \\[describe-mode] for help."))) + ) + +(defun thy-mode-quiet () + (interactive) + (thy-mode t)) + + + + +;;; "use" and "use_thy" with theory files ======================== + +;;; FIXME: Isabelle has been improved, so the following code could +;;; be cleaned up. Also set variable to allow automatic starting +;;; of process by reading logic image. + +;;; NB: this is a mess at the moment because of the theory file +;;; naming conventions. Really we need to parse the theory/ML +;;; file - yuk!! +;;; The next version of Isabelle will be more consistent. + +;(defun thy-use-file (&optional force-use_thy) +; "Send the file of the current buffer to an Isabelle buffer with use_thy or use." +; (interactive "P") +; (let ((fname (buffer-file-name))) +; (if fname +; (isa-query-save (current-buffer)) +; (setq fname +; (or (buffer-file-name) +; (read-file-name "Use file: " nil nil t)))) +; (let* +; ((has-thy-extn (string-match "\\.thy$" fname)) ; o/w assume ML. +; (tname (if has-thy-extn +; (substring fname 0 -4); cos use_thy is daft! +; fname)) +; (use (if (or has-thy-extn force-use_thy) +; "use_thy" +; "use")) +; (use-thy-string (concat use " \"" tname "\";")) +; (logic (isa-guess-root))) +; (thy-send-string logic use-thy-string)))) + +;(defun thy-use-region (beg end) +; "Send the region to an Isabelle buffer, with use" +; (interactive "r") +; (write-region beg end thy-use-tempname nil 'nomessage) +; (let* ((use-thy-string (concat "use \"" thy-use-tempname "\";")) +; (logic (isa-guess-root))) +; (thy-send-string logic use-thy-string))) + +;(defun thy-copy-region (beg end &optional isa-buffer) +; "Copy the region to an Isabelle buffer." +; (interactive "r") +; (let ((text (buffer-substring beg end)) +; (logic (isa-guess-root))) +; (save-excursion +; (thy-send-string logic text)))) + +;(defun thy-use-line (&optional isabuffer) +; "Send the current interactive ML line to an Isabelle buffer. +;Advance to the next line." +; (interactive) +; (isa-apply-to-interactive-line 'thy-copy-region)) + +;(defun thy-send-string (logic text &optional hide) +; "Send TEXT to a buffer running LOGIC. +;If LOGIC is nil, pick the first Isabelle buffer." +; (require 'isa-mode) +; (setq logic nil) ;;; #### HACK! This all needs changing for single-session. +; (let ((cur-frm (selected-frame))) ; Preserve selected frame. +; (if logic ; switch to Isabelle buffer, without +; (isabelle-session logic) ; raising the frame. +; ; (NB: this fails if was renamed). +; (set-buffer +; (or (car-safe (isa-find-buffers-in-mode 'isa-mode)) +; (error "Can't find an Isabelle buffer")))) +; (if hide +; (isa-send-string +; (get-buffer-process (current-buffer)) +; text) +; (isa-insert-ret text)) ; send use command +; (select-frame cur-frm))) + +(defun thy-proofgeneral-send-string (logic text &optional hide) + ;; FIXME -- new function! + ) + +;(defun thy-raise-windows () +; "Raise windows/frames associated with Isabelle session." +; (interactive) +; (isa-select-buffer isa-session-buffer t) +; (let ((raise t)) +; (mapcar 'isa-display-if-active +; isa-associated-buffers))) + + +;(defun thy-guess-logic-in-use () +; (if (featurep 'isa-mode) +; (let* ((buf (car-safe (isa-find-buffers-in-mode 'isa-mode))) +; (log (and buf +; (save-excursion +; (set-buffer buf) +; isa-logic-name)))) +; log) +; nil)) + + +;(defvar thy-use-tempname ".region.ML" +; "*Name of temporary file to hold region dring thy-use-region.") + + +;(defconst thy-logic-image-regexp +; "[lL][oO][gG][iI][cC] [iI][mM][aA][gG][eE]:[ \t]*\"?\\([^ \t\n\"]+\\)\"?[ \t]*$" +; "Regexp for locating name of logic image file in a .thy or .ML file.") + +;(defvar isa-logic-parents +; ;; I can't be bothered to write all of them in here, +; ;; and anyway they're ambiguous. Use "Logic image:" +; ;; instead. (Or find a way of getting emacs to track +; ;; theory structure...) +; '(("List" . "HOL") ("Prod" . "HOL") ("Nat" . "HOL") +; ("Ord" . "HOL") ("Set" ."HOL") ("Sexp" . "HOL") +; ("Univ" . "HOL") ("WF" . "HOL") ("Sum" . "HOL") +; ("IFOL" . "FOL")) +; "*An alist of parents of theories that live in logic files.") + +;(defun isa-guess-root () +; "Guess the root logic of the .thy or .ML file in current buffer. +;Choice based on first name found by: +; (i) special text: \"Logic Image: <name>\" toward start of file +; (ii) guess work based on parent in THY = <parent> if a .thy file." +; (save-excursion +; (goto-char (point-min)) +; (cond +; ((re-search-forward thy-logic-image-regexp 500 t) +; (buffer-substring (match-beginning 1) (match-end 1))) +; ((and (string-match "\\.thy$" (or (buffer-file-name) "")) +; (re-search-forward +; "\\w+[ \t\n]*=[ \t\n]*\\(\\w+\\)[ \t\n]*\\+") 500 t) +; ;; Something looks like a parent theory: +; ;; MyThy = HOL + ... +; (let ((child +; (buffer-substring (match-beginning 1) (match-end 1)))) +; (or (cdr-safe (assoc child isa-logic-parents)) +; child)))))) + +;(defun isa-query-save (buffer) +; (and (buffer-modified-p buffer) +; (y-or-n-p (concat "Save file " +; (buffer-file-name buffer) +; "? ")) +; (save-excursion (set-buffer buffer) (save-buffer)))) + + + + +;;; Interfacing with sml-mode ======================== + +;; extending sml-mode. This only works if you visit the theory file +;; (or start Isabelle mode) first. +;; This is probably fairly close to The Right Thing... + +(defun isa-sml-hook () + "Hook to customize sml-mode for use with Isabelle." + ;(isa-menus) ; Add Isabelle main menu + ;; NB: these keydefs will affect other sml-mode buffers too! + (define-key sml-mode-map "\C-c\C-o" 'thy-find-other-file) + ; Disabled for proof general + ;(define-key sml-mode-map "\C-c\C-u" 'thy-use-file) + ;(define-key sml-mode-map "\C-c\C-r" 'thy-use-region) + ;(define-key sml-mode-map "\C-c\C-l" 'thy-use-line) + ;; listener minor mode removed: \C-c\C-c freed up + (define-key sml-mode-map "\C-c\C-t" 'thy-insert-id-header)) + +(add-hook 'sml-mode-hook 'isa-sml-hook) + +(defun isa-sml-mode () + "Invoke sml-mode after installing Isabelle hook." + (interactive) + (and (fboundp 'sml-mode) (sml-mode))) + +(defcustom isa-ml-file-extension ".ML" + "*File name extension to use for ML files." + :type 'string + :group 'isabelle) + +(defun thy-find-other-file (&optional samewindow) + "Find associated .ML or .thy file. +Finds and switch to the associated ML file (when editing a theory file) +or theory file (when editing an ML file). +If SAMEWINDOW is non-nil (interactively, with an optional argument) +the other file replaces the one in the current window." + (interactive "p") + (and + (buffer-file-name) + (let* ((fname (buffer-file-name)) + (thyfile (string-match "\\.thy$" fname)) + (mlfile (string-match + (concat (regexp-quote isa-ml-file-extension) "$") fname)) + (basename (file-name-sans-extension fname)) + (findfn (if samewindow 'find-file else 'find-file-other-window))) + (cond (thyfile + (funcall findfn (concat basename isa-ml-file-extension))) + (mlfile + (funcall findfn (concat basename ".thy"))))))) + + +;;; "minor" sml-mode inside theory files ========== + +(defvar thy-minor-sml-mode-map nil) + +(defun thy-install-sml-mode () + (progn + (require 'sml-mode) + (setq thy-minor-sml-mode-map (copy-keymap sml-mode-map)) + ;; Bind TAB to what it should be in sml-mode. + (define-key thy-minor-sml-mode-map "\t" 'indent-for-tab-command) + (define-key thy-minor-sml-mode-map "\C-c\C-m" 'thy-mode-quiet) + (define-key thy-minor-sml-mode-map "\C-c\C-t" 'thy-insert-template))) + +(defun thy-minor-sml-mode () + "Invoke sml-mode as if a minor mode inside a theory file. +This has no effect if thy-use-sml-mode is nil." + (interactive) + (if thy-use-sml-mode + (progn + (if (not (boundp 'sml-mode)) + (thy-install-sml-mode)) + (kill-all-local-variables) + (sml-mode) ; Switch to sml-mode + (setq major-mode 'thy-mode) + (setq mode-name "Theory Sml") ; looks like it's a minor-mode. + (use-local-map thy-minor-sml-mode-map) ; special map has \C-c\C-c binding. + (make-local-variable 'indent-line-function) + (setq indent-line-function 'thy-do-sml-indent) + (force-mode-line-update) + (message "Use C-c C-c to exit SML mode.")))) + +(defun thy-do-sml-indent () + "Run sml-indent-line in an Isabelle theory file, provided inside ML section. +If not, will turn off simulated minor mode and run thy-indent-line." + (interactive) + (if (string= (thy-current-section) "ML") ; NB: Assumes that TAB key was + (sml-indent-line) ; bound to sml-indent-line. + (thy-mode t) ; (at least, it is now!). + (thy-indent-line))) + + +(defun thy-insert-name (name) + "Insert NAME -- as a string if there are non-alphabetic characters in NAME." + (if (string-match "[a-zA-Z]+" name) + (insert name) + (insert "\"" name "\""))) + +(defun thy-insert-class (name supers) + (interactive + (list + (isa-read-id "Class name: ") + (isa-read-idlist "Super classes %s: "))) + (insert name) + (if supers (insert "\t< " (isa-splice-separator ", " supers))) + (indent-according-to-mode) + (forward-line 1)) + +(defun thy-insert-default-sort (sort) + (interactive + (list + (isa-read-id "Default sort: "))) + (insert sort) + (indent-according-to-mode) + (thy-goto-next-section)) + +(defun thy-insert-type (name no-of-args) + (interactive + (list + (isa-read-id "Type name: ") + (isa-read-num "Number of arguments: "))) + ;; make type variables for arguments. Daft things for >26! + (cond + ((zerop no-of-args)) + ((= 1 no-of-args) + (insert "'a ")) + (t + (insert "(") + (let ((i 0)) + (while (< i no-of-args) + (if (> i 0) (insert ",")) + (insert "'" (+ ?a i)) + (setq i (1+ i)))) + (insert ") "))) + (thy-insert-name name) + (indent-according-to-mode) + ;; forward line, although use may wish to add infix. + (forward-line 1)) + +(defun thy-insert-arity (name param-sorts result-class) + (interactive + (list + (isa-read-id "Type name: ") + (isa-read-idlist "Parameter sorts %s: ") + (isa-read-id "Result class: "))) + (insert name " :: ") + (if param-sorts + (insert "(" (isa-splice-separator ", " param-sorts) ") ")) + (insert result-class) + (indent-according-to-mode) + (forward-line 1)) + +(defun thy-insert-const (name type) + ;; only does a single constant, no lists. + (interactive + (let* ((thename (isa-read-id "Constant name: ")) + (thetype (isa-read-string (format "Type of `%s' : " thename)))) + (list thename thetype))) + (thy-insert-name name) + (insert " ::\t \"" type "\"\t\t") + (indent-according-to-mode) + ;; no forward line in case user adds mixfix + ) + +(defun thy-insert-rule (name) + (interactive + (list + (isa-read-id "Axiom name: "))) + (end-of-line 1) + (insert name "\t\"\"") + (backward-char) + (indent-according-to-mode)) + +(defun thy-insert-template () + "Insert a syntax template according to the current section" + (interactive) + (thy-check-mode) + (let* ((sect (thy-current-section)) + (tmpl (cdr-safe (assoc sect thy-sections)))) + ;; Ensure point is at start of an empty line. + (beginning-of-line) + (skip-chars-forward "\t ") + (if (looking-at sect) + (progn + (forward-line 1) + (skip-chars-forward "\t "))) + (if (looking-at "$") + nil + (beginning-of-line) + (newline) + (forward-line -1)) + (cond ((stringp tmpl) + (insert tmpl) + (indent-according-to-mode)) + ((null tmpl)) ; nil is a symbol! + ((symbolp tmpl) + (call-interactively tmpl))))) + +;;; === Functions for reading from the minibuffer. +;;; + +; These could be improved, e.g. to enforce syntax for identifiers. +; Unfortunately, Xemacs, and now Emacs too, lack a +; read-no-blanks-input function! + +(defun isa-read-idlist (prompt &optional init) + "Read a list of identifiers from the minibuffer." + (let ((items init) item) + (while (not (string= "" + (setq item (read-string + (format prompt (or items "")))))) + (setq items (nconc items (list item)))) + items)) + +(defun isa-read-id (prompt &optional init) + "Read an identifier from the minibuffer." + ;; don't allow empty input + (let ((result "")) + (while (string= result "") + (setq result (read-string prompt init))) + result)) + +(defun isa-read-string (prompt &optional init) + "Read a non-empty string from the minibuffer" + ;; don't allow empty input + (let ((result "")) + (while (string= result "") + (setq result (read-string prompt init))) + result)) + +(defun isa-read-num (prompt) + "Read a number from the minibuffer." + (read-number prompt t)) + +;(defun thy-read-thy-name () +; (let* ((default (car +; (isa-file-name-cons-extension +; (file-name-nondirectory +; (abbreviate-file-name (buffer-file-name))))))) +; default)) + +(defun thy-read-thy-name () + (let* ((default (car + (isa-file-name-cons-extension + (file-name-nondirectory + (abbreviate-file-name (buffer-file-name)))))) + (name (read-string + (format "Name of theory [default %s]: " default)))) + (if (string= name "") default name))) + +(defun thy-read-logic-image () + (let* ((defimage "Pure") + ;; (or (thy-guess-logic-in-use) + ;; "Pure")) + + (logic (read-string + (format "Name of logic image to use [default %s]: " + defimage)))) + (if (string= logic "") defimage logic))) + +(defun thy-insert-header (name logic parents) + "Insert a theory file header, for LOGIC, theory NAME with PARENTS" + (interactive + (list + (thy-read-thy-name) + (thy-read-logic-image) + (isa-read-idlist "Parent theory %s: "))) + (let* ((parentplus (isa-splice-separator + " + " + (or parents (list (or logic "Pure"))))) + (formalist (list + (cons "%t" name) + (cons "%p" parentplus)))) + (thy-insert-id-header name logic) + (insert (isa-format formalist thy-template))) + (goto-char (point-min)) + (thy-goto-next-section)) + +(defun thy-insert-id-header (name logic) + "Insert an identification header, for theory NAME logic image LOGIC." + (interactive + (list + (thy-read-thy-name) + (thy-read-logic-image))) + (let* ((formalist (list + (cons "%f" (buffer-file-name)) + (cons "%t" name) + (cons "%l" logic)))) + (insert (isa-format formalist thy-id-header)))) + +(defun thy-check-mode () + (if (not (eq major-mode 'thy-mode)) + (error "Not in Theory mode."))) + + +(defconst thy-headings-regexp + (concat + "^\\s-*\\(" + (substring (apply 'concat (mapcar + '(lambda (pair) + (concat "\\|" (car pair))) + (cdr thy-sections))) 2) + "\\)[ \t]*") + "Regular expression matching headings in theory files.") + +(defvar thy-mode-font-lock-keywords + (list + (list (proof-ids-to-regexp + (append '("infixl" "infixr" "binder") + (mapcar 'car (cdr thy-sections)))) + 0 'font-lock-keyword-face) + ;; FIXME: needs more work. Get symbols in quotes, etc, etc. + (list "\\s-*\\(\\w+\\)\\s-*\\(::?\\)" + 2 'font-lock-preprocessor-face) + (list "\\s-*\\(\\w+\\)\\s-*::?" + 1 'font-lock-variable-name-face) + (list "\".*\"\\s-*\\(::?\\)" + 1 'font-lock-preprocessor-face) + (list "\"\\(.*\\)\"\\s-*\\(::?\\)" + 1 'font-lock-variable-name-face)) +; (list "^\\s-*\\(\\w*\\)\\s-*\\(::\\)" +; 1 'font-lock-function-name-face +; 2 'font-lock-preprocessor-face)) + "Font lock keywords for thy-mode.") + +;;; movement between sections =================================== + +(defun thy-goto-next-section (&optional count noerror) + "Goto the next (or COUNT'th next) section of a theory file. +Negative value for count means previous sections. +If NOERROR is non-nil, failed search will not be signalled." + (interactive "p") + (condition-case nil + ;; string matching would probably be good enough + (cond ((and count (< count 0)) + (let ((oldp (point))) + (beginning-of-line) + (thy-goto-top-of-section) + ;; not quite right here - should go to top + ;; of file, like top of section does. + (if (equal (point) oldp) + (progn + (re-search-backward thy-headings-regexp + nil nil (1+ (- count))) + (forward-line 1)))) + t) + (t + (re-search-forward thy-headings-regexp nil nil count) + (forward-line 1) + t)) + ;; could just move to top or bottom if this happens, instead + ;; of giving this error. + (search-failed (if noerror nil + (error "No more headings"))))) + +(defun thy-goto-prev-section (&optional count noerror) + "Goto the previous section (or COUNT'th previous) of a theory file. +Negative value for count means following sections. +If NOERROR is non-nil, failed search will not be signalled." + (interactive) + (thy-goto-next-section (if count (- count) -1) noerror)) + +(defun thy-goto-top-of-section () + "Goto the top of the current section" + (interactive) + (if (re-search-backward thy-headings-regexp nil t) + (forward-line 1) + (goto-char (point-min)))) + +(defun thy-current-section () + "Return the current section of the theory file, as a string. +\"top\" indicates no section." + (save-excursion + (let* ((gotsect (re-search-backward thy-headings-regexp nil t)) + (start (if gotsect + (progn + (skip-chars-forward " \t") + (point))))) + (if (not start) + "top" + (skip-chars-forward "a-zA-z") + (buffer-substring start (point)))))) + + + +;;; kill line ================================================== + +(defun thy-kill-line (&optional arg) + "As kill-line, except in a string will kill continuation backslashes also. +Coalesces multiple lined strings by leaving single spaces." + (interactive "P") + (let ((str (thy-string-start)) + (kill-start (point)) + following-slash) + (if (not str) + ;; Usual kill line if not inside a string. + (kill-line arg) + (if arg + (forward-line (prefix-numeric-value arg)) + (if (eobp) + (signal 'end-of-buffer nil))) + (setq kill-start (point)) + (if (thy-string-start str) ; if still inside a string + (cond + ((looking-at "[ \t]*$") ; at end of line bar whitespace + (skip-chars-backward + " \t" + (save-excursion (beginning-of-line) (1+ (point)))) + (backward-char) + (if (looking-at "\\\\") ; preceding backslash + (progn + (skip-chars-backward " \t") + (setq following-slash t) + (setq kill-start (min (point) kill-start))) + (goto-char kill-start)) + (forward-line 1)) + ((looking-at "[ \t]*\\\\[ \t]*$") ; before final backslash + (setq following-slash t) + (forward-line 1)) + ((looking-at "\\\\[ \t]*\\\\[ \t]*$") ; an empty line! + (forward-line 1)) + ((looking-at ".*\\(\\\\\\)[ \t]*$") ; want to leave backslash + (goto-char (match-beginning 1))) + ((and kill-whole-line (bolp)) + (forward-line 1)) + (t + (end-of-line)))) + (if (and following-slash + (looking-at "[ \t]*\\\\")) ; delete following slash if + (goto-char (1+ (match-end 0)))) ; there's one + (kill-region kill-start (point)) ; do kill + (if following-slash + ;; did do just-one-space, but it's not nice to delete backwards + ;; too + (delete-region (point) + (save-excursion + (skip-chars-forward " \t") + (point))))))) + + +;;; INDENTATION ================================================== + +;;; Could do with thy-correct-string function, +;;; which does roughly the same as indent-region. +;;; Then we could have an electric " that did this! + +;;; Could perhaps have used fill-prefix to deal with backslash +;;; indenting, rather than lengthy code below? + +(defun thy-indent-line () + "Indent the current line in an Isabelle theory file. +If in the ML section, this switches into a simulated minor sml-mode." + (let ((sect (thy-current-section))) + (cond + ((and thy-use-sml-mode (string= sect "ML")) + (progn ; In "ML" section, + (thy-minor-sml-mode) ; switch to sml mode. + (sml-indent-line))) + + (t (let ((indent (thy-calculate-indentation sect))) + (save-excursion + (beginning-of-line) + (let ((beg (point))) + (skip-chars-forward "\t ") + (delete-region beg (point))) + (indent-to indent)) + (if (< (current-column) + (current-indentation)) + (skip-chars-forward "\t "))))))) + +;; Better Emacs major modes achieve a kind of "transparency" to +;; the user, where special indentation,etc. happens under your feet, but +;; in a useful way that you soon get accustomed to. Worse modes +;; cause frustration and repetitive re-editing of automatic indentation. +;; I hope I've achieved something in the first category... + +(defun thy-calculate-indentation (sect) + "Calculate the indentation for the current line. +SECT should be the string name of the current section." + (save-excursion + (beginning-of-line) + (or (thy-long-comment-string-indentation) + (if (looking-at "\\s-*$") + ;; Empty lines use indentation for section. + (thy-indentation-for sect) + (if (looking-at thy-headings-regexp) + thy-heading-indent + (progn + (skip-chars-forward "\t ") + (cond + ;; A comment? + ((looking-at "(\\*") + (thy-indentation-for sect)) + ;; Anything else, use indentation for section + (t (thy-indentation-for sect))))))))) + +(defun thy-long-comment-string-indentation () + "Calculate the indentation if inside multi-line comment or string. +Also indent string contents." + (let* ((comstr (thy-comment-or-string-start)) + (bolpos (save-excursion + (beginning-of-line) + (point))) + (multi (and comstr + (< comstr bolpos)))) + (if (not multi) + nil + (save-excursion + (beginning-of-line) + (cond + + ;; Inside a comment? + ((char-equal (char-after comstr) ?\( ) + (forward-line -1) + (if (looking-at "[\t ]*(\\*") + (+ 3 (current-indentation)) + (current-indentation))) + + ;; Otherwise, a string. + ;; Enforce correct backslashing on continuing + ;; line and return cons of backslash indentation + ;; and string contents indentation for continued + ;; line. + (t + (let ((quote-col (save-excursion (goto-char comstr) + (current-column)))) + (if thy-indent-strings + (thy-string-indentation comstr) + ;; just to right of matching " + (+ quote-col 1))))))))) + +(defun thy-string-indentation (start) + ;; Guess indentation for text inside a string + (let* ((startcol (save-excursion (goto-char start) (current-column))) + (pps-state (parse-partial-sexp (1+ start) (point))) + (par-depth (car pps-state))) + (cond (;; If not in nested expression, startcol+1 + (zerop par-depth) + (1+ startcol)) + (;; If in a nested expression, use position of opening bracket + (natnump par-depth) + (save-excursion + (goto-char (nth 1 pps-state)) + (+ (current-column) + (cond ((looking-at "\\[|") 3) + (t 1))))) + (;; Give error for too many closing parens + t + (error "Mismatched parentheses"))))) + +(defun thy-indentation-for (sect) + "Return the indentation for section SECT" + (if (string-equal sect "top") + thy-heading-indent + thy-indent-level)) + +(defun thy-string-start (&optional min) + "Return position of start of string if inside one, nil otherwise." + (let ((comstr (thy-comment-or-string-start))) + (if (and comstr + (save-excursion + (goto-char comstr) + (looking-at "\""))) + comstr))) + +;;; Is this parsing still too slow? (better way? e.g., try setting +;;; variable "char" and examining it, rather than finding current +;;; state first - fewer branches in non-interesting cases, perhaps. +;;; NB: it won't understand escape sequences in strings, such as \" + +(defun thy-comment-or-string-start (&optional min) + "Find if point is in a comment or string, starting parse from MIN. +Returns the position of the comment or string start or nil. +If MIN is nil, starts from top of current section. + +Doesn't understand nested comments." + (or min + (setq min + (save-excursion + (thy-goto-top-of-section) (point)))) + (if (<= (point) min) + nil + (let ((pos (point)) + (incomdepth 0) + incom instring) ; char + (goto-char min) + (while (< (point) pos) + ;; When inside a string, only look for its end + (if instring + (if (eq (char-after (point)) ?\") ; looking-at "\"" + (setq instring nil)) + ;; If inside a comment, look for a comment end + (if (> 0 incomdepth) + (if (and ; looking-at "\\*)" + (eq (char-after (point)) ?\*) + (eq (char-after (1+ (point))) ?\))) + (setq incomdepth (1- incomdepth))) + ;; If inside neither comment nor string, look for + ;; a string start. + (if (eq (char-after (point)) ?\") ; looking-at "\"" + (setq instring (point)))) + ;; Look for a comment start (unless inside a string) + (if (and + (eq (char-after (point)) ?\() + (eq (char-after (1+ (point))) ?\*)) + (progn + (if (= 0 incomdepth) ; record start of main comment + (setq incom (point))) ; only + (setq incomdepth (1+ incomdepth))))) + (forward-char)) + (if (> 0 incomdepth) incom instring)))) + + + + +(provide 'thy-mode) + +;;; end of thy-mode.el |