From 0dd3ac1f157750367f637d80d4cd2e5dc1f34279 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 21 Nov 2002 14:41:29 +0000
Subject: markup ml for Isar

---
 isa/isabelle-system.el | 7 +++++--
 1 file 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
-- 
cgit v1.2.3