Add proof-shell-theorem-dependency-list-split

2 files changed, 12 insertions, 1 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index cc71eb11..3f880639 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1966,6 +1966,16 @@ This is an experimental feature, currently work-in-progress."
   :type '(choice nil regexp)
   :group 'proof-shell)
 
+(defcustom proof-shell-theorem-dependency-list-split nil
+  "Regexp used to split the list of strings which match
+`proof-shell-theorem-dependency-list-regexp'.  Used as
+an argument to `split-string'; nil defaults to whitespace.
+(This setting is necessary for provers which allow whitespace in
+the names of theorems/definitions/constants), see setting for
+Isabelle in isa/isa.el and isar/isar.el."
+  :type '(choice nil regexp)
+  :group 'proof-shell)
+
 (defcustom proof-shell-show-dependency-cmd nil
   "Command sent to the prover to display a dependency.
 This is typically a command used to print a theorem, constant, or whatever.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index fdb5413d..03c6f29d 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1232,7 +1232,8 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end."
      ((and proof-shell-theorem-dependency-list-regexp 
 	   (string-match proof-shell-theorem-dependency-list-regexp message))
       (setq proof-last-theorem-dependencies 
-	    (split-string (match-string 1 message))))
+	    (split-string (match-string 1 message) 
+			  proof-shell-theorem-dependency-list-split)))
 
      ;; CASE tracing output: output in the tracing buffer instead
      ;; of the response buffer