-
Notifications
You must be signed in to change notification settings - Fork 88
/
proof-shell.el
2142 lines (1755 loc) · 77.9 KB
/
proof-shell.el
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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
;;; proof-shell.el --- Proof General shell mode
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003-2021 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
;; SPDX-License-Identifier: GPL-3.0-or-later
;;; Commentary:
;;
;; Mode for buffer which interacts with proof assistant.
;; Includes management of a queue of commands waiting to be sent.
;;
;; A big portion of the code in this file implements the callback
;; function that Emacs calls when output arrives from the proof
;; assistant. This callback implements a major feature of Proof
;; General: Sending one command after the other to the proof assistant
;; and processing/displaying the reply.
;;
;; The following documents the call graph of important functions that
;; contribute to this callback. The entry point is
;; `proof-shell-filter-wrapper', which is configured in
;; `scomint-output-filter-functions'. Sending the next comand to the
;; proof assistant and calling the callbacks of the spans happens in
;; `proof-shell-exec-loop'.
;;
;; proof-shell-filter-wrapper
;; -> proof-shell-filter
;; -> proof-shell-process-urgent-messages
;; -> proof-shell-process-urgent-message
;; -> proof-shell-filter-manage-output
;; -> proof-shell-handle-immediate-output
;; -> proof-shell-exec-loop
;; -> proof-tree-check-proof-finish
;; -> proof-shell-handle-error-or-interrupt
;; -> proof-shell-insert-action-item
;; -> proof-shell-invoke-callback
;; -> proof-release-lock
;; -> proof-shell-handle-delayed-output
;; -> proof-tree-handle-delayed-output
;; -> proof-release-lock
;; -> proof-start-prover-with-priority-items-maybe
;;
;;; Code:
(require 'cl-lib) ; cl-set-difference, cl-every
(eval-when-compile
(require 'span)
(require 'proof-utils))
;; declare a few functions and variables from proof-tree - if we
;; require proof-tree the compiler complains about a recusive
;; dependency.
(declare-function proof-tree-handle-delayed-output "proof-tree"
(old-proof-marker cmd flags span))
;; without the nil initialization the compiler still warns about this variable
(defvar proof-tree-external-display)
(require 'scomint)
(require 'pg-response)
(require 'pg-goals)
(require 'pg-user) ; proof-script, new-command-advance
(require 'span)
;;
;; Internal variables used by proof shell
;;
(defvar proof-marker nil
"Marker in proof shell buffer pointing to previous command input.")
(defvar proof-action-list nil
"The main queue of things to do: spans, commands and actions.
The value is a list of lists of the form
(SPAN COMMANDS ACTION [DISPLAYFLAGS])
which is the queue of things to do.
SPAN is a region in the sources, where COMMANDS come from. Often,
additional properties are recorded as properties of SPAN.
COMMANDS is a list of strings, holding the text to be send to the
prover. It might be the empty list if nothing needs to be sent to
the prover, such as, for comments. Usually COMMANDS
contains just 1 string, but it might also contains more elements.
The text should be obtained with
`(mapconcat 'identity COMMANDS \" \")', where the last argument
is a space.
ACTION is the callback to be invoked when this item has been
processed by the prover. For normal scripting items it is
`proof-done-advancing', for retract items
`proof-done-retracting', but there are more possibilities (e.g.
`proof-done-invisible', `proof-shell-set-silent',
`proof-shell-clear-silent' and `proof-tree-show-goal-callback').
The DISPLAYFLAGS are set
for non-scripting commands or for when scripting should not
bother the user. They may include
'invisible non-script command (`proof-shell-invisible-command')
'no-response-display do not display messages in *response* buffer
'no-error-display do not display errors/take error action
'no-goals-display do not goals in *goals* buffer
'proof-tree-show-subgoal item inserted by the proof-tree package
'priority-action item added via proof-add-to-priority-queue
Note that 'invisible does not imply any of the others. If flags
are non-empty, interactive cues will be surpressed. (E.g.,
printing hints).
See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
(defvar proof-priority-action-list nil
"Holds action items to be inserted at the head of `proof-action-list' ASAP.
When the proof assistant is busy, one cannot push to the head of
`proof-action-list`, because the head usually (but not always)
contains the item that the proof assistant is currently
executing. This list therefore holds the items to be executed
before any other items in `proof-action-list'. Inside
`proof-shell-exec-loop', when `proof-action-list' is in the right
state, the content of this list is prepended to
`proof-action-list'. Use `proof-add-to-priority-queue' to add
items to this priority list, to ensure the proof assistant starts
running, in case `proof-action-list' is currently empty.
The items in this list are reversed, that is, the one added last
and to be executed last is at the head.")
(defsubst proof-shell-invoke-callback (listitem)
"From `proof-action-list' LISTITEM, invoke the callback on the span."
(condition-case err
(funcall (nth 2 listitem) (car listitem))
(error
(message "error escaping proof-shell-invoke-callback %s for command %s: %s"
(nth 2 listitem) (nth 1 listitem) err)
nil)))
(defvar proof-second-action-list-active nil
"Signals that some items are waiting outside of `proof-action-list'.
If this is t it means that some items from the queue region are
waiting for being processed in a place different from
`proof-action-list'. In this case Proof General must behave as if
`proof-action-list' would be non-empty, when it is, in fact, empty.
This is used, for instance, for parallel background compilation
for Coq: The Require command and the following items are not put
into `proof-action-list' and are stored somewhere else until the
background compilation finishes. Then those items are put into
`proof-action-list' for getting processed.")
;; We record the last output from the prover and a flag indicating its
;; type, as well as a previous ("delayed") version for when the end
;; of the queue is reached or an error or interrupt occurs.
;;
;; See `proof-shell-last-output', `proof-shell-last-prompt' in
;; pg-vars.el
(defvar proof-shell-last-goals-output ""
"The last displayed goals string.")
(defvar proof-shell-last-response-output ""
"The last displayed response message.")
(defvar proof-shell-delayed-output-start nil
"A record of the start of the previous output in the shell buffer.
The previous output is held back for processing at end of queue.")
(defvar proof-shell-delayed-output-end nil
"A record of the start of the previous output in the shell buffer.
The previous output is held back for processing at end of queue.")
(defvar proof-shell-delayed-output-flags nil
"A copy of the `proof-action-list' flags for `proof-shell-delayed-output'.")
(defvar proof-shell-interrupt-pending nil
"A flag indicating an interrupt is pending.
This ensures that the proof queue will be interrupted even if no
interrupt message is printed from the prover after the last output.")
(defvar proof-shell-exit-in-progress nil
"A flag indicating that the current proof process is about to exit.
This flag is set for the duration of `proof-shell-kill-function'
to tell hooks in `proof-deactivate-scripting-hook' to refrain
from calling `proof-shell-exit'.")
;;
;; Indicator and fake minor mode for active scripting buffer
;;
(defcustom proof-shell-active-scripting-indicator
'(:eval (propertize
" Scripting " 'face
(cond
(proof-shell-busy 'proof-queue-face)
((eq proof-shell-last-output-kind 'error) 'proof-script-sticky-error-face)
((proof-with-current-buffer-if-exists proof-script-buffer
(proof-locked-region-full-p))
'font-lock-type-face)
(t 'proof-locked-face))))
"Modeline indicator for active scripting buffer.
Changes colour to indicate whether the shell is busy, etc."
:type 'sexp
:group 'proof-general-internals)
(unless
(assq 'proof-active-buffer-fake-minor-mode minor-mode-alist)
(setq minor-mode-alist
(append minor-mode-alist
(list
(list
'proof-active-buffer-fake-minor-mode
proof-shell-active-scripting-indicator)))))
;;
;; Implementing the process lock
;;
;; Note that because Emacs Lisp code is single-threaded, there are no
;; concurrency issues here (a loop parsing process output cannot get
;; pre-empted by the user trying to send more input to the process, or
;; by the process filter trying to deal with more output). But the
;; lock allows for clear management of the queue.
;;
;; Three relevant functions:
;;
;; proof-shell-ready-prover
;; starts proof shell, gives error if it's busy.
;;
;; proof-activate-scripting (in proof-script.el)
;; calls proof-shell-ready-prover, and turns on scripting minor
;; mode for current (scripting) buffer.
;;
;; Also, an enabler predicate:
;;
;; proof-shell-available-p
;; returns non-nil if a proof shell is active and not locked.
;;
;;;###autoload
(defun proof-shell-ready-prover (&optional queuemode)
"Make sure the proof assistant is ready for a command.
If QUEUEMODE is set, succeed if the proof shell is busy but
has mode QUEUEMODE, which is a symbol or list of symbols.
Otherwise, if the shell is busy, give an error.
No change to current buffer or point."
(proof-shell-start)
(unless (or (not proof-shell-busy)
(eq queuemode proof-shell-busy)
(and (listp queuemode)
(member proof-shell-busy queuemode)))
(error "Proof process busy!")))
;;;###autoload
(defun proof-shell-live-buffer ()
"Return non-nil if ‘proof-shell-buffer’ is live."
(and proof-shell-buffer
(buffer-live-p proof-shell-buffer)
;; FIXME: Use process-live-p?
(scomint-check-proc proof-shell-buffer)))
;;;###autoload
(defun proof-shell-available-p ()
"Return non-nil if there is a proof shell active and available.
No error messages. Useful as menu or toolbar enabler."
(and (proof-shell-live-buffer)
(not proof-shell-busy)))
(defun proof-grab-lock (&optional queuemode)
"Grab the proof shell lock, starting the proof assistant if need be.
Runs `proof-state-change-hook' to notify state change.
If QUEUEMODE is supplied, set the lock to that value."
(proof-shell-ready-prover queuemode)
(setq proof-shell-interrupt-pending nil
proof-shell-busy (or queuemode t)
proof-shell-last-queuemode proof-shell-busy)
(run-hooks 'proof-state-change-pre-hook)
(run-hooks 'proof-state-change-hook))
(defun proof-release-lock ()
"Release the proof shell lock. Clear `proof-shell-busy'."
(setq proof-shell-busy nil))
;;
;; Starting and stopping the proof shell
;;
(defcustom proof-shell-fiddle-frames t
"Non-nil if proof-shell functions should fire-up/delete frames like crazy."
:type 'boolean
:group 'proof-shell)
(defvar proof-shell-filter-active nil
"Variable equal to t if `proof-shell-filter' is running.")
(defvar proof-shell-filter-was-blocked nil
"Variable equal to t if a recursive call of `proof-shell-filter' was blocked.
In this case `proof-shell-filter' must be called again after it finished.")
(defun proof-shell-set-text-representation ()
"Adjust representation for current buffer, to match `proof-shell-unicode'."
(unless proof-shell-unicode
;; Prevent interpretation of multi-byte characters.
;; Otherwise, chars 128-255 get remapped higher, breaking regexps
(toggle-enable-multibyte-characters -1)))
(defun proof-shell-make-associated-buffers ()
"Create the associated buffers and set buffer variables holding them."
(let ((goals "*goals*")
(resp "*response*")
(trace "*trace*")
(thms "*thms*"))
(setq proof-goals-buffer (get-buffer-create goals))
(setq proof-response-buffer (get-buffer-create resp))
(if proof-shell-trace-output-regexp
(setq proof-trace-buffer (get-buffer-create trace)))
(if proof-shell-thms-output-regexp
(setq proof-thms-buffer (get-buffer-create thms)))
;; Set the special-display-regexps now we have the buffer names
(setq pg-response-special-display-regexp
(proof-regexp-alt goals resp trace thms))))
(defun proof-strip-whitespace-at-end (string)
"Return STRING stripped of all trailing whitespace."
(while (string-match "[\r\n\t ]+$" string)
(setq string (replace-match "" t t string)))
string)
(defvar proof-shell-before-process-hook nil
"Functions run from `proof-shell-start' just before
starting the prover process. Last chance to modify
xxx-prog-args and xxx-prog-name")
(defun proof-shell-start ()
"Initialise a shell-like buffer for a proof assistant.
Does nothing if proof assistant is already running.
Also generates goal and response buffers.
If `proof-prog-name-ask' is set, query the user for the
process command."
(interactive)
(unless (proof-shell-live-buffer)
(setq proof-shell-filter-active nil)
(setq proof-included-files-list nil) ; clear some state
(let ((name (buffer-file-name (current-buffer))))
(if (and name proof-prog-name-guess proof-guess-command-line)
(setq proof-prog-name
(apply proof-guess-command-line (list name)))))
(if proof-prog-name-ask
;; if this option is set, an absolute file name is better to show if possible
(let ((prog-name (locate-file proof-prog-name exec-path exec-suffixes 1)))
(setq proof-prog-name (proof-strip-whitespace-at-end
(read-shell-command "Run process: "
prog-name)))))
;; Once proof-prog-name is set (possibly asked to the user by the
;; code above), some final option setting may need to be done.
(run-hooks 'proof-shell-before-process-hook)
(let
((proc (downcase proof-assistant)))
;; Starting the inferior process (asynchronous)
(let* ((prog-name-list1
(if (functionp (proof-ass-sym prog-args))
;; complex assistants define <PA>-prog-args as function
;; that computes the argument list.
(cons proof-prog-name (funcall (proof-ass-sym prog-args)))
(if (proof-ass prog-args)
;; Intermediate complex assistants set the value
;; of <PA>-prog-args to the argument list.
(cons proof-prog-name (proof-ass prog-args))
;; Trivial assistants simply set proof-prog-name
(split-string proof-prog-name))))
(prog-name-list
;; Splice in proof-rsh-command if it's non-nil
(if (and proof-rsh-command
(> (length proof-rsh-command) 0))
(append (split-string proof-rsh-command)
prog-name-list1)
prog-name-list1))
(prog-command-line (mapconcat 'identity prog-name-list " "))
(process-connection-type
proof-shell-process-connection-type)
;; Trac #324, Trac #284: default with Emacs 23 variants
;; is t. nil gave marginally better results with "make
;; profile.isar" on homogenous test input. Top-level
;; Emacs loop causes slow down on Mac and Windows ports.
(process-adaptive-read-buffering nil)
;; The next few settings control the proof assistant encoding.
;; See Elisp manual for recommendations for coding systems.
;; Modern versions of proof systems should be Unicode
;; clean, i.e., outputing only ASCII characters or using a
;; representation such as UTF-8. Old versions of PG
;; relied on control sequences using 8-bit characters with
;; codes between 127 and 255, this is now deprecated.
;; Backward compatibility: remove UTF-8 encoding if not
;; wanted; it conflicts with using chars 128-255 for
;; markup and results in blocking in C libraries.
(process-environment
(append (proof-ass prog-env) ; custom environment
(if proof-shell-unicode ; if specials not used,
process-environment ; leave it alone
(cons
(if (getenv "LANG")
(format "LANG=%s"
(replace-regexp-in-string
"\\.UTF-8" ""
(getenv "LANG")))
"LANG=C")
(delete
(concat "LANG=" (getenv "LANG"))
process-environment)))))
(normal-coding-system-for-read coding-system-for-read)
(coding-system-for-read
(if proof-shell-unicode
(or (condition-case nil
(check-coding-system 'utf-8)
(error nil))
normal-coding-system-for-read)
(if (string-match "Linux"
(shell-command-to-string "uname"))
'raw-text
normal-coding-system-for-read)))
(coding-system-for-write coding-system-for-read))
(message "Starting: %s" prog-command-line)
(apply 'scomint-make (append (list proc (car prog-name-list) nil)
(cdr prog-name-list)))
(setq proof-shell-buffer (get-buffer (concat "*" proc "*")))
(unless (proof-shell-live-buffer)
;; Give error now if shell buffer isn't live (process exited). We also
;; set the process filter to nil to avoid processing error messages
;; related to the process exit.
(set-process-filter (get-buffer-process proof-shell-buffer) nil)
(setq proof-shell-buffer nil)
(error "Starting process: %s..failed" prog-command-line)))
(proof-shell-make-associated-buffers)
(with-current-buffer proof-shell-buffer
;; Clear and set text representation (see CVS history for comments)
(erase-buffer)
(proof-shell-set-text-representation)
;; Initialise associated buffers
(with-current-buffer proof-response-buffer
(erase-buffer)
(proof-shell-set-text-representation)
(funcall proof-mode-for-response))
(with-current-buffer proof-goals-buffer
(erase-buffer)
(proof-shell-set-text-representation)
(funcall proof-mode-for-goals))
(proof-with-current-buffer-if-exists proof-trace-buffer
(erase-buffer)
(proof-shell-set-text-representation)
(funcall proof-mode-for-response)
(setq pg-response-eagerly-raise nil))
;; Initialise shell mode (calls hook function, after process started)
(funcall proof-mode-for-shell)
;; Check to see that the process is still going. If not,
;; switch buffer to display the error messages to the user.
(unless (proof-shell-live-buffer)
(switch-to-buffer proof-shell-buffer)
(error "%s process exited!" proc))
;; Setting modes initialises local variables which
;; may affect frame/buffer appearance: so we fire up frames
;; once this has been done.
(if proof-shell-fiddle-frames
;; Call multiple-frames-enable in case we need to fire up
;; new frames (NB: sets specifiers to remove modeline)
(save-selected-window
(proof-multiple-frames-enable))))
(message "Starting %s process... done." proc))))
;;
;; Shutting down proof shell and associated buffers
;;
;; Hooks here are handy for liaising with prover config stuff.
(defvar proof-shell-kill-function-hooks nil
"Functions run from `proof-shell-kill-function'.")
(defun proof-shell-kill-function-kill-associated-buffers ()
"Kill the goal, response, and trace buffers, as well as frames if necessary."
;; Remove auxiliary windows, trying to stop proliferation of
;; frames (NB: loses if user has switched buffer in special frame)
(if (and proof-multiple-frames-enable
proof-shell-fiddle-frames)
(proof-delete-all-associated-windows))
(let ((proof-shell-buffer nil)) ;; fool kill buffer hooks
(dolist (buf '(proof-goals-buffer proof-response-buffer
proof-trace-buffer))
(when (buffer-live-p (symbol-value buf))
(delete-windows-on (symbol-value buf))
(kill-buffer (symbol-value buf))
(set buf nil)))))
(defun proof-shell-kill-function ()
"Function run when a proof-shell buffer is killed.
Try to shut down the proof process nicely and clear locked
regions and state variables. Value for `kill-buffer-hook' in
shell buffer, called by `proof-shell-bail-out' if process exits."
(let* ((alive (scomint-check-proc (current-buffer)))
(proc (get-buffer-process (current-buffer)))
(bufname (buffer-name)))
(message "%s, cleaning up and exiting..." bufname)
(let (prover-was-busy)
;; hook functions might set prover-was-busy
(run-hooks 'proof-shell-signal-interrupt-hook))
(redisplay t)
(when (and alive proc)
(catch 'exited
(setq proof-shell-exit-in-progress t)
(set-process-sentinel
proc
(lambda (p m) (throw 'exited t)))
;; Turn off scripting (ensure buffers completely processed/undone)
(proof-deactivate-scripting-auto)
(proof-shell-wait (proof-ass quit-timeout))
;; Try to shut down politely.
(if proof-shell-quit-cmd
(scomint-send-string proc
(concat proof-shell-quit-cmd "\n"))
(scomint-send-eof))
;; Wait for it to die
(let ((timecount (proof-ass quit-timeout))
(proc (get-buffer-process proof-shell-buffer)))
(while (and (> timecount 0)
(scomint-check-proc proof-shell-buffer))
(accept-process-output proc 1 nil 1)
(cl-decf timecount)))
;; Still there, kill it rudely.
(when (memq (process-status proc) '(open run stop))
(message "%s, cleaning up and exiting...killing process" bufname)
(kill-process proc)))
(set-process-sentinel proc nil))
;; Clear all state
(proof-script-remove-all-spans-and-deactivate)
(proof-shell-clear-state)
(run-hooks 'proof-shell-kill-function-hooks)
(when proof-shell-kill-function-also-kills-associated-buffers
(proof-shell-kill-function-kill-associated-buffers))
(setq proof-shell-exit-in-progress nil)
(message "%s exited." bufname)))
(defun proof-shell-clear-state ()
"Clear internal state of proof shell."
(setq proof-action-list nil
proof-included-files-list nil
proof-shell-busy nil
proof-shell-last-queuemode nil
proof-shell-proof-completed nil
proof-nesting-depth 0
proof-shell-silent nil
proof-shell-last-output ""
proof-shell-last-prompt ""
proof-shell-last-output-kind nil
proof-shell-delayed-output-start nil
proof-shell-delayed-output-end nil
proof-shell-delayed-output-flags nil))
(defun proof-shell-exit (&optional dont-ask)
"Query the user and exit the proof process.
This simply kills the `proof-shell-buffer' relying on the hook function
`proof-shell-kill-function' to do the hard work. If optional
argument DONT-ASK is non-nil, the proof process is terminated
without confirmation.
The kill function uses `<PA>-quit-timeout' as a timeout to wait
after sending `proof-shell-quit-cmd' before rudely killing the process.
This function should not be called if
`proof-shell-exit-in-progress' is t, because a recursive call of
`proof-shell-kill-function' will give strange errors."
(interactive "P")
(if (buffer-live-p proof-shell-buffer)
(when (or dont-ask
(yes-or-no-p (format "Exit %s process? " proof-assistant)))
(let ((kill-buffer-query-functions nil)) ; avoid extra dialog
(kill-buffer proof-shell-buffer))
(setq proof-shell-buffer nil))
(error "No proof shell buffer to kill!")))
(defun proof-shell-bail-out (process event)
"Value for the process sentinel for the proof assistant PROCESS.
If the proof assistant dies, run `proof-shell-kill-function' to
cleanup and remove the associated buffers. The shell buffer is
left around so the user may discover what killed the process.
EVENT is the string describing the change."
(message "Process %s %s, shutting down scripting..." process event)
(proof-shell-kill-function)
(message "Process %s %s, shutting down scripting...done." process event))
(defun proof-shell-restart ()
"Clear script buffers and send `proof-shell-restart-cmd'.
All locked regions are cleared and the active scripting buffer
deactivated.
If the proof shell is busy, an interrupt is sent with
`proof-interrupt-process' and we wait until the process is ready.
The restart command should re-synchronize Proof General with the proof
assistant, without actually exiting and restarting the proof assistant
process.
It is up to the proof assistant how much context is cleared: for
example, theories already loaded may be \"cached\" in some way,
so that loading them the next time round only performs a re-linking
operation, not full re-processing. (One way of caching is via
object files, used by Coq)."
(interactive)
(when proof-shell-busy
(proof-interrupt-process)
(proof-shell-wait))
(if (not (proof-shell-live-buffer))
(proof-shell-start) ;; start if not running
;; otherwise clear context
(proof-script-remove-all-spans-and-deactivate)
(proof-shell-clear-state)
(with-current-buffer proof-shell-buffer
(delete-region (point-min) (point-max)))
(if (and (buffer-live-p proof-shell-buffer)
proof-shell-restart-cmd)
(proof-shell-invisible-command
proof-shell-restart-cmd))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Response buffer processing
;;
(defvar proof-shell-urgent-message-marker nil
"Marker in proof shell buffer pointing to end of last urgent message.")
(defvar proof-shell-urgent-message-scanner nil
"Marker in proof shell buffer pointing to scan start for urgent messages.
This is only used in `proof-shell-process-urgent-message'.")
(defun proof-shell-handle-error-output (start-regexp append-face)
"Displays output from process in `proof-response-buffer'.
The output is taken from `proof-shell-last-output' and begins
the first match for START-REGEXP.
If START-REGEXP is nil or no match can be found (which can happen
if output has been garbled somehow), begin from the start of
the output for this command.
This is a subroutine of `proof-shell-handle-error'."
(let ((string proof-shell-last-output) pos)
(if (and start-regexp
(setq pos (string-match start-regexp string)))
(setq string (substring string pos)))
;; Erase if need be, and erase next time round too.
(pg-response-maybe-erase t nil)
;; Coloring the whole message may be ugly ad hide better
;; coloring mechanism.
(if proof-script-color-error-messages
(pg-response-display-with-face string append-face)
(pg-response-display-with-face string))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Processing error output
;;
(defun proof-shell-handle-error-or-interrupt (err-or-int flags)
"React on an error or interrupt message triggered by the prover.
The argument ERR-OR-INT should be set to 'error or 'interrupt
which affects the action taken.
For errors, we first flush unprocessed output (usually goals).
The error message is the (usually) displayed in the response buffer.
For interrupts, a warning message is displayed.
In both cases we then sound a beep, clear the queue and spans and
finally we call `proof-shell-handle-error-or-interrupt-hook'.
Commands which are not part of regular script management (with
FLAGS containing 'no-error-display) will not cause any display action.
This is called in two places: (1) from the output processing
functions, in case we find an error or interrupt message output,
and (2) from the exec loop, in case of a pending interrupt which
didn't cause prover output."
(unless (memq 'no-error-display flags)
(cond
((eq err-or-int 'interrupt)
(pg-response-maybe-erase t t t) ; force cleaned now & next
(proof-shell-handle-error-output
(if proof-shell-truncate-before-error proof-shell-interrupt-regexp)
'proof-error-face)
(pg-response-warning
"Interrupt: script management may be in an inconsistent state
(but it's probably okay)"))
(t ; error
(if proof-shell-delayed-output-start
(save-excursion
(proof-shell-handle-delayed-output)))
(proof-shell-handle-error-output
(if proof-shell-truncate-before-error proof-shell-error-regexp)
'proof-error-face)
(proof-display-and-keep-buffer proof-response-buffer))))
(proof-with-current-buffer-if-exists proof-shell-buffer
(proof-shell-error-or-interrupt-action err-or-int)))
(defun proof-shell-error-or-interrupt-action (err-or-int)
"Take action on errors or interrupts.
ERR-OR-INT is a flag, 'error or 'interrupt.
This is a subroutine of `proof-shell-handle-error-or-interrupt'.
Must be called with proof shell buffer current.
This function invokes `proof-shell-handle-error-or-interrupt-hook'
unless the FLAGS for the command are non-nil (see `proof-action-list')."
(unless proof-shell-quiet-errors
(beep))
(let* ((fatalitem (car-safe proof-action-list))
(badspan (car-safe fatalitem))
(flags (if fatalitem (nth 3 fatalitem))))
(proof-with-current-buffer-if-exists proof-script-buffer
(save-excursion
(proof-script-clear-queue-spans-on-error badspan
(eq err-or-int 'interrupt))))
;; Note: coq-par-emergency-cleanup, which might be called via
;; proof-shell-handle-error-or-interrupt-hook below, assumes that
;; proof-action-list is empty on error.
(setq proof-action-list nil)
(proof-release-lock)
(unless flags
;; Give a hint about C-c C-`. (NB: approximate test)
(if (pg-response-has-error-location)
(pg-next-error-hint))
;; Run hooks for additional effects, e.g. highlight or moving pointer
(run-hooks 'proof-shell-handle-error-or-interrupt-hook))))
(defun proof-goals-pos (span maparg)
"Given a SPAN, return the start of it if corresponds to a goal, nil otherwise."
(and (eq 'goal (car (span-property span 'proof-top-element)))
(span-start span)))
(defun proof-pbp-focus-on-first-goal ()
"If the `proof-goals-buffer' contains goals, bring the first one into view.
This is a hook function for proof-shell-handle-delayed-output-hook."
)
;; PG 4.0 FIXME
; (let
; ((pos (map-extents 'proof-goals-pos proof-goals-buffer
; nil nil nil nil 'proof-top-element)))
; (and pos (set-window-point
; (get-buffer-window proof-goals-buffer t) pos)))))
(defsubst proof-shell-string-match-safe (regexp string)
"Like (string-match REGEXP STRING), but return nil if REGEXP is nil."
(and regexp (string-match regexp string)))
(defun proof-shell-handle-immediate-output (cmd start end flags)
"See if the output between START and END must be dealt with immediately.
To speed up processing, PG tries to avoid displaying output that
the user will not have a chance to see. Some output must be
handled immediately, however: these are errors, interrupts,
goals and loopbacks (proof step hints/proof by pointing results).
In this function we check, in turn:
`proof-shell-interrupt-regexp'
`proof-shell-error-regexp'
`proof-shell-proof-completed-regexp'
`proof-shell-result-start'
Other kinds of output are essentially display only, so only
dealt with if necessary.
To extend this, set `proof-shell-handle-output-system-specific',
which is a hook to take particular additional actions.
This function sets variables: `proof-shell-last-output-kind',
and the counter `proof-shell-proof-completed' which counts commands
after a completed proof."
(setq proof-shell-last-output-kind nil) ; unclassified
(goto-char start)
(cond
;; TODO: Isabelle has changed (since 2009) and is now amalgamating
;; output between prompts, and does e.g.,
;; GOALS
;; ERROR
;; we need to override delayed output from the previous
;; command with delayed output from this command to handle that!
((proof-re-search-forward-safe proof-shell-interrupt-regexp end t)
(setq proof-shell-last-output-kind 'interrupt)
(proof-shell-handle-error-or-interrupt 'interrupt flags))
((proof-re-search-forward-safe proof-shell-error-regexp end t)
(setq proof-shell-last-output-kind 'error)
(proof-shell-handle-error-or-interrupt 'error flags))
((proof-re-search-forward-safe proof-shell-result-start end t)
;; NB: usually the action list is empty, strange results likely if
;; more commands follow. Therefore, this case might be delayed.
(let (pstart pend)
(setq pstart (+ 1 (match-end 0)))
(re-search-forward proof-shell-result-end end t)
(setq pend (- (match-beginning 0) 1))
(proof-shell-insert-loopback-cmd
(buffer-substring-no-properties pstart pend)))
(setq proof-shell-last-output-kind 'loopback)
(proof-shell-exec-loop))
((proof-re-search-forward-safe proof-shell-proof-completed-regexp end t)
(setq proof-shell-proof-completed 0))) ; commands since complete
;; PG4.0 change: simplify and run earlier
(if proof-shell-handle-output-system-specific
(funcall proof-shell-handle-output-system-specific
cmd proof-shell-last-output)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Interrupts
;;
(defun proof-interrupt-process ()
"Interrupt the proof assistant. Warning! This may confuse Proof General.
This sends an interrupt signal to the proof assistant, if Proof General
thinks it is busy.
This command is risky because we don't know whether the last command
succeeded or not. The assumption is that it didn't, which should be true
most of the time, and all of the time if the proof assistant has a careful
handling of interrupt signals.
Some provers may ignore (and lose) interrupt signals, or fail to indicate
that they have been acted upon yet stop in the middle of output.
In the first case, PG will terminate the queue of commands at the first
available point. In the second case, you may need to press enter inside
the prover command buffer (e.g., with Isabelle2009 press RET inside *isabelle*)."
(interactive)
(let ((prover-was-busy nil))
(unless (proof-shell-live-buffer)
(error "Proof process not started!"))
;; Hook functions might set prover-was-busy.
;; In case `proof-action-list' is empty and only
;; `proof-second-action-list-active' is t, the hook functions
;; should clear the queue region and release the proof shell lock.
;; `coq-par-user-interrupt' actually does this.
(run-hooks 'proof-shell-signal-interrupt-hook)
(if proof-shell-busy
(progn
(setq proof-shell-interrupt-pending t)
(with-current-buffer proof-shell-buffer
(interrupt-process)))
(unless prover-was-busy
(error "Proof process not active!")))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Low-level commands for shell communication
;;
;;;###autoload
(defun proof-shell-insert (strings action &optional scriptspan)
"Insert STRINGS at the end of the proof shell, call `scomint-send-input'.
STRINGS is a list of strings (which will be concatenated), or a
single string.
The ACTION argument is a symbol which is typically the name of a
callback for when each string has been processed.
This calls `proof-shell-insert-hook'. The arguments ACTION and
SCRIPTSPAN may be examined by the hook to determine how to modify
the string variable (exploiting dynamic scoping) which will be
the command actually sent to the shell.
Note that the hook is not called for the empty (null) string
or a carriage return.
We strip the string of carriage returns before inserting it
and updating `proof-marker' to point to the end of the newly
inserted text.
Do not use this function directly, or output will be lost. It is only
used in `proof-add-to-queue' when we start processing a queue, and in
`proof-shell-exec-loop', to process the next item."
(cl-assert (or (stringp strings)
(listp strings))
nil "proof-shell-insert: expected string list argument")
(with-current-buffer proof-shell-buffer
(goto-char (point-max))
;; TEMP: next step: preprocess list of strings directly
(let ((string (if (stringp strings) strings
(apply 'concat strings))))
;; Hook for munging `string' and other dirty hacks.
(run-hooks 'proof-shell-insert-hook)
;; Replace CRs from string with spaces to avoid spurious prompts.
(if proof-shell-strip-crs-from-input
(setq string (subst-char-in-string ?\n ?\ string)))
(insert string)
;; Advance the proof-marker, if synchronization has been gained.
;; Null marker => no yet synced; output is ignored.
(unless (null (marker-position proof-marker))
(set-marker proof-marker (point)))
(scomint-send-input))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Code for manipulating proof queue
;;
(defun proof-shell-action-list-item (cmd callback &optional flags)
"Return action list entry run CMD with callback CALLBACK and FLAGS.
The queue entry does not refer to a span in the script buffer."
(list nil (list cmd) callback flags))
(defun proof-shell-set-silent (span)
"Callback for `proof-shell-start-silent'.
Very simple function but it's important to give it a name to help
track what happens in the proof queue."
(setq proof-shell-silent t))
(defun proof-shell-start-silent-item ()
"Return proof queue entry for starting silent mode."