1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
;;; pg-goals.el --- Proof General goals buffer mode.
;; 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, Yves Bertot, Healfdene Goguen,
;; Thomas Kleymann and Dilip Sequeira
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;; Commentary:
;;; Code:
(eval-when-compile
(require 'easymenu) ; easy-menu-add, etc
(require 'cl) ; incf
(require 'span) ; span-*
(defvar proof-goals-mode-menu) ; defined by macro below
(defvar proof-assistant-menu)) ; defined by macro in proof-menu
(require 'pg-assoc)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Goals buffer mode
;;
;;;###autload
(define-derived-mode proof-goals-mode proof-universal-keys-only-mode
proof-general-name
"Mode for goals display.
May enable proof-by-pointing or similar features.
\\{proof-goals-mode-map}"
(setq proof-buffer-type 'goals)
(add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
(easy-menu-add proof-goals-mode-menu proof-goals-mode-map)
(easy-menu-add proof-assistant-menu proof-goals-mode-map)
(proof-toolbar-setup)
(buffer-disable-undo)
(if proof-keep-response-history (bufhist-mode)) ; history for contents
(set-buffer-modified-p nil)
(setq cursor-in-non-selected-windows nil))
;;
;; Menu for goals buffer
;;
(proof-eval-when-ready-for-assistant ; proof-aux-menu depends on <PA>
(easy-menu-define proof-goals-mode-menu
proof-goals-mode-map
"Menu for Proof General goals buffer."
(proof-aux-menu)))
;;
;; Keys for goals buffer
;;
(define-key proof-goals-mode-map [q] 'bury-buffer)
;; TODO: use standard Emacs button behaviour here (cf Info mode)
(define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
(define-key proof-goals-mode-map [C-M-mouse-3]
'proof-undo-and-delete-last-successful-command)
;;
;; The completion of init
;;
;;;###autoload
(defun proof-goals-config-done ()
"Initialise the goals buffer after the child has been configured."
(setq font-lock-defaults '(proof-goals-font-lock-keywords)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Goals buffer processing
;;
(defun pg-goals-display (string keepresponse)
"Display STRING in the `proof-goals-buffer', properly marked up.
Converts term substructure markup into mouse-highlighted extents.
The response buffer may be cleared to avoid confusing the user
with output associated with a previous goals message. This
function tries to do that by calling `pg-response-maybe-erase'.
If KEEPRESPONSE is non-nil, we assume that a response message
corresponding to this goals message has already been displayed
before this goals message (see `proof-shell-handle-delayed-output'),
so the response buffer should not be cleared."
(save-excursion
;; Response buffer may be out of date. It may contain (error)
;; messages relating to earlier proof states
;; Erase the response buffer if need be, maybe removing the
;; window. Indicate it should be erased before the next output.
(pg-response-maybe-erase t t nil keepresponse)
;; Erase the goals buffer and add in the new string
(set-buffer proof-goals-buffer)
(setq buffer-read-only nil)
(unless (eq 0 (buffer-size))
(bufhist-checkpoint-and-erase))
;; Only display if string is non-empty.
(unless (string-equal string "")
(insert string))
(setq buffer-read-only t)
(set-buffer-modified-p nil)
;; Keep point at the start of the buffer.
(proof-display-and-keep-buffer
proof-goals-buffer (point-min))))
;;
;; Actions in the goals buffer
;;
(defun pg-goals-button-action (event)
"Construct a command based on the mouse-click EVENT."
(interactive "e")
(let* ((posn (event-start event))
(pos (posn-point posn))
(buf (window-buffer (posn-window posn)))
(props (text-properties-at pos buf))
(sendback (plist-get props 'sendback)))
(cond
(sendback
(with-current-buffer buf
(let* ((cmdstart (previous-single-property-change pos 'sendback
nil (point-min)))
(cmdend (next-single-property-change pos 'sendback
nil (point-max)))
(cmd (buffer-substring-no-properties cmdstart cmdend)))
(proof-insert-sendback-command cmd)))))))
(provide 'pg-goals)
;;; pg-goals.el ends here
|
