From 257d140db218b53f5469b4dd2a05557bc92db050 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 18 Nov 2002 22:01:49 +0000
Subject: Add proof-shell-issue-pgip-cmd using ProofGeneral.process_pgip.

---
 isa/isa.el             |  1 +
 isa/isabelle-system.el | 13 +++++++++++++
 isar/isar.el           |  1 +
 3 files changed, 15 insertions(+)

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
diff --git a/isar/isar.el b/isar/isar.el
index 2b04a912..0775b018 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -227,6 +227,7 @@ See -k option for Isabelle interface script."
 
    ;; 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."
-- 
cgit v1.2.3