aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2002-11-21 14:41:29 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2002-11-21 14:41:29 +0000
commit0dd3ac1f157750367f637d80d4cd2e5dc1f34279 (patch)
tree40cf7b5ab9f8fc0e9dd3f2e9c2728d98ee33e299 /isa
parent9798eefc31212f619cfabf80cfd36f5485a8f2ed (diff)
markup ml for Isar
Diffstat (limited to 'isa')
-rw-r--r--isa/isabelle-system.el7
1 files changed, 5 insertions, 2 deletions
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el
index 70e625b0..a4814fb1 100644
--- a/isa/isabelle-system.el
+++ b/isa/isabelle-system.el
@@ -489,8 +489,11 @@ the function `pg-remove-specials' can be used instead)."
(replace-regexp-in-string "\"" "\\\"" xmlstring))
(defun isabelle-process-pgip (xmlstring)
- (format "ProofGeneral.process_pgip(\"%s\");"
- (isabelle-xml-sml-escapes xmlstring)))
+ (let ((mlcmd (format "ProofGeneral.process_pgip(\"%s\");"
+ (isabelle-xml-sml-escapes xmlstring))))
+ (if (eq proof-assistant-symbol 'isar)
+ (isar-markup-ml mlcmd)
+ mlcmd)))
(provide 'isabelle-system)
;; End of isabelle-system.el