diff options
| author | David Aspinall | 2002-11-18 22:01:49 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-11-18 22:01:49 +0000 |
| commit | 257d140db218b53f5469b4dd2a05557bc92db050 (patch) | |
| tree | d757d2e89eec16ce0e466c4b90e446508d2999b8 | |
| parent | f97f8a8f12f0fb6b82cd7d8d4cc34250234e155a (diff) | |
Add proof-shell-issue-pgip-cmd using ProofGeneral.process_pgip.
| -rw-r--r-- | isa/isa.el | 1 | ||||
| -rw-r--r-- | isa/isabelle-system.el | 13 | ||||
| -rw-r--r-- | isar/isar.el | 1 |
3 files changed, 15 insertions, 0 deletions
@@ -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." |