Deleted file

1 files changed, 0 insertions, 1045 deletions

diff --git a/isa/thy-mode.el b/isa/thy-mode.el
deleted file mode 100644
index 2eef0988..00000000
--- a/isa/thy-mode.el
+++ /dev/null
@@ -1,1045 +0,0 @@
-;; thy-mode.el - Mode for Isabelle theory files.
-;;
-;; Copyright (C) 1998 LFCS Edinburgh. 
-;; Author:    David Aspinall <David.Aspinall@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 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 isa 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$" . isa-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