From fb474f38984c9752e0ca06dbf70a176af93bedc3 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 29 May 2000 18:33:15 +0000
Subject: Use generic default setting mechanism now.  Add isar-markup-ml here.

---
 isar/isar.el | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/isar/isar.el b/isar/isar.el
index 24d54fc2..5775f24d 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -184,10 +184,6 @@
       found-header)))
 
 
-;;; NB!  Disadvantage of *not* shadowing variables is that user
-;;; cannot override them.  It might be nice to override some
-;;; variables, which ones?
-
 (defun isar-mode-config-set-variables ()
   "Configure generic proof scripting mode variables for Isabelle/Isar."
   (setq
@@ -275,11 +271,13 @@
 
    ;; initial command configures Isabelle/Isar by modifying print
    ;; functions, restoring settings saved by Proof General, etc.
-   proof-shell-pre-sync-init-cmd	(isar-verbatim "ProofGeneral.init true;")
-   proof-shell-init-cmd                 (isabelle-set-default-cmd)
+   proof-shell-pre-sync-init-cmd	(isar-verbatim 
+					 "ProofGeneral.init true;")
+   proof-shell-init-cmd                 (proof-assistant-settings-cmd)
    proof-shell-restart-cmd		"ProofGeneral.restart;"
    proof-shell-quit-cmd			(isar-verbatim "quit();")
-   
+   proof-assistant-setting-format	'isar-markup-ml
+
    proof-shell-eager-annotation-start-length 1
    proof-shell-eager-annotation-start   "\360\\|\362"
    proof-shell-eager-annotation-end     "\361\\|\363"
@@ -525,6 +523,10 @@ proof-shell-retract-files-regexp."
       (setq string (match-string 1 string))
     (setq string (concat "\\<^sync>" (isar-shell-adjust-line-width) string "\\<^sync>;"))))
 
+(defun isar-markup-ml (string)
+  "Return marked up version of ML command STRING for Isar."
+  (format "ML_command {* %s *};" string))
+
 (defun isar-mode-config ()
   (isar-mode-config-set-variables)
   (isar-init-syntax-table)
-- 
cgit v1.2.3