From 4531ad9f1922fbaf80f9321a5b8535610aab881d Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 5 Dec 2006 12:43:39 +0000 Subject: Use Isar-specific isabelle-system file --- isar/isabelle-system.el | 477 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 477 insertions(+) create mode 100644 isar/isabelle-system.el (limited to 'isar/isabelle-system.el') diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el new file mode 100644 index 00000000..7e105bda --- /dev/null +++ b/isar/isabelle-system.el @@ -0,0 +1,477 @@ +;; isabelle-system.el Interface with Isabelle system +;; +;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall. +;; +;; Author: David Aspinall +;; Maintainer: Proof General maintainer +;; +;; $Id$ +;; +;; Most of this code is taken from the final version of Isamode. +;; -------------------------------------------------------------- +;; + +(require 'proof) ; for proof-assistant-symbol, etc. +(require 'proof-syntax) ; for proof-string-match + + +;; The isabelle custom group won't have been defined yet. +(defgroup isabelle nil + "Customization of user options for Isabelle and Isabelle/Isar Proof General" + :group 'proof-general) + +(defcustom isabelle-web-page + "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" + ;; "http://isabelle.in.tum.de" + ;; "http://www.dcs.ed.ac.uk/home/isabelle" + "URL of web page for Isabelle." + :type 'string + :group 'isabelle) + + +;;; ================ Extract Isabelle settings ================ + +(defcustom isa-isatool-command + (or (getenv "ISATOOL") + (proof-locate-executable "isatool") + ;; FIXME: use same mechanism as isabelle-program-name below. + (let ((possibilities + (list + (concat (getenv "HOME") "/Isabelle/bin/isatool") + "/usr/share/Isabelle/bin/isatool" + "/usr/local/bin/isatool" + "/usr/local/Isabelle/bin/isatool" + "/usr/bin/isatool" + "/opt/bin/isatool" + "/opt/Isabelle/bin/isatool"))) + (while (and possibilities + (not (file-executable-p + (car possibilities)))) + (setq possibilities (cdr possibilities))) + (car-safe possibilities)) + "path_to_isatool_is_unknown") + "Command to invoke Isabelle tool 'isatool'. +XEmacs should be able to find `isatool' if it is on the PATH when +started. Then several standard locations are attempted. +Otherwise you should set this, using a full path name here for reliable +working." + :type 'file + :group 'isabelle) + +(defvar isatool-not-found nil + "Non-nil if user has been prompted for `isatool' already and it wasn't found.") + +(defun isa-set-isatool-command () + "Make sure isa-isatool-command points to a valid executable. +If it does not, prompt the user for the proper setting. +If it appears we're running on win32 or FSF Emacs, we allow this to +remain unverified. +Returns non-nil if isa-isatool-command is surely an executable +with full path." + (interactive) + (unless (or isatool-not-found (file-executable-p isa-isatool-command)) + (setq isa-isatool-command + (read-file-name + "Please give the full path to `isatool' (RET if you don't have it): " + nil nil nil)) + (if (not (file-executable-p isa-isatool-command)) + (progn + (setq isatool-not-found t) + (beep) + (warn "Proof General: isatool command not found; some menus will be incomplete and Isabelle may not run correctly. Please check your Isabelle installation.")))) + (file-executable-p isa-isatool-command)) + +(defun isa-shell-command-to-string (command) + "Like shell-command-to-string except the last character is stripped." + (let ((s (shell-command-to-string command))) + (if (equal (length s) 0) s + (substring s 0 -1)))) + +(defun isa-getenv (envvar &optional default) + "Extract an environment variable setting using the `isatool' program. +If the isatool command is not available, try using elisp's getenv +to extract the value from Emacs' environment. +If there is no setting for the variable, DEFAULT will be returned" + (isa-set-isatool-command) + (if (file-executable-p isa-isatool-command) + (let ((setting (isa-shell-command-to-string + (concat isa-isatool-command + " getenv -b " envvar)))) + (if (string-equal setting "") + default + setting)) + (or (getenv envvar) default))) + +;;; +;;; ======= Interaction with System using Isabelle tools ======= +;;; + +(defcustom isabelle-program-name + (if (fboundp 'proof-running-on-win32) + "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" + (proof-locate-executable "isabelle" t + '("/usr/local/Isabelle/bin/" + "/opt/Isabelle/bin/" + "/usr/Isabelle/bin/" + "/usr/share/Isabelle/bin/"))) + "*Default name of program to run Isabelle. + +The default value except when running under Windows is \"isabelle\", +which will get expanded using PATH if possible, or in a number +of standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc). + +The default value when running under Windows is: + + C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\ + +This expects SML/NJ in C:\\sml and Isabelle images in C:\Isabelle. +The logic image name is tagged onto the end. + +NB: The Isabelle settings mechanism or the environment variable +ISABELLE will always override this setting." + :type 'file + :group 'isabelle) + +(defvar isabelle-prog-name isabelle-program-name + "Set from `isabelle-program-name', has name of logic appended sometimes.") + +(defun isabelle-command-line () + "Make proper command line for running Isabelle" + (let* + ;; The ISABELLE and PROOFGENERAL_LOGIC values (as set when run + ;; under the interface wrapper script) indicate that we should + ;; determine the proper command line from the current Isabelle + ;; settings environment. + ((isabelle (or + (getenv "ISABELLE") ; overrides default, may be updated + isabelle-program-name ; calculated earlier + "isabelle")) ; to be really sure + (isabelle-opts (getenv "ISABELLE_OPTIONS")) + (opts (concat + " -PI" ;; Proof General + Isar + (if proof-shell-unicode " -m PGASCII" "") + (if (and isabelle-opts (not (equal isabelle-opts ""))) + (concat " " isabelle-opts) ""))) + (logic (or isabelle-chosen-logic + (getenv "PROOFGENERAL_LOGIC"))) + (logicarg (if (and logic (not (equal logic ""))) + (concat " " logic) ""))) + (concat isabelle opts logicarg))) + + +(defun isabelle-choose-logic (logic) + "Adjust isabelle-prog-name and proof-prog-name for running LOGIC." + (interactive + (list (completing-read + "Use logic: " + (mapcar 'list (cons "Default" + isabelle-logics-available))))) + ;; a little bit obnoxious maybe (but maybe what naive user would expect) + ;; (customize-save-variable 'isabelle-chosen-logic logic) + (if (proof-shell-live-buffer) + (error "Can't change logic while Isabelle is running, please exit process first!")) + (customize-set-variable 'isabelle-chosen-logic + (unless (string-equal logic "Default") logic)) + (setq isabelle-prog-name (isabelle-command-line)) + (setq proof-prog-name isabelle-prog-name) + ;; Settings are potentially different between logics, and + ;; so are Isar keywords. Set these to nil so they get + ;; automatically re-initialised. + ;; FIXME: Isar keywords change not handled yet. + (setq proof-assistant-settings nil) + (setq proof-menu-settings nil)) + +(defun isa-tool-list-logics () + "Generate a list of available object logics." + (if (isa-set-isatool-command) + (delete "" (split-string + (isa-shell-command-to-string + (concat isa-isatool-command " findlogics")) "[ \t]")))) + +(defun isa-view-doc (docname) + "View Isabelle document DOCNAME, using Isabelle tools." + (if (isa-set-isatool-command) + (apply 'start-process + "isa-view-doc" nil + (list isa-isatool-command "doc" docname)))) + +(defvar isabelle-version-string 'unset) + +(defun isa-version () + "Try to retrieve a version value for Isabelle." + (unless (stringp isabelle-version-string) + (setq isabelle-version-string + (if (isa-set-isatool-command) + (isa-shell-command-to-string + ;; This may return the string "Unknown Isabelle tool: + ;; version", but that's fine. + (concat isa-isatool-command " version")) + "Unknown"))) + isabelle-version-string) + +;; We're going to need to know this pretty soon, so let's do it now. +(defconst isa-supports-pgip + ;; PGIP-aware Isabelle versions are also aware of their own version + (not (string-match "^Unknown" (isa-version))) + "Whether the currently configured version of Isabelle supports PGIP.") + + + + +(defun isa-tool-list-docs () + "Generate a list of documentation files available, with descriptions. +This function returns a list of lists of the form + ((DOCNAME DESCRIPTION) ....) +of Isabelle document names and descriptions. When DOCNAME is +passed to isa-tool-doc-command, DOCNAME will be viewed." + (if (isa-set-isatool-command) + (let ((docs (isa-shell-command-to-string + (concat isa-isatool-command " doc")))) + (unless (string-equal docs "") + (mapcan + (function (lambda (docdes) + (if (proof-string-match "^[ \t]+\\(\\S-+\\)[ \t]+" docdes) + (list (list + (substring docdes (match-beginning 1) (match-end 1)) + (substring docdes (match-end 0))))))) + (split-string docs "\n")))))) + +(defun isa-quit (save) + "Quit / save the Isabelle session. +Called with one argument: t to save database, nil otherwise." + (if (not save) + (isa-insert-ret "quit();")) + (comint-send-eof)) + +(defconst isabelle-verbatim-regexp "\\`\^VERBATIM: \\(\\(.\\|\n\\)*\\)\\'" + "Regexp matching internal marker for verbatim command output") + +(defun isabelle-verbatim (str) + "Mark internal command for verbatim output" + (concat "\^VERBATIM: " str)) + +;;; Set proof-shell-pre-interrupt-hook for PolyML 3. +(if (and + (not proof-shell-pre-interrupt-hook) + ;; (Older versions of Isabelle reported PolyML for PolyML 3). + (proof-string-match-safe "\\`polyml" (isa-getenv "ML_SYSTEM")) + (not (proof-string-match-safe "\\`polyml-4" (isa-getenv "ML_SYSTEM")))) + (add-hook + 'proof-shell-pre-interrupt-hook + (lambda () (proof-shell-insert (isabelle-verbatim "f") nil)))) + +;;; ========== Utility functions ========== + +(defcustom isabelle-refresh-logics t + "*Whether to refresh the list of logics during an interactive session. +If non-nil, then `isatool findlogics' will be used to regenerate +the `isabelle-logics-available' setting. If this tool does not work +for you, you should disable this behaviour." + :type 'boolean + :group 'isabelle) + +(defcustom isabelle-logics-available (isa-tool-list-logics) + "*List of logics available to use with Isabelle. +If the `isatool' program is available, this is automatically +generated with the lisp form `(isa-tool-list-logics)'." + :type (list 'string) + :group 'isabelle) + +;; FIXME: document this one +(defcustom isabelle-chosen-logic nil + "*Choice of logic to use with Isabelle. +If non-nil, will be added into isabelle-prog-name as default value. + +NB: you have saved a new logic image, it may not appear in the choices +until Proof General is restarted." + :type (append + (list 'choice) + (mapcar (lambda (str) (list 'const str)) isabelle-logics-available) + (list '(string :tag "Choose another") + '(const :tag "Unset (use default)" nil))) + :group 'isabelle) + +(defconst isabelle-docs-menu + (let ((vc '(lambda (docdes) + (vector (car (cdr docdes)) + (list 'isa-view-doc (car docdes)) t)))) + (list (cons "Isabelle documentation" (mapcar vc (isa-tool-list-docs))))) + "Isabelle documentation menu. Constructed when PG is loaded.") + + +;; PG 3.5: logics menu is now refreshed automatically. Rather +;; a big effort for such a small effect. +(defun isabelle-logics-menu-calculate () + (setq isabelle-logics-menu-entries + (cons "Logics" + (append + '(["Default" + (isabelle-choose-logic nil) + :active (not (proof-shell-live-buffer)) + :style radio + :selected (not isabelle-chosen-logic)]) + (mapcar (lambda (l) + (vector l (list 'isabelle-choose-logic l) + :active '(not (proof-shell-live-buffer)) + :style 'radio + :selected (list 'equal 'isabelle-chosen-logic l))) + isabelle-logics-available))))) + +(defvar isabelle-time-to-refresh-logics t + "Non-nil if we should refresh the logics list") + +(defun isabelle-logics-menu-refresh () + "Refresh isabelle-logics-menu-entries, returning new entries." + (interactive) + (if (and isabelle-refresh-logics + (or isabelle-time-to-refresh-logics (interactive-p))) + (progn + (setq isabelle-logics-available (isa-tool-list-logics)) + (isabelle-logics-menu-calculate) + (if proof-running-on-Emacs21 + ;; update the menu manually + (easy-menu-add-item proof-assistant-menu nil + isabelle-logics-menu-entries)) + (setq isabelle-time-to-refresh-logics nil) ;; just done it, don't repeat! + (run-with-timer 2 nil ;; short delay to avoid doing this too often + (lambda () (setq isabelle-time-to-refresh-logics t)))))) + +;; Function for XEmacs only +(defun isabelle-logics-menu-filter (&optional ignored) + (isabelle-logics-menu-refresh) + (cdr isabelle-logics-menu-entries)) + +;; Functions for GNU Emacs only to update logics menu +(if proof-running-on-Emacs21 +(defun isabelle-menu-bar-update-logics () + ;; standard check we're being invoked + (and (current-local-map) + (keymapp (lookup-key (current-local-map) + (vector 'menu-bar (intern proof-assistant)))) + (isabelle-logics-menu-refresh)))) + +(if proof-running-on-Emacs21 + (add-hook 'menu-bar-update-hook 'isabelle-menu-bar-update-logics)) + + +(defvar isabelle-logics-menu-entries (isabelle-logics-menu-calculate)) + +(defvar isabelle-logics-menu + (if proof-running-on-XEmacs + (cons (car isabelle-logics-menu-entries) + (list :filter 'isabelle-logics-menu-filter)) ;; generates menu on click + isabelle-logics-menu-entries) + "Isabelle logics menu. Calculated when Proof General is loaded.") + +;; Added in PG 3.4: load isar-keywords file. +;; This roughly follows the method given in the interface script. +;; It could be used to add an elisp command at the bottom of +;; a theory file, if we sorted out the load order a bit, or +;; added a facility to reconfigure. +;; TODO: also add something to spill out a keywords file? +(defun isabelle-load-isar-keywords (&optional kw) + (interactive "sLoad isar keywords: ") + (let ((userhome (isa-getenv "ISABELLE_HOME_USER")) + (isahome (isa-getenv "ISABELLE_HOME")) + (isarkwel "%s/etc/isar-keywords-%s.el") + (isarel "%s/etc/isar-keywords.el") + (ifrdble (lambda (f) (if (file-readable-p f) f)))) + (load-file + (or + (and kw (funcall ifrdble (format isarkwel userhome kw))) + (and kw (funcall ifrdble (format isarkwel isahome kw))) + (funcall ifrdble (format isarel userhome)) + (funcall ifrdble (format isarel isahome)) + (locate-library "isar-keywords"))))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Generic Isabelle menu for Isabelle and Isabelle/Isar +;; + +(defpgdefault menu-entries + isabelle-logics-menu) + +(defpgdefault help-menu-entries isabelle-docs-menu) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; X-Symbol language configuration, and adding to completion table +;; + +(defpgdefault x-symbol-language 'isabelle) + + +(eval-after-load "x-symbol-isabelle" + ;; Add x-symbol tokens to isa-completion-table and rebuild + ;; internal completion table if completion is already active +'(progn + (defpgdefault completion-table + (append (proof-ass completion-table) + (mapcar (lambda (xsym) (nth 2 xsym)) + x-symbol-isabelle-table))) + (setq proof-xsym-font-lock-keywords + x-symbol-isabelle-font-lock-keywords) + (if (featurep 'completion) + (proof-add-completions)))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Subterm markup -- faking it +;; + +(defun isabelle-convert-idmarkup-to-subterm () + "Convert identifier markup to subterm markup. +This is a hook setting for `pg-after-fontify-output-hook' to +enable identifiers to be highlighted. (To disable that behaviour, +the function `pg-remove-specials' can be used instead)." + ;; NB: the order of doing this is crucial: it must happen after + ;; fontifying (since replaces chars used for fontifying), but before + ;; X-Sym decoding (since some chars used for fontifying may clash + ;; with X-Sym character codes: luckily those codes don't seem to + ;; cause problems for subterm markup). + ;; Future version of this should use PGML output in Isabelle2002. + (goto-char (point-min)) + (while (proof-re-search-forward "[\351-\357]" nil t) + (replace-match "\372\200\373" nil t)) + (goto-char (point-min)) + (while (proof-re-search-forward "\350" nil t) + (replace-match "\374" nil t))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Context-senstive in-span menu additions +;; + +(defun isabelle-create-span-menu (span idiom name) + (if (string-equal idiom "proof") + (let ((thm (span-property span 'name))) + (list (vector + "Visualise dependencies" + `(proof-shell-invisible-command + ,(format "thm_deps %s;" thm)) + (not (string-equal thm proof-unnamed-theorem-name))))))) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; XML as an SML string: add escapes for quotes +;; + +(defun isabelle-xml-sml-escapes (xmlstring) + (replace-regexp-in-string "\"" "\\\"" xmlstring t t)) + +(defun isabelle-process-pgip (xmlstring) + "Return an Isabelle or Isabelle/Isar command to process PGIP in XMLSTRING." + (format "ProofGeneral.process_pgip \"%s\";" + (isabelle-xml-sml-escapes xmlstring))) + + +(provide 'isabelle-system) +;; End of isabelle-system.el -- cgit v1.2.3