[emacs-mode] enable yas-snippets for holscript mode more readily

Also adjust some of the snippets for more modern syntax.

tools/editor-modes/emacs/holscript-mode.el

@@ -1394,3 +1394,16 @@ class characters.")
 
 (setq auto-mode-alist (cons '("Script\\.sml" . holscript-mode)
                             auto-mode-alist))
+
+(if (fboundp 'yas-minor-mode)
+    (progn
+      (setq yas-snippet-dirs
+            (append
+             yas-snippet-dirs
+             (list (concat
+                    hol-dir
+                    "tools/editor-modes/emacs/yasnippets"))))
+      (yas-reload-all)
+      (add-hook 'holscript-mode-hook #'yas-minor-mode)
+      (add-hook 'holscript-mode-hook
+                (lambda () (setq yas-also-auto-indent-first-line t)))))

tools/editor-modes/emacs/yasnippets/holscript-mode/Cases

@@ -2,5 +2,6 @@
 # name: Automatic case distinction for leading universal quantifier
 # key: Cases
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
 Cases $0

tools/editor-modes/emacs/yasnippets/holscript-mode/Cases_on

@@ -2,5 +2,6 @@
 # name: Automatic case distinction for given expression
 # key: Cases_on
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
 Cases_on \`$1\` $0

tools/editor-modes/emacs/yasnippets/holscript-mode/Definition

@@ -1,8 +1,8 @@
 # -*- mode: snippet -*-
 # name: Definition of functions HOL4
 # key: Define
-# expand-env: ((yas-indent-line 'fixed))
+# expand-env: ((yas-indent-line 'auto))
 # --
-Definition $1_def:
-  $2
+Definition ${1:name}_def${2:[${3:attributes}]}:
+  ${4:equation(s)}
 End

tools/editor-modes/emacs/yasnippets/holscript-mode/Induct

@@ -2,5 +2,6 @@
 # name: Perform induction on first variable behind universal quantifier
 # key: Induct
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
 Induct

tools/editor-modes/emacs/yasnippets/holscript-mode/Induct_on

@@ -1,6 +1,7 @@
 # -*- mode: snippet -*-
-# name: Perform induction on given variable
+# name: Perform induction on given variable/term
 # key: Induct_on
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
-Induct_on \`$1\` $0
+Induct_on ‘$1’ $0

tools/editor-modes/emacs/yasnippets/holscript-mode/Theorem

@@ -1,10 +1,10 @@
 # -*- mode: snippet -*-
-# name: Theorem statement in HOl4
+# name: Theorem statement in HOL4
 # key: Theorem
 # expand-env: ((yas-indent-line 'fixed))
 # --
-Theorem $1:
-  $2
+Theorem ${1:theorem-name}${2:[${3:attributes}]}:
+  ${4:theorem-statement}
 Proof
-  $3
-End
+  $0
+QED

tools/editor-modes/emacs/yasnippets/holscript-mode/metis_tac

@@ -2,5 +2,6 @@
 # name: Apply first-order prover metis to current goal
 # key: metis_tac
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
-metis_tac [$1] $0
+metis_tac [${1:theorems}] $0

tools/editor-modes/emacs/yasnippets/holscript-mode/once_rewrite_tac

@@ -2,5 +2,6 @@
 # name: rewrite theorems only once
 # key: once_rewrite_tac
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
 once_rewrite_tac [${1:theorem list}] $0

tools/editor-modes/emacs/yasnippets/holscript-mode/qpat_x_assum

@@ -2,5 +2,6 @@
 # name: Find first assumption matching pattern, give it to theorem tactic and remove it
 # key: qpat_x_assum
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
-qpat_x_assum \`${1:term pattern}\` ${2:theorem tactic} $0
+qpat_x_assum ‘${1:term pattern}’ ${2:theorem tactic} $0

tools/editor-modes/emacs/yasnippets/holscript-mode/qspecl_then

@@ -1,6 +1,7 @@
 # -*- mode: snippet -*-
-# name: Specialize given theorem based on term list, then give to theorem tactic
+# name: Specialize theorem with term list, then give to theorem tactic
 # key: qspecl_then
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
 qspecl_then [${1:term quotations}] ${2:theorem tactic} ${3:theorem}

tools/editor-modes/emacs/yasnippets/holscript-mode/resolve

@@ -2,7 +2,6 @@
 # name: Automatic resolution of a theorem until no resolution possible
 # key: resolve
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
-drule $1
-\\\\ rpt (disch_then drule)
-\\\\ $0
+drule $1 >> rpt (disch_then drule) $0

tools/editor-modes/emacs/yasnippets/holscript-mode/sg

@@ -1,8 +1,8 @@
 # -*- mode: snippet -*-
 # name: create a new subgoal prove with corresponding by clause
-# key: sg
+# key: by
 # expand-env: ((yas-indent-line 'fixed))
+# group: tactics
 # --
-\`${1:subgoal}\`
-  by (
-    $0)
+‘${1:subgoal}’
+  by ($0)