emacs-mode: fix failure to handle Unicode lambda λ in tokenization

tools/holscript-mode.el

@@ -42,6 +42,7 @@
     (modify-syntax-entry ?‘ "(’" st)
     (modify-syntax-entry ?’ ")‘" st)
     (modify-syntax-entry ?\\ "\\" st)
+    (modify-syntax-entry ?λ "." st)
     ;; backslash only escapes in strings but we need to have it seen
     ;; as one in general if the hol-mode isn't to get seriously
     ;; confused by script files that contain escaped quotation
@@ -1061,7 +1062,8 @@ ignoring fact that it should really only occur at the beginning of the line.")
        ((looking-back "\\\\\\\\" (- (point) 3))
         (goto-char (match-beginning 0)) "\\\\")
        (; am I just after either a backslash or Greek lambda?
-        (looking-back (concat "[^$[:punct:]]" holscript-lambda-regexp)
+        (looking-back (concat "\\([^$[:punct:]]\\|[~()“‘]\\)"
+                              holscript-lambda-regexp)
                       (- (point) 3) nil)
         (if (equal 1 (syntax-class (syntax-after (point))))
             (buffer-substring-no-properties

tools/mode-tests/holscript-tests.el

@@ -103,7 +103,8 @@
      (should (move-check '(4435 4452 4505 4552) 'forward-sexp))
      (should (move-check '(4455 4505) 'forward-sexp))
      (should (move-check '(4508 4455 4435) 'backward-sexp))
-     (should (move-check '(3943 3959 3999 4046) 'forward-sexp)))))
+     (should (move-check '(3943 3959 3999 4046) 'forward-sexp))
+     (should (move-check '(4599 4558) 'backward-sexp)))))
 
 (ert-deftest holscript-sexp-movement ()
   "sexp-moves are made correctly"

tools/mode-tests/sampleScript.sml

@@ -275,6 +275,8 @@ Inductive foob2:
   (l. foob (HD l) ==> foob (LAST l))
 End
 
-
+Definition foo:
+  foo x = λy z. y + z
+End
 
 val _ = export_theory()