From 10385afbe5ad48cdb5a6de7c937884941a3a3886 Mon Sep 17 00:00:00 2001 From: Thomas Kleymann Date: Thu, 5 Dec 1996 17:15:19 +0000 Subject: added variable pbp-mode-is so that pbp-mode can be inherited --- pbp.el | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/pbp.el b/pbp.el index e250f454..3713e288 100644 --- a/pbp.el +++ b/pbp.el @@ -3,7 +3,7 @@ ;; Copyright (C) 1996 LFCS Edinburgh & INRIA Sophia Antipolis ;; Author: Yves Bertot < Yves.Bertot@sophia.inria.fr> ;; Maintainer: LEGO Team -;; 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)) -- cgit v1.2.3