Add proof-shell-issue-pgip-cmd using ProofGeneral.process_pgip.

2 files changed, 14 insertions, 0 deletions

diff --git a/isa/isa.el b/isa/isa.el
index 7adcc3fc..b433e6d7 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -196,6 +196,7 @@ and script mode."
 
    ;; Isabelle is learning to talk PGIP...
    proof-shell-match-pgip-cmd		"<pgip"
+   proof-shell-issue-pgip-cmd		'isabelle-process-pgip
 
    ;; Some messages delimited by eager annotations
    proof-shell-clear-response-regexp    "Proof General, please clear the response buffer."
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index bedd87cd..c08ad39e 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -462,5 +462,18 @@ the function `pg-remove-specials' can be used instead)."
 	       (not (string-equal thm proof-unnamed-theorem-name)))))))
 
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; XML as an SML string: add escapes for quotes
+;;
+
+(defun isabelle-xml-sml-escapes (xmlstring)
+  (replace-regexp-in-string "\"" "\\\"" xmlstring))
+
+(defun isabelle-process-pgip (xmlstring)
+  (format "ProofGeneral.process_pgip(\"%s\");"
+	  (isabelle-xml-sml-escapes xmlstring)))
+
 (provide 'isabelle-system)
 ;; End of isabelle-system.el