diff options
Diffstat (limited to 'generic/proof-depends.el')
| -rw-r--r-- | generic/proof-depends.el | 29 |
1 files changed, 17 insertions, 12 deletions
diff --git a/generic/proof-depends.el b/generic/proof-depends.el index c55df53d..72beb1d2 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -1,21 +1,28 @@ ;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies -;; -;; Copyright (C) 2000-2004, 2010 University of Edinburgh. + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> ;; Earlier version by Fiona McNeil. + ;; License: GPL (GNU GENERAL PUBLIC LICENSE) -;; Status: Experimental code + +;;; Commentary: ;; -;; $Id$ +;; Status: Experimental code ;; -;;; Commentary: -;; ;; Based on Fiona McNeill's MSc project on analysing dependencies ;; within proofs. Code rewritten by David Aspinall. ;; - - +;;; Code: (require 'cl) (require 'span) (require 'pg-vars) @@ -34,9 +41,6 @@ A list of lists; the first element of each list is a file-name, the second element a list of all the def names in that file. i.e.: ((file-name-1 (def1 def2 def3)) (file-name-2 (def1 def2 def3)))") - -;;; Code: - ;; Utility functions (defun proof-depends-module-name-for-buffer () @@ -177,7 +181,7 @@ Called from `proof-done-advancing' when a save is processed and (vector menuname nil nil)))) (defun proof-dep-split-deps (deps) - "Split dependencies into named nested lists according to dotted prefixes." + "Split dependencies DEPS into named nested lists according to dotted prefixes." ;; NB: could handle deeper nesting here, but just do one level for now. (let (nested toplevel) ;; Add each name into a nested list or toplevel list @@ -219,6 +223,7 @@ NAMEFN is applied to each element of LIST to make the names." (defun proof-goto-dependency (name span) "Go to the start of SPAN." + ;; FIXME(EMD): seems buggy as NAME is not used ;; FIXME: check buffer is right one. Later we'll allow switching buffer ;; here and jumping to different files. (goto-char (span-start span)) |