Cleanup. Add more insertion commands.

1 files changed, 10 insertions, 7 deletions

diff --git a/isar/isar-mmm.el b/isar/isar-mmm.el
index ceffa85c..7517aad5 100644
--- a/isar/isar-mmm.el
+++ b/isar/isar-mmm.el
@@ -35,8 +35,8 @@
 (defconst isar-start-sml-regexp 
   (concat
    "\\(" 
-   (proof-ids-to-regexp (list "ML" "ML_command" "ML_setup"
-			      "typed_print_translation"))
+   (proof-ids-to-regexp 
+    (list "ML" "ML_command" "ML_setup" "typed_print_translation"))
    "\\)[ \t]+{\\*"))
 
 
@@ -47,17 +47,20 @@
    :face mmm-comment-submode-face
    :front ,isar-start-latex-regexp 
    :back  "\\*}"
-   :insert ((?t isartext nil @ "text {*" @ " " _ " " @ "*}" @))
-   :save-matches 1)
+   :insert ((?t isar-text nil @ "text {*" @ " " _ " " @ "*}" @)
+	    (?s isar-section nil @ "section {*" @ " " _ " " @ "*}" @)
+	    (?d  isar-header nil @ "header {*" @ " " _ " " @ "*}" @)))
 
   (isar-sml
    :submode sml-mode
    :face mmm-code-submode-face
    :front ,isar-start-sml-regexp
    :back  "\\*}"
-   :insert ((?M isarml nil @ "ML_setup {*" @ " " _ " " @ "*}" @))
-   :save-matches 1)))
-   
+   :insert ((?u isar-ML-setup nil @ "ML_setup {*" @ " " _ " " @ "*}" @)
+	    (?c isar-ML-command nil @ "ML_command {*" @ " " _ " " @ "*}" @)
+	    (?m isar-ML nil @ "ML {*" @ " " _ " " @ "*}" @)
+	    (?p isar-print-trans nil @ "typed_print_translation {*" @ " " _ " " @ "*}" @)))))
+	    
 
 (provide 'isar-mmm)