diff options
-rw-r--r-- | generic/proof-depends.el | 567 | ||||
-rw-r--r-- | generic/proof-script.el | 24 |
2 files changed, 298 insertions, 293 deletions
diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 62a21c5d..ac77d5ef 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -1,9 +1,9 @@ -;; proof-depends.el Functions +;; proof-depends.el Managing theorem-theorem and theorem-definition dependencies. ;; -;; Copyright (C) 2000 University of Edinburgh. -;; Author: Fiona McNeill +;; Copyright (C) 2000,1 University of Edinburgh. +;; Author: Fiona McNeill ;; -;; Status: Experimental code, currently dormant +;; Status: Experimental code ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> ;; ;; $Id$ @@ -15,8 +15,7 @@ ;; ;; FIXME: ;; -;; * Clean up, rationalize and integrate -;; * All functions should be renamed to proof-depends-<blah> +;; * Clean up and integrate ;; @@ -26,91 +25,94 @@ ;;time. Note; only definitions that have some dependents in the file ;;are added to the list - otherwise their names are not needed. -(defvar proof-thm-names-of-files nil) -;;of form: ((file-name-1 (thm1 thm2 thm3)) (file-name-2 (thm1 thm2 thm3))) +(defvar proof-thm-names-of-files nil + "A list of file and theorems contained within. +Of form: ((file-name-1 (thm1 thm2 thm3)) (file-name-2 (thm1 thm2 thm3)))") -(defvar proof-def-names-of-files nil) -;;of form: ((file-name-1 (def1 def2 def3)) (file-name-2 (def1 def2 def3))) +(defvar proof-def-names-of-files nil + "A list of files and defs contained within. +Of form: ((file-name-1 (def1 def2 def3)) (file-name-2 (def1 def2 def3)))") +;; ***************************************************************************** +;; DEPENDENCY INFORMATION +;; ***************************************************************************** +;; The following functions are responsible for updated the dependencies +;; and dependents information for each span and updating the two +;; variables above. -;;***************************************************************************** -;;DEPENDENCY INFORMATION - - -;;The following functions are responsible for updated the dependencies -;;and dependents information for each span and updating the two -;;variables above. +;; dependencies-within-file-list is called in proof-script.el within +;; the function proof-done-advancing. This function is called every +;; time a span is completed. It will set the result of +;; dependencies-within-file-list to the span-property +;; dependencies-within-file which can then be called. +;; dependencies-within-file-list takes the list of dependencies +;; returned by Isabelle and filters them to return only those +;; dependencies that are in the same file as the span. -;;dependencies-within-file-list is called in proof-script.el within -;;the function proof-done-advancing. This function is called every -;;time a span is completed. It will set the result of -;;dependencies-within-file-list to the span-property -;;dependencies-within-file which can then be called. -;;dependencies-within-file-list takes the list of dependencies -;;returned by Isabelle and filters them to return only those -;;dependencies that are in the same file as the span. -(defun dependencies-within-file-list (dependency-list-of-strings buffer-file-name-sans-extension) +;;;###autoload +(defun proof-dependencies-within-file-list (dependency-list-of-strings + buffer-file-name-sans-extension) "Takes a list of dependencies and returns those contained in buffer" - (remove-duplicates - (remove-nils + (proof-remove-duplicates + (proof-remove-nils (mapcar #'(lambda (theorem) - (let ((theorem-pair (divide-string theorem))) + (let ((theorem-pair (proof-divide-string theorem))) (if (equal (car theorem-pair) buffer-file-name-sans-extension) (cadr theorem-pair)))) proof-last-theorem-dependencies)))) -;;update-dependents is also called in proof-done-advancing and is -;;passed the result of dependencies-within-file-list. This function -;;will recurse over this list and for each element will check if it is -;;a span. Depending on this, the function then calls either -;;update-depts-thy or update-depts-ml which both add SPAN-NAME to the -;;dependents list of the first element of the list, which is classed -;;as either a span or a definition. They then update the relevant -;;variable (see above). +;; update-dependents is also called in proof-done-advancing and is +;; passed the result of proof-dependencies-within-file-list. This +;; function will recurse over this list and for each element will +;; check if it is a span. Depending on this, the function then calls +;; either proof-update-depts-thy or proof-update-depts-ml which both +;; add SPAN-NAME to the dependents list of the first element of the +;; list, which is classed as either a span or a definition. They then +;; update the relevant variable (see above). -;;Note: this is not ideal as there are some objects, such as ml -;;commands like [Addsimps] which are neither spans nor definitions. -;;These are classed as definitions as they fail the span test but -;;ideally they should be filtered out. +;; Note: this is not ideal as there are some objects, such as ml +;; commands like [Addsimps] which are neither spans nor definitions. +;; These are classed as definitions as they fail the span test but +;; ideally they should be filtered out. -(defun update-dependents (depcs-list file file-name span-name) +(defun proof-update-dependents (depcs-list file file-name span-name) "Takes a list of dependencies and uses these to update span dependents info For each element of depcs-list in file, span-name is added to its list of dependents" (while depcs-list (let* ((this-span-name (car depcs-list)) - (this-span (find-span-with-prop 'name this-span-name file))) + (this-span (proof-find-span-with-prop 'name this-span-name file))) (if (null this-span) (let ((def-name (car (split-string this-span-name "\\.")))) - (update-depts-thy file file-name def-name span-name)) - (update-depts-ML file this-span span-name))) + (proof-update-depts-thy file file-name def-name span-name)) + (proof-update-depts-ML file this-span span-name))) (setq depcs-list (cdr depcs-list))) t) -(defun update-depts-thy (file file-name def-name span-name) +(defun proof-update-depts-thy (file file-name def-name span-name) (let* ((theory-file (concat file-name ".thy")) - (thy-span (find-first-span theory-file)) + (thy-span (proof-find-first-span theory-file)) (def-list-name (intern (concat "dependents_" def-name))) (new-depts-list (cons span-name (span-property thy-span def-list-name)))) (set-span-property thy-span def-list-name new-depts-list)) - (setq proof-def-names-of-files (merge-names-list-it def-name file proof-def-names-of-files))) - - + (setq proof-def-names-of-files (proof-merge-names-list-it + def-name file proof-def-names-of-files))) -(defun update-depts-ML (file this-span span-name) +(defun proof-update-depts-ML (file this-span span-name) (let ((new-deps-list (cons span-name (span-property this-span 'dependents-within-file)))) (set-span-property this-span 'dependents-within-file new-deps-list)) - (setq proof-thm-names-of-files (merge-names-list-it span-name file-name proof-thm-names-of-files))) + (setq proof-thm-names-of-files + (proof-merge-names-list-it span-name file-name proof-thm-names-of-files))) @@ -124,23 +126,27 @@ For each element of depcs-list in file, span-name is added to its list of depend -(defun merge-names-list-it (name-to-add file-name list-so-far) +(defun proof-merge-names-list-it (name-to-add file-name list-so-far) "Takes the name of a span in file FILE-NAME and updates list-so-far. This is done by locating FILE-NAME in list-so-far and adding NAME-TO-ADD to its list of span names. If it is not in list-so-far then it is now added." - (let ((merge-names-list '()) + (let ((proof-merge-names-list '()) (found-it nil)) (while list-so-far - (setq merge-names-list + (setq proof-merge-names-list (if (equal file-name (caar list-so-far)) (and (setq found-it t) - (if (not (check-dups name-to-add (cadar list-so-far))) - (append (list (cons file-name (list (cons name-to-add (cadar list-so-far))))) (cdr list-so-far)) + (if (not (proof-check-dups name-to-add (cadar list-so-far))) + (append (list (cons file-name + (list (cons name-to-add + (cadar list-so-far))))) + (cdr list-so-far)) list-so-far)) - (append (list (car list-so-far)) merge-names-list)) + (append (list (car list-so-far)) proof-merge-names-list)) list-so-far (cdr list-so-far))) (if found-it - merge-names-list - (append (list (list file-name (list name-to-add))) merge-names-list)))) + proof-merge-names-list + (append (list (list file-name (list name-to-add))) + proof-merge-names-list)))) @@ -174,24 +180,24 @@ This is done by locating FILE-NAME in list-so-far and adding NAME-TO-ADD to its ;;Note: there are two functions on this menu which are not defined as ;;yet; this functionality will hopefully be added soon. -(defun create-in-span-context-menu (span file) - `("Span-menu" - ,(make-dependents-list span file) - ,(make-dependencies-list span file) +(defun proof-create-in-span-context-menu (span file) + `("Dependencies" + ,(proof-make-dependents-list span file) + ,(proof-make-dependencies-list span file) "-------------" - ,(make-highlight-depts-menu file) - ,(make-highlight-depcs-menu file) - ,(unhighlight-cmd file) + ,(proof-make-highlight-depts-menu file) + ,(proof-make-highlight-depcs-menu file) + ,(proof-unhighlight-cmd file) "------------")) ; ["Cycle through dependent spans" (message "need to work this out") t] ; ["Cycle through dependence spans" (message "need to work this out") t])) -(defun span-context-menu (event) +(defun proof-span-context-menu (event) (interactive "e") (select-window (event-window event)) (setf event-span (span-at (event-point event) 'type)) (let ((event-file (buffer-name (span-object event-span)))) - (popup-menu (create-in-span-context-menu event-span event-file)))) + (popup-menu (proof-create-in-span-context-menu event-span event-file)))) @@ -203,63 +209,75 @@ This is done by locating FILE-NAME in list-so-far and adding NAME-TO-ADD to its -;;the following items build up list of the form ("name" ["subname" action t] ... ["subnamex" actionx t]) which is passed back to create-in-span-context-menu. This is a way of building up the menu when not all of the informatino is known initially; this setup means `action' will only be called when that menu item is chosen and the information need not be known when the menu is set up. "name" is typically a command such as "Move to span" and "subname" is typically the name of, in this case, a span that can be chosen to move to. `action' must contain all the information that is needed to call the particular function without any further evaluation; for example, (unhighlight "loading.ML") is a correct possibility, (unhighlight file) is not because file is not evaluated. +;; the following items build up list of the form ("name" ["subname" +;; action t] ... ["subnamex" actionx t]) which is passed back to +;; create-in-span-context-menu. This is a way of building up the menu +;; when not all of the informatino is known initially; this setup +;; means `action' will only be called when that menu item is chosen +;; and the information need not be known when the menu is set up. +;; "name" is typically a command such as "Move to span" and "subname" +;; is typically the name of, in this case, a span that can be chosen +;; to move to. `action' must contain all the information that is +;; needed to call the particular function without any further +;; evaluation; for example, (unhighlight "loading.ML") is a correct +;; possibility, (unhighlight file) is not because file is not +;; evaluated. -;;If the list returned will be empty then each function returns just a -;;string containing the name of the command, such as "Move to span"; -;;this causes it to appear in the menu as unselectable text so that -;;the user can see it is not an appropriate command. +;; If the list returned will be empty then each function returns just +;; a string containing the name of the command, such as "Move to +;; span"; this causes it to appear in the menu as unselectable text so +;; that the user can see it is not an appropriate command. -;;make-depcs-list returns a sublist consisting of two further sublists -;;because it is convenient in this case to distinguish between spans -;;and dependencies. +;; make-depcs-list returns a sublist consisting of two further +;; sublists because it is convenient in this case to distinguish +;; between spans and dependencies. -(defun make-dependents-list (span file) +(defun proof-make-dependents-list (span file) "Returns a menu item submenu which gives the option to move to any dependent" (let ((depts-list (span-property span 'dependents-within-file))) (if (null depts-list) "Move to dependent" - (cons "Move to dependent" (make-depts-list-it depts-list file))))) + (cons "Move to dependent" + (proof-make-depts-list-it depts-list file))))) -(defun make-depts-list-it (depts-list file) +(defun proof-make-depts-list-it (depts-list file) (let ((depts-list-menu '())) (while depts-list - (let ((span-with-name (find-span-with-prop 'name (car depts-list) file))) + (let ((span-with-name (proof-find-span-with-prop 'name (car depts-list) file))) (setq depts-list-menu (cons - `[,(car depts-list) (and (goto-char ,(+ 2 (span-start span-with-name))) (recenter)) t] + `[,(car depts-list) + (and (goto-char ,(+ 2 (span-start span-with-name))) (recenter)) t] depts-list-menu) depts-list (cdr depts-list)))) depts-list-menu)) - - -(defun make-dependencies-list (span file) +(defun proof-make-dependencies-list (span file) "Returns a menu item submenu which gives the option to move to any dependence." (let* ((span (if (null span) (span-at (point) 'type) span)) (file (buffer-name (span-object span))) (file-name-sans-extension (car (split-string file "\\."))) (thy-file-name (concat file-name-sans-extension ".thy")) - (depcs-list (span-property span 'dependencies-within-file)) - (returned-list (make-depcs-list-it depcs-list file))) + (depcs-list (span-property span 'proof-dependencies-within-file)) + (returned-list (proof-make-depcs-list-it depcs-list file))) (setf current-thy-file thy-file-name) (cons "Move to dependency" returned-list))) -(defun make-depcs-list-it (depcs-list file) +(defun proof-make-depcs-list-it (depcs-list file) (let ((depcs-list-menu '()) (defs-list '()) (span-list '())) (while depcs-list - (let ((span-with-name (find-span-with-prop 'name (car depcs-list) file))) + (let ((span-with-name (proof-find-span-with-prop 'name (car depcs-list) file))) (if (null span-with-name) (setq defs-list (cons (car depcs-list) defs-list)) (setq span-list (cons span-with-name span-list))) (setq depcs-list (cdr depcs-list)))) - (let ((defs-list-menu-items (make-depcs-defs-list-it defs-list)) - (span-list-menu-items (make-depcs-span-list-it span-list))) + (let ((defs-list-menu-items (proof-make-depcs-defs-list-it defs-list)) + (span-list-menu-items (proof-make-depcs-span-list-it span-list))) (if (null defs-list-menu-items) (if (null span-list-menu-items) '("definitions" "spans") @@ -270,57 +288,56 @@ This is done by locating FILE-NAME in list-so-far and adding NAME-TO-ADD to its -(defun make-depcs-defs-list-it (defs-list) +(defun proof-make-depcs-defs-list-it (defs-list) (let ((defs-list-menu '())) (while defs-list (setq defs-list-menu (cons - `[,(car defs-list) (move-to-def ,(car defs-list)) t] + `[,(car defs-list) (proof-move-to-def ,(car defs-list)) t] defs-list-menu) defs-list (cdr defs-list))) defs-list-menu)) -(defun make-depcs-span-list-it (span-list) +(defun proof-make-depcs-span-list-it (span-list) (let ((span-list-menu '())) (while span-list (let ((current-span (car span-list))) (setq span-list-menu (cons - `[,(span-property current-span 'name) (goto-char ,(+ 2 (span-start current-span))) t] + `[,(span-property current-span 'name) + (goto-char ,(+ 2 (span-start current-span))) t] span-list-menu) span-list (cdr span-list)))) span-list-menu)) -(defun make-highlight-depts-menu (file) +(defun proof-make-highlight-depts-menu (file) "Return a menu item that will highlight the dependents of event-span" (if (null (span-property event-span 'dependents-within-file)) "Highlight all dependent spans" '["Highlight all dependent spans" (highlight-depts-of-span file) t])) -(defun make-highlight-depcs-menu (file) +(defun proof-make-highlight-depcs-menu (file) "Return a menu item that will highlight the depencdencies of event-span" - (if (null (span-property event-span 'dependencies-within-file)) + (if (null (span-property event-span 'proof-dependencies-within-file)) "Highlight all dependence spans" '["Highlight all dependence spans" (highlight-depcs-of-span file) t])) -(defun move-to-def (def) +(defun proof-move-to-def (def) "Brings up the theory file and moves the cursor to the first mention of DEF." (save-excursion (set-buffer current-thy-file) (let ((def-name (car (split-string def "\\.")))) (and (find-file-other-window current-thy-file) (goto-char (- (search-forward def-name) (length def-name))))))) - - -(defun unhighlight-cmd (file) - `["Unhighlight" (unhighlight ,file) t]) +(defun proof-unhighlight-cmd (file) + `["Unhighlight" (proof-unhighlight ,file) t]) @@ -333,28 +350,28 @@ This is done by locating FILE-NAME in list-so-far and adding NAME-TO-ADD to its ;;********************** -;;ML-FILE MENU +;; ML-FILE MENU -;;The following functions define the menu that appears in the ml file -;;outwith a span. +;; The following functions define the menu that appears in the ml file +;; outwith a span. -;;Since there is already a menu defined here that we wish to add to -;;rather than replace, it is not necessary to set up the event as -;;above. Rather, we simply indicate that proof-menu-define-deps -;;belongs to proof-mode-map. Everytime the function -;;proof-done-advancing in proof-script.el (see above) is called, the -;;span information gets updated and we wish to re-evaluate this menu. -;;This is because this menu contains items such as move to spans, -;;where we require an up to date list of all spans. Since we wish -;;this menu to be available at any point rather than just at the end -;;this process is done incrementally. +;; Since there is already a menu defined here that we wish to add to +;; rather than replace, it is not necessary to set up the event as +;; above. Rather, we simply indicate that proof-menu-define-deps +;; belongs to proof-mode-map. Everytime the function +;; proof-done-advancing in proof-script.el (see above) is called, the +;; span information gets updated and we wish to re-evaluate this menu. +;; This is because this menu contains items such as move to spans, +;; where we require an up to date list of all spans. Since we wish +;; this menu to be available at any point rather than just at the end +;; this process is done incrementally. -;;So everytime proof-done-advancing is called, proof-deps-menu (the -;;name of the menu created by proof-menu-define-deps) is removed from -;;proof-mode-map, if it exists, and once the span working has been -;;done proof-menu-define-deps is re-evaluted and the new value is then -;;added to proof-deps-menu. All this is done in proof-script.el. +;; So everytime proof-done-advancing is called, proof-deps-menu (the +;; name of the menu created by proof-menu-define-deps) is removed from +;; proof-mode-map, if it exists, and once the span working has been +;; done proof-menu-define-deps is re-evaluted and the new value is then +;; added to proof-deps-menu. All this is done in proof-script.el. (defun proof-menu-define-deps (file) @@ -362,73 +379,74 @@ This is done by locating FILE-NAME in list-so-far and adding NAME-TO-ADD to its proof-deps-menu proof-mode-map "The dependency menu" - `("Dependence info" - ,(highlight-depts-spans file) - ,(highlight-depcs-spans file) - ,(highlight-depts-defs file) - ,(unhighlight-cmd file) + `("ThyDependencies" + ,(proof-highlight-depts-spans file) + ,(proof-highlight-depcs-spans file) + ,(proof-highlight-depts-defs file) + ,(proof-unhighlight-cmd file) "--------------" - ,(move-to-spans file) - ,(goto-thy-file file)))) + ,(proof-move-to-spans file) + ,(proof-goto-thy-file file)))) -;;The following functions returns submenus of the form described -;;above. The particular action that these menu items do should be -;;obvious from the function name, for example highlight-depts-spans -;;returns a submenu which appears to user as follows: the name -;;"Highlight dependents of span" appears in the menu, if this is -;;chosen then the option of all choosing any span appears, when a span -;;is chosen its dependents are highlighted. +;; The following functions returns submenus of the form described +;; above. The particular action that these menu items do should be +;; obvious from the function name, for example highlight-depts-spans +;; returns a submenu which appears to user as follows: the name +;; "Highlight dependents of span" appears in the menu, if this is +;; chosen then the option of all choosing any span appears, when a +;; span is chosen its dependents are highlighted. - -(defun highlight-depts-spans (file) +(defun proof-highlight-depts-spans (file) "Returns a menu item which is either a string or a submenu. If the current event-span has no dependents then the menu name is given as unselectable text. Otherwise a submenu is returned, each item containing the name of a span and the direction to highlight its dependents." - (let ((thm-names-list (find-thm-or-def-list-it proof-thm-names-of-files file))) + (let ((thm-names-list (proof-find-thm-or-def-list-it + proof-thm-names-of-files file))) (if (null thm-names-list) "Highlight dependents of span" - (cons "Highlight dependents of span" (highlight-depts-spans-it thm-names-list file))))) + (cons "Highlight dependents of span" (proof-highlight-depts-spans-it + thm-names-list file))))) - - -(defun highlight-depts-spans-it (thm-names-list file) +(defun proof-highlight-depts-spans-it (thm-names-list file) (let ((menu-list '())) (while thm-names-list (setq menu-list (cons - `[,(car thm-names-list) (highlight-depts-of-span-name ,(car thm-names-list) ,file) t] + `[,(car thm-names-list) + (proof-highlight-depts-of-span-name ,(car thm-names-list) ,file) t] menu-list) thm-names-list (cdr thm-names-list))) menu-list)) -(defun highlight-depcs-spans (file) +(defun proof-highlight-depcs-spans (file) "Returns a menu item which is either a string or a submenu. If the current event-span has no dependencies then the menu name is given as unselectable text. Otherwise a submenu is returned, each item containing the name of a span and the direction to highlight its dependencies." - (let ((thm-names-list (find-thm-or-def-list-it proof-thm-names-of-files file))) + (let ((thm-names-list (proof-find-thm-or-def-list-it + proof-thm-names-of-files file))) (if (null thm-names-list) "Highlight dependencies of span" - (cons "Highlight dependencies of span" (highlight-depcs-spans-it thm-names-list file))))) + (cons "Highlight dependencies of span" + (proof-highlight-depcs-spans-it thm-names-list file))))) - - -(defun highlight-depcs-spans-it (thm-names-list file) +(defun proof-highlight-depcs-spans-it (thm-names-list file) (let ((menu-list '())) (while thm-names-list (setq menu-list (cons - `[,(car thm-names-list) (highlight-depcs-of-span-name ,(car thm-names-list) ,file) t] + `[,(car thm-names-list) + (proof-highlight-depcs-of-span-name ,(car thm-names-list) ,file) t] menu-list) thm-names-list (cdr thm-names-list))) menu-list)) -(defun find-thm-or-def-list-it (list file) +(defun proof-find-thm-or-def-list-it (list file) "Returns a list of all the thm or def names in file. LIST is a variable containing list of two elements: the first being the file name and the second being a list of thm / def names. If FILE matches any of these file names then the associated list is returned." (let ((right-list '())) @@ -439,33 +457,33 @@ LIST is a variable containing list of two elements: the first being the file nam right-list)) -(defun move-to-spans (file) +(defun proof-move-to-spans (file) "Returns a menu item which is either unselectable text or a submenu. A list of menu items containing thm names and a command to move to them is returned." - (let ((thm-names-list (find-thm-or-def-list-it proof-thm-names-of-files file))) + (let ((thm-names-list (proof-find-thm-or-def-list-it + proof-thm-names-of-files file))) (if (null thm-names-list) "Move to span" - (cons "Move to span" (move-to-spans-it thm-names-list file))))) + (cons "Move to span" (proof-move-to-spans-it thm-names-list file))))) -(defun move-to-spans-it (thm-names-list file) +(defun proof-move-to-spans-it (thm-names-list file) (let ((menu-list '())) (while thm-names-list (setq menu-list (cons - `[,(car thm-names-list) (and (move-to-span-name ,(car thm-names-list) ,file) (recenter)) t] + `[,(car thm-names-list) + (and (proof-move-to-span-name ,(car thm-names-list) ,file) (recenter)) t] menu-list) thm-names-list (cdr thm-names-list))) menu-list)) +(defun proof-move-to-span-name (span-name file) + (goto-char (+ 2 (span-start (proof-find-span-with-prop 'name span-name file))))) -(defun move-to-span-name (span-name file) - (goto-char (+ 2 (span-start (find-span-with-prop 'name span-name file))))) - - -(defun goto-thy-file (file) +(defun proof-goto-thy-file (file) "Opens the theory file connected to the ml-file FILE" (let ((thy-file (concat (car (split-string file "\\.")) ".thy"))) `["Move to thy file" (find-file ,thy-file) t])) @@ -473,93 +491,92 @@ A list of menu items containing thm names and a command to move to them is retur -;;********************** -;;THY-FILE MENU - - -;;The following functions define the menu that appears in the theory file. +;; ********************** +;; THY-FILE MENU +;; ********************** -;;This is added to the theory menu in thy-mode.el and then updated in -;;proof-script.el, as above, which rather than calling -;;thy-menu-define-deps and adding that to the menu, in fact calls -;;thy-added-menu in which the commands to remove, update and add this -;;to the thy-menu are. Hence it is tied in to the existing theory -;;menu. +;; The following functions define the menu that appears in the theory file. +;; This is added to the theory menu in thy-mode.el and then updated in +;; proof-script.el, as above, which rather than calling +;; thy-menu-define-deps and adding that to the menu, in fact calls +;; thy-added-menu in which the commands to remove, update and add this +;; to the thy-menu are. Hence it is tied in to the existing theory +;; menu. -(defun thy-menu-define-deps (file) +;; FIXME: this stuff belongs in thy-mode, I suppose. +;;;###autoload +(defun proof-thy-menu-define-deps (file) (easy-menu-define thy-mode-deps-menu thy-mode-map "The dependency menu" `("Dependence info" - ,(highlight-depts-defs file) - ,(unhighlight-cmd file) + ,(proof-highlight-depts-defs file) + ,(proof-unhighlight-cmd file) "-------------" - ,(move-to-spans-from-thy-file file) - ,(goto-ml-file file)))) + ,(proof-move-to-spans-from-thy-file file) + ,(proof-goto-ml-file file)))) ;;The functions below are evaluated in a similar manner to above. - - -(defun goto-ml-file (file) +(defun proof-goto-ml-file (file) `["Move to ml file" (find-file ,file) t]) -(defun highlight-depts-defs (file) +(defun proof-highlight-depts-defs (file) "Highlights the dependents of a definition." - (let ((def-names-list (find-thm-or-def-list-it proof-def-names-of-files file))) + (let ((def-names-list (proof-find-thm-or-def-list-it proof-def-names-of-files file))) (if (null def-names-list) "Highlight dependents of definition" (cons "Highlight dependents of definition" - (highlight-depts-defs-it def-names-list file))))) + (proof-highlight-depts-defs-it def-names-list file))))) -(defun highlight-depts-defs-it (def-names-list file) +(defun proof-highlight-depts-defs-it (def-names-list file) (let ((answer '())) (while def-names-list (setq answer (cons - `[,(car def-names-list) (highlight-depts-of-def ,(car def-names-list) ,file) t] + `[,(car def-names-list) + (proof-highlight-depts-of-def ,(car def-names-list) ,file) t] answer) def-names-list (cdr def-names-list))) answer)) -(defun move-to-spans-from-thy-file (file) +(defun proof-move-to-spans-from-thy-file (file) "Returns a menu item which is a submenu or unselectable text. A submenu is returned whose elements are the names of the theorems and instructions to move to that text in FILE" - (let ((thm-names-list (find-thm-or-def-list-it proof-thm-names-of-files file))) + (let ((thm-names-list (proof-find-thm-or-def-list-it + proof-thm-names-of-files file))) (if (null thm-names-list) "Move to span" - (cons "Move to span" (move-to-spans-from-thy-it thm-names-list file))))) - - - + (cons "Move to span" (proof-move-to-spans-from-thy-it + thm-names-list file))))) -(defun move-to-spans-from-thy-it (thm-names-list file) +(defun proof-move-to-spans-from-thy-it (thm-names-list file) (let ((menu-list '())) (while thm-names-list (setq menu-list (cons - `[,(car thm-names-list) (and (move-to-span-from-thy-name ,(car thm-names-list) ,file) (recenter)) t] + `[,(car thm-names-list) + (and (proof-move-to-span-from-thy-name + ,(car thm-names-list) ,file) (recenter)) t] menu-list) thm-names-list (cdr thm-names-list))) menu-list)) - -(defun move-to-span-from-thy-name (span-name file) +(defun proof-move-to-span-from-thy-name (span-name file) (and (find-file file) - (goto-char (+ 2 (span-start (find-span-with-prop 'name span-name file)))))) - - + (goto-char (+ 2 (span-start + (proof-find-span-with-prop 'name span-name file)))))) @@ -568,76 +585,74 @@ A submenu is returned whose elements are the names of the theorems and instructi -;;*************************************************************************** -;;HIGHLIGHTING FUNCTIONS +;; *************************************************************************** +;; HIGHLIGHTING FUNCTIONS +;; *************************************************************************** -;;The following functions are responsible for actually highlighting -;;the data and are called by the functions in the menu section when -;;they are setting up the submenus. +;; The following functions are responsible for actually highlighting +;; the data and are called by the functions in the menu section when +;; they are setting up the submenus. -;;They work by immediately unhighlighting all highlighting that exists -;;at present and then working through a given list of spans setting -;;the span's face property to the appropriate colour. These colours -;;are defined in proof-config.el. The given list is calculated from -;;dependents/dependency information. +;; They work by immediately unhighlighting all highlighting that exists +;; at present and then working through a given list of spans setting +;; the span's face property to the appropriate colour. These colours +;; are defined in proof-config.el. The given list is calculated from +;; dependents/dependency information. -;;Some of the functions are passed only a file and calculate -;;information using the event file; these are those that are called -;;from the span-context menu and hence a current event-span is set. -;;Others are passed a particular span or span-name; these are called -;;from the ml and thy menus when there is no event-span and -;;information can be returned about any span. +;; Some of the functions are passed only a file and calculate +;; information using the event file; these are those that are called +;; from the span-context menu and hence a current event-span is set. +;; Others are passed a particular span or span-name; these are called +;; from the ml and thy menus when there is no event-span and +;; information can be returned about any span. -;;In most cases these functions will merely highlighting the -;;appropriate spans and return nothing; the exception is -;;highlight-depcs-of-span-it. This is unusual in that it is called -;;when there is sometimes no highlighting to be done. Dependency -;;information contains both spans and defintions, but highlighting is -;;inappropriate for a definition because it would merely mean -;;highlighting the whole of the theory file; the theory file is not -;;divided into spans. Therefore a message is returned to explain to -;;the user why no dependency information is highlighted even there -;;dependencies within the file exist. +;; In most cases these functions will merely highlighting the +;; appropriate spans and return nothing; the exception is +;; highlight-depcs-of-span-it. This is unusual in that it is called +;; when there is sometimes no highlighting to be done. Dependency +;; information contains both spans and defintions, but highlighting is +;; inappropriate for a definition because it would merely mean +;; highlighting the whole of the theory file; the theory file is not +;; divided into spans. Therefore a message is returned to explain to +;; the user why no dependency information is highlighted even there +;; dependencies within the file exist. -(defun highlight-depts-of-span (file) +(defun proof-highlight-depts-of-span (file) "Finds all the dependents of the current event-span and highlights them" - (unhighlight file) + (proof-unhighlight file) (let ((depts-list (span-property event-span 'dependents-within-file))) - (highlight-depts-of-span-it depts-list file))) + (proof-highlight-depts-of-span-it depts-list file))) -(defun highlight-depts-of-span-name (span-name file) +(defun proof-highlight-depts-of-span-name (span-name file) "Finds all the dependents of span with name SPAN-NAME and highlights them" - (let ((span (find-span-with-prop 'name span-name file))) - (unhighlight file) + (let ((span (proof-find-span-with-prop 'name span-name file))) + (proof-unhighlight file) (let ((depts-list (span-property span 'dependents-within-file))) - (highlight-depts-of-span-it depts-list file)))) + (proof-highlight-depts-of-span-it depts-list file)))) -(defun highlight-depts-of-span-it (depts-list file) +(defun proof-highlight-depts-of-span-it (depts-list file) (while depts-list - (let ((next-depts-span (find-span-with-prop 'name (car depts-list) file))) + (let ((next-depts-span (proof-find-span-with-prop 'name (car depts-list) file))) (set-span-property next-depts-span 'face 'proof-highlight-dependent-face)) (setq depts-list (cdr depts-list)))) - - - -(defun highlight-depts-of-def (def-name file) +(defun proof-highlight-depts-of-def (def-name file) "Highlights all the dependents of the definition named DEF-NAME" - (unhighlight file) + (proof-unhighlight file) (find-file file) (let ((thy-file (concat (car (split-string file "\\.")) ".thy"))) (save-excursion @@ -645,65 +660,63 @@ A submenu is returned whose elements are the names of the theorems and instructi (let* ((thy-span (span-at (point-min) 'type)) (depts-list-name (intern (concat "dependents_" def-name))) (depts-list (span-property thy-span depts-list-name))) - (highlight-depts-of-def-it depts-list ml-file))))) + (proof-highlight-depts-of-def-it depts-list + file ;; da: was ml-file + ))))) - - -(defun highlight-depts-of-def-it (depts-list file) +(defun proof-highlight-depts-of-def-it (depts-list file) (save-excursion (set-buffer file) (while depts-list - (let ((next-depts-span (find-span-with-prop 'name (car depts-list) file))) + (let ((next-depts-span (proof-find-span-with-prop 'name (car depts-list) file))) (set-span-property next-depts-span 'face 'proof-highlight-dependent-face)) (setq depts-list (cdr depts-list))))) - - - -(defun highlight-depcs-of-span (file) +(defun proof-highlight-depcs-of-span (file) "Highlights all dependencies of event-span" - (unhighlight file) - (let ((depcs-list (span-property event-span 'dependencies-within-file))) - (highlight-depcs-of-span-it depcs-list file))) + (proof-unhighlight file) + (let ((depcs-list (span-property event-span 'proof-dependencies-within-file))) + (proof-highlight-depcs-of-span-it depcs-list file))) -(defun highlight-depcs-of-span-name (span-name file) +(defun proof-highlight-depcs-of-span-name (span-name file) "Highlights all dependencies of span with name SPAN-NAME" - (let ((span (find-span-with-prop 'name span-name file))) - (unhighlight file) - (let ((depcs-list (span-property span 'dependencies-within-file))) - (highlight-depcs-of-span-it depcs-list file)))) + (let ((span (proof-find-span-with-prop 'name span-name file))) + (proof-unhighlight file) + (let ((depcs-list (span-property span 'proof-dependencies-within-file))) + (proof-highlight-depcs-of-span-it depcs-list file)))) -(defun highlight-depcs-of-span-it (depcs-list file) +(defun proof-highlight-depcs-of-span-it (depcs-list file) (let ((exists-some-depc-span nil)) (while depcs-list - (let ((next-depcs-span (find-span-with-prop 'name (car depcs-list) file))) + (let ((next-depcs-span (proof-find-span-with-prop 'name (car depcs-list) file))) (if next-depcs-span (and (set-span-property next-depcs-span 'face 'proof-highlight-dependency-face) (setq exists-some-depc-span t))) (setq depcs-list (cdr depcs-list)))) (if (not exists-some-depc-span) - (and (message "This span has dependence on definition(s) but not on other spans in this file") - (ding))))) + (and (message + "This span has dependence on definition(s) but not on other spans in this file") + (ding))))) -(defun unhighlight (file) +(defun proof-unhighlight (file) "Returned all highlighted spans in file to the proof-locked-face highlighting" (save-excursion (set-buffer file) (let ((first-span (span-at (point-min) 'type))) - (unhighlight-it first-span)))) + (proof-unhighlight-it first-span)))) -(defun unhighlight-it (span) +(defun proof-unhighlight-it (span) (while span (set-span-property span 'face 'proof-locked-face) (setq span (next-span span 'type)))) @@ -721,14 +734,17 @@ A submenu is returned whose elements are the names of the theorems and instructi -;;***************************************************************************** -;;AUXILARY FUNCTIONS +;; ***************************************************************************** +;; AUXILARY FUNCTIONS +;; ***************************************************************************** -;;The following functions do not fall into any of the above catagories and are used as tools within larger functions. The function names should make their actions clear. +;; The following functions do not fall into any of the above +;; catagories and are used as tools within larger functions. The +;; function names should make their actions clear. -(defun find-first-span (file) +(defun proof-find-first-span (file) "this function takes a file and returns the span found at point-min" (find-file-noselect file) (save-excursion @@ -738,11 +754,10 @@ A submenu is returned whose elements are the names of the theorems and instructi - - -(defun find-span-with-prop (type-prop value-prop file) +(defun proof-find-span-with-prop (type-prop value-prop file) "Returns the span in FILE that has VALUE-PROP as its value for type TYPE-PROP. -Creates a list of all the spans in FILE and checks each one. Terminates when the first matching span in found." +Creates a list of all the spans in FILE and checks each one. +Terminates when the first matching span in found." (save-excursion (set-buffer file) (let ((list-of-spans (extent-list)) @@ -758,8 +773,8 @@ Creates a list of all the spans in FILE and checks each one. Terminates when th -(defun divide-string (string) - "this function takes a string containing a dot and splits it into a list of two strings containing what was on each side of the dot" +(defun proof-divide-string (string) + "Splits a string at a dot, returning two substrings." (let ((dot (string-match "\\." string))) (list (substring string 0 dot) (substring string (+ dot 1))))) @@ -768,7 +783,7 @@ Creates a list of all the spans in FILE and checks each one. Terminates when th -(defun remove-nils (list) +(defun proof-remove-nils (list) (let ((returned-list '())) (while list (if (car list) @@ -779,10 +794,10 @@ Creates a list of all the spans in FILE and checks each one. Terminates when th -(defun remove-duplicates (list) +(defun proof-remove-duplicates (list) (let ((returned-list '())) (while list - (if (not (check-dups (car list) (cdr list))) + (if (not (proof-check-dups (car list) (cdr list))) (setq returned-list (cons (car list) returned-list))) (setq list (cdr list))) returned-list)) @@ -791,7 +806,7 @@ Creates a list of all the spans in FILE and checks each one. Terminates when th -(defun check-dups (element list) +(defun proof-check-dups (element list) (let ((truth nil)) (while list (if (equal element (car list)) diff --git a/generic/proof-script.el b/generic/proof-script.el index fb507593..51bd7b5f 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -496,16 +496,6 @@ Names must be unique for a given " (interactive) (pg-show-all-portions "proof" 'hide)) -;;(defun pg-toggle-proof-visibility () -;; (interactive)) -;; If any proof element is invisible, show all, else hide all. - -; see pg-user.el for span-context-menu default. -; (defun pg-proof-element-menu (name) -; `(,(concat "Proof of " name) -; ["Show" (pg-make-element-visible "proof" ,name)] -; ["Hide" (pg-make-element-invisible "proof" ,name)])) - (defun pg-add-proof-element (name span) (pg-add-element "proof" name span) (set-span-property span 'name name) @@ -1248,14 +1238,13 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; the name of a dependency of that span ;; depcs-within-file returns the names of all the theorems that ;; the span depends on which are in the same file as the theorem. - + ;; See proof-depends.el for code. (if proof-last-theorem-dependencies (progn (if (boundp 'proof-deps-menu) (easy-menu-remove proof-deps-menu)) (set-span-property gspan 'dependencies proof-last-theorem-dependencies) - (set-span-property gspan 'keymap pg-span-context-menu-keymap) (if buffer-file-name (let* ((buffer-file-name-sans-path @@ -1263,12 +1252,12 @@ the ACS is marked in the current buffer. If CMD does not match any, (buffer-file-name-sans-extension (car (split-string buffer-file-name-sans-path "\\."))) (depcs-within-file-list - (dependencies-within-file-list + (proof-dependencies-within-file-list proof-last-theorem-dependencies buffer-file-name-sans-extension))) (set-span-property gspan 'dependencies-within-file depcs-within-file-list) - (update-dependents depcs-within-file-list + (proof-update-dependents depcs-within-file-list buffer-file-name-sans-path buffer-file-name-sans-extension (span-property gspan 'name)) @@ -1284,9 +1273,10 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; da: this code was outside if, I've put it inside now (setq proof-last-theorem-dependencies nil) (setq proof-thm-names-of-files - (merge-names-list-it (span-property gspan 'name) - (buffer-name (span-object gspan)) - proof-thm-names-of-files)))) + (proof-merge-names-list-it + (span-property gspan 'name) + (buffer-name (span-object gspan)) + proof-thm-names-of-files)))) ;; In Coq, we have the invariant that if we've done a save and ;; there's a top-level declaration then it must be the |