From d5b15c0fb62aa93bcb03b3a73f203f087494823a Mon Sep 17 00:00:00 2001
From: Makarius Wenzel
Date: Wed, 19 Jul 2000 15:04:49 +0000
Subject: use ML_command to avoid unwanted output;

---
 isar/isar.el | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'isar')

diff --git a/isar/isar.el b/isar/isar.el
index 647fd320..90e2250b 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -211,7 +211,7 @@
    proof-shell-prompt-pattern		"^\\w*[>#] "
 
    ;; for issuing command, not used to track cwd in any way.
-   proof-shell-cd-cmd			"ML {* Library.cd \"%s\" *}"
+   proof-shell-cd-cmd			"ML_command {* Library.cd \"%s\" *}"
 
    ;; Escapes for filenames inside ML strings.
    ;; We also make a hack for a bug in Isabelle, by switching from 
@@ -501,7 +501,7 @@ proof-shell-retract-files-regexp."
 		  ;; proof-segment-upto-cmdstart (which becomes even more
 		  ;; Isar specific, then...)
 		  ;; (if (string-match "\\.ML$" (buffer-name proof-script-buffer))
-		  ;;    (format "ML_setup {* %s *};" string)
+		  ;;    (format "ML_command {* %s *};" string)
 		  ;;    string)
 		  string
 		  "\\<^sync>;"))))
-- 
cgit v1.2.3