diff options
| author |  Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1996-12-05 17:15:19 +0000 |
|---|---|---|
| committer | Thomas Kleymann <da+pg-tms@inf.ed.ac.uk> | 1996-12-05 17:15:19 +0000 |
| commit | 10385afbe5ad48cdb5a6de7c937884941a3a3886 (patch) | |
| tree | 3b1fa5d083811cb3f72e78b4a13c9475ecd37994 /pbp.el | |
| parent | 84724259c3d4658c3d37dde3502e90262db3ff65 (diff) | |
added variable pbp-mode-is so that pbp-mode can be inherited
Diffstat (limited to 'pbp.el')
| -rw-r--r-- | pbp.el | 7 |
1 files changed, 5 insertions, 2 deletions
@@ -3,7 +3,7 @@ ;; Copyright (C) 1996 LFCS Edinburgh & INRIA Sophia Antipolis ;; Author: Yves Bertot < Yves.Bertot@sophia.inria.fr> ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> -;; Time-stamp: <03 Dec 96 tms /home/tms/elisp/pbp.el> +;; Time-stamp: <05 Dec 96 tms /home/tms/elisp/pbp.el> ;; Reference: Yves Bertot and Laurent Théry ;; A Generic Approach to Building User Interfaces for ;; Theorem Provers @@ -92,6 +92,9 @@ (deflocal pbp-keymap (make-keymap 'Pbp-keymap) "Keymap for pbp mode") +(deflocal pbp-mode-is nil + "The actual mode for Proof-by-Pointing.") + (defun pbp-analyse-structure () (map-extents (lambda (ext maparg) @@ -258,7 +261,7 @@ (save-excursion (setq pbp-goals-buffer (get-buffer-create pbp-goals-buffer-name )) (set-buffer pbp-goals-buffer) - (pbp-mode) + (funcall pbp-mode-is) (erase-buffer pbp-goals-buffer) (add-hook 'comint-output-filter-functions 'pbp-filter t) (pbp-sanitise-region (point-min) (point-max)) |