emacs-mode: handle colons better (different in HOL and SML contexts)

tools/holscript-mode.el

@@ -368,7 +368,8 @@ a store_thm equivalent.")
                          holscript-quotedmaterial-delimiter-fullregexp nil t))
           (setq ppss (syntax-ppss)))
         (and beginmatch
-             (or (looking-at holscript-quoteddeclaration-begin)
+             (or (and (looking-at holscript-quoteddeclaration-begin)
+                      (>= p (match-end 0)))
                  (looking-at "[“‘]")))))))
 
 (defun holscript-find-syntax-error (limit)
@@ -752,7 +753,7 @@ a store_thm equivalent.")
             ("structure" id))
       (theorem-contents (id-quoted "^Proof" tactic))
       (definition-contents (id-quoted "^Termination" tactic) (id-quoted))
-      (id-quoted (id ":" quotedmaterial))
+      (id-quoted (id "SML:" quotedmaterial))
       (quotedmaterial
         ("QFIER." quotedmaterial "ENDQ." quotedmaterial)
         (quotedmaterial "/\\" quotedmaterial)
@@ -774,6 +775,7 @@ a store_thm equivalent.")
         (quotedmaterial "<-" quotedmaterial)
         (quotedmaterial "|" quotedmaterial)
         (quotedmaterial "=>" quotedmaterial)
+        (quotedmaterial ":" quotedmaterial)
         ("[defnlabel]" quotedmaterial)
         ("case" quotedmaterial "of" quotedmaterial)
         ("do" quotedmaterial "od")
@@ -800,14 +802,15 @@ a store_thm equivalent.")
     '((assoc "^Proof")
       (left ">>" "\\\\" ">-"  ">|" "THEN" "THEN1" "THENL" "THEN_LT" ">~")
       (assoc "by" "suffices_by"))
-    '((assoc "ENDQ." "QFIER." "in" "of")
+    '((assoc "ENDQ." "QFIER." "in" "of") ; HOL syntax
       (assoc "|")
       (assoc "=>")
       (assoc "else")
       (assoc "<=>" "⇔" "<-")
       (assoc "==>" "⇒") (assoc "\\/" "∨") (assoc "/\\" "∧")
       (assoc "[defnlabel]")
-      (assoc "=" "<" "≤" "<=") (assoc ":=") (assoc "++" "+") (assoc "*")))))
+      (assoc "=" "<" "≤" "<=") (assoc ":=") (assoc "++" "+") (assoc "*")
+      (assoc ":")))))
 
 (defvar holscript-quotedmaterial-delimiter-regexp
   (regexp-opt (list "“" "”" "‘" "’" holscript-quoteddeclaration-begin)))
@@ -925,6 +928,10 @@ ignoring fact that it should really only occur at the beginning of the line.")
                (save-excursion (skip-chars-backward " \t") (bolp)))
           (goto-char (match-end 0))
           "[defnlabel]")
+         ((looking-at ":\\([^[:punct:]]\\|[(]\\)")
+          (let ((p (point)))
+            (goto-char (1- (match-end 0)))
+            (if (holscript-in-quotedmaterialp p) ":" "SML:")))
          ((looking-at "\\\\/") (goto-char (match-end 0)) "\\/")
          ((looking-at "/\\\\") (goto-char (match-end 0)) "/\\")
          ((looking-at "\\\\\\\\") (goto-char (match-end 0)) "\\\\")
@@ -1080,6 +1087,9 @@ ignoring fact that it should really only occur at the beginning of the line.")
         (goto-char (match-beginning 0)) "\\/")
        ((looking-back "/\\\\" (- (point) 3))
         (goto-char (match-beginning 0)) "/\\")
+       ((looking-back "\\([^[:punct:]]\\|[])]\\):" (- (point) 3))
+        (goto-char (1+ (match-beginning 0)))
+        (if (holscript-in-quotedmaterialp (point)) ":" "SML:"))
        ((looking-back (regexp-quote "|>") (- (point) 3))
         (goto-char (match-beginning 0))
         (if (holscript-in-quotedmaterialp (point)) "|>" "SML|>"))
@@ -1116,14 +1126,14 @@ ignoring fact that it should really only occur at the beginning of the line.")
                      (point) kind token)
   (pcase (cons kind token)
     (`(:elem  . basic) (holscript-message "In elem rule") 0)
-    (`(:list-intro . ":")
+    (`(:list-intro . "SML:")
      (holscript-message "In list-intro :")
      holscript-indent-level)
     (`(:list-intro . "‘") 1)
     (`(:list-intro . "“") 1)
     (`(:list-intro . "")
      (holscript-message "In (:list-intro \"\"))") holscript-indent-level)
-    (`(:after . ":") 2)
+    (`(:after . "SML:") 2)
     (`(:before . "SML|>")
      (holscript-message "|> Current column = %d" (current-column))
      (save-mark-and-excursion
@@ -1175,7 +1185,7 @@ ignoring fact that it should really only occur at the beginning of the line.")
      (and (not (smie-rule-bolp))
           (smie-rule-prev-p "else")
           (smie-rule-parent)))
-    (`(:before . ":") holscript-indent-level)
+    (`(:before . "SML:") holscript-indent-level)
     (`(:after . "=>") 2)
     (`(:after . "do") 2)
     ; (`(:before . "==>") 2)

tools/mode-tests/indentScript.sml

@@ -282,4 +282,11 @@ Proof
   tac
 QED
 
+Theorem foo_bar:
+  f x : bool ∧
+  Q
+Proof
+  tactic
+QED
+
 val _ = export_theory();