[nongnu] elpa/proof-general 4814efb366: proof-shell: document call graph

[ELPA Syncer]

branch: elpa/proof-general
commit 4814efb3668ec6c6a747c6b95691ca79d9f94bca
Author: Hendrik Tews <hendrik@askra.de>
Commit: hendriktews <hendrik@askra.de>

    proof-shell: document call graph
---
 generic/proof-shell.el | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index bdb7037f94..3de1c87684 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -19,6 +19,35 @@
 ;; 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-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: