From 97c10f623dc9a61c625d466b87c9a626d3aa30f8 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 29 Sep 1999 16:28:29 +0000
Subject: Extended documentation for proof-shell-restart.

---
 generic/proof-shell.el | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index f9db16ce..022f592f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -421,8 +421,15 @@ left around so the user may discover what killed the process."
 (defun proof-shell-restart ()
   "Clear script buffers and send proof-shell-restart-cmd.
 All locked regions are cleared and the active scripting buffer
-deactivated.  The restart command should re-synchronize
-Proof General with the proof assistant."
+deactivated.  
+
+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 does not require re-processing."
   (interactive)
   (proof-script-remove-all-spans-and-deactivate)
   (setq proof-included-files-list nil
-- 
cgit v1.2.3