diff --git a/tools/editor-modes/emacs/tree-sitter/holscript-ts-mode.el b/tools/editor-modes/emacs/tree-sitter/holscript-ts-mode.el
new file mode 100644
index 0000000000..3fff10ad6f
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/holscript-ts-mode.el
@@ -0,0 +1,209 @@
+(require 'treesit)
+
+;; References
+;; * https://github.com/nverno/sml-ts-mode
+;; * https://github.com/HOL-Theorem-Prover/HOL (holscript-mode.el)
+;; * https://www.masteringemacs.org/article/lets-write-a-treesitter-major-mode
+
+(defvar holscript-ts-mode--syntax-table
+  (let ((st (make-syntax-table)))
+    (modify-syntax-entry ?\* ". 23n" st)
+    (modify-syntax-entry ?\( "()1" st)
+    (modify-syntax-entry ?\) ")(4" st)
+    (modify-syntax-entry ?“ "(”" st)
+    (modify-syntax-entry ?” ")“" st)
+    (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
+    ;; characters. This despite the fact that it does cause pain in
+    ;; terms such as \(x,y). x + y
+    (mapc (lambda (c) (modify-syntax-entry c "w" st)) "'")
+    (mapc (lambda (c) (modify-syntax-entry c "_" st)) "$_")
+    (mapc (lambda (c) (modify-syntax-entry c "."  st)) ".%&+-/:<=>?@`^|!~#,;∀∃")
+    st)
+  "Syntax table used in `holscript-ts-mode'.")
+
+(defconst holscript-ts-mode--sml-keywords
+  '(;; Reserved Words Core
+    "abstype" "and" "andalso" "as" "case" "datatype" "do" "else" "end"
+    "exception" "fn" "fun" "handle" "if" "in" "infix" "infixr" "let"
+    "local" "nonfix" "of" "op" "open" "orelse" "raise" "rec" "then"
+    "type" "val" "with" "withtype" "while"
+    ;; Reserved Words Modules
+    "eqtype" "functor" "include" "sharing" "sig" "signature" "struct"
+    "structure" "where")
+  "SML keywords for tree-sitter font-locking.")
+
+(defconst holscript-ts-mode--hol-keywords
+  '("Definition" "Theorem" "Termination" "Proof" "Datatype:" "End" "QED"
+    "if" "then" "else" "case" "of")
+  "HOL keywords for tree-sitter font-locking.")
+
+(defconst holscript-ts-mode--sml-builtins
+  '("abs" "app" "before" "ceil" "chr" "concat" "exnMessage" "exnName" "explode"
+    "floor" "foldl" "foldr" "getOpt" "hd" "ignore" "implode" "isSome" "length"
+    "map" "null" "ord" "print" "real" "rev" "round" "size" "str" "substring"
+    "tl" "trunc" "valOf" "vector")
+  "SML builtin functions for tree-sitter font-locking.")
+
+(defvar holscript-ts-mode--font-lock-feature-list
+  '((comment definition)
+    (keyword string)
+    (builtin constant number type property)
+    (assignment bracket delimiter operator))
+  "Font-lock features for `treesit-font-lock-feature-list' in `holscript-ts-mode'.")
+
+(defun holscript-ts-mode--fontify-patterns (node override start end &rest _args)
+  "Fontify pattern bindings and in NODE.
+For a description of OVERRIDE, START, and END, see `treesit-font-lock-rules'."
+  (pcase (treesit-node-type node)
+    ((or "typed_pat" "paren_pat" "tuple_pat" "conj_pat")
+     (holscript-ts-mode--fontify-patterns
+      (treesit-node-child node 0 t) override start end))
+    ("app_pat"
+     ;; Fontify both bindings in (h::t)
+     (when (equal "::" (treesit-node-text (treesit-node-child node 1)))
+       (holscript-ts-mode--fontify-patterns
+        (treesit-node-child node 0 t) override start end))
+     (holscript-ts-mode--fontify-patterns
+      (treesit-node-child node 1 t) override start end))
+    ((or "vid_pat" "wildcard_pat")
+     (treesit-fontify-with-override
+      (treesit-node-start node) (treesit-node-end node)
+      'font-lock-variable-name-face
+      override start end))))
+
+(defvar holscript-ts-mode--font-lock-settings
+  (treesit-font-lock-rules
+   :language 'holscript
+   :feature 'comment ; SML and HOL
+   '((block_comment) @font-lock-comment-face)
+
+   :language 'holscript
+   :feature 'string
+   '(;; SML
+     (string_scon) @font-lock-string-face
+     (char_scon) @font-lock-constant-face
+     ;; HOL
+     (hol_string) @font-lock-string-face
+     (hol_character) @font-lock-constant-face)
+
+   :language 'holscript
+   :feature 'keyword
+   `(;; SML
+     [,@holscript-ts-mode--sml-keywords] @font-lock-keyword-face
+     ;; Misinterpreted identifiers, eg. val x = struct
+     ;; See notes from highlights.scm (MatthewFluet/tree-sitter-sml)
+     ([(vid) (tycon) (strid) (sigid) (fctid)] @font-lock-warning-face
+      (:match ,(rx-to-string `(seq bos (or ,@holscript-ts-mode--sml-keywords) eos))
+              @font-lock-warning-face))
+     ;; As an additional special case, The Defn of SML excludes `*` from tycon.
+     ([(tycon)] @font-lock-warning-face
+      (:match ,(rx bos "*" eos) @font-lock-warning-face))
+     ;; HOL
+     [,@holscript-ts-mode--hol-keywords] @font-lock-keyword-face)
+
+   :language 'holscript
+   :feature 'builtin
+   `(;; SML
+     ((vid_exp) @font-lock-builtin-face
+      (:match ,(rx-to-string `(seq bos (or ,@holscript-ts-mode--sml-builtins) eos))
+              @font-lock-builtin-face))
+     ((vid_exp) @font-lock-preprocessor-face
+      (:match ,(rx bos (or "use") eos) @font-lock-preprocessor-face)))
+
+   :language 'holscript
+   :feature 'definition
+   (let ((pats '((app_pat) (paren_pat) (vid_pat) (tuple_pat) (wildcard_pat))))
+     `(;; SML
+       (fmrule
+        name: (_) @font-lock-function-name-face
+        ([,@pats] :* @holscript-ts-mode--fontify-patterns :anchor "=") :?)
+       (mrule ([,@pats] :* @holscript-ts-mode--fontify-patterns :anchor "=>"))
+       (handle_exp (mrule (_) @holscript-ts-mode--fontify-patterns))
+       (labvar_patrow [(vid)] @font-lock-variable-name-face)
+       (patrow (vid_pat) @holscript-ts-mode--fontify-patterns)
+       (tuple_pat (_) @holscript-ts-mode--fontify-patterns
+                  ("," (vid_pat) @holscript-ts-mode--fontify-patterns) :*)
+       (app_pat (_) (_) @holscript-ts-mode--fontify-patterns)
+       (valbind pat: (_) @holscript-ts-mode--fontify-patterns)
+       (valdesc name: (vid) @font-lock-variable-name-face)
+       ;; Modules, Sigs
+       (fctbind name: (_) @font-lock-module-def-face
+                arg: (strid) :? @font-lock-variable-name-face)
+       (strbind name: (_) @font-lock-module-def-face)
+       (sigbind name: (_) @font-lock-module-def-face)
+       ;; Types
+       (datatype_dec (datbind name: (tycon) @font-lock-type-def-face))
+       (datatype_spec (datdesc name: (tycon) @font-lock-type-def-face))
+       (datatype_dec
+        withtype: (typbind name: (tycon) @font-lock-type-def-face))
+       (type_dec (typbind name: (tycon) @font-lock-type-def-face))
+       (type_spec (typbind name: (tycon) @font-lock-type-def-face))
+       (typedesc name: (_) @font-lock-type-def-face)
+       (infix_dec (vid) @font-lock-function-name-face)
+       ;; Uppercase does not mean we have a type
+       ;; ((vid) @font-lock-type-face
+       ;;  (:match "^[A-Z].*" @font-lock-type-face))
+       ;; HOL
+       ((hol_defname) @font-lock-variable-name-face)
+       (hol_eqn (hol_identifier) @font-lock-function-name-face)
+       ((hol_variable) @font-lock-variable-name-face)))
+
+   :language 'holscript
+   :feature 'constant
+   `(;; SML
+     ((vid) @font-lock-constant-face
+      (:match ,(rx bos (or "true" "false" "nil" "ref") eos)
+              @font-lock-constant-face))
+     (recordsel_exp ((lab) @font-lock-constant-face
+                     (:match "^[0-9]+$" @font-lock-constant-face))))
+
+   :language 'holscript
+   :feature 'property  ; SML only?
+   `((tyrow (lab) @font-lock-property-name-face)
+     (patrow (lab) @font-lock-property-use-face)
+     (exprow (lab) @font-lock-property-use-face))
+
+   :language 'holscript
+   :feature 'type
+   `(;; SML
+     (fn_ty "->" @font-lock-type-face)
+     (tuple_ty "*" @font-lock-type-face)
+     (paren_ty ["(" ")"] @font-lock-type-face)
+     (tyvar) @font-lock-type-face
+     [(strid) (sigid) (fctid)] @font-lock-type-face
+     (record_ty ["{" "," "}"] @font-lock-type-face
+                (tyrow [(lab) ":"] @font-lock-type-face) :?
+                (ellipsis_tyrow ["..." ":"] @font-lock-type-face) :?)
+     (tycon_ty (tyseq ["(" "," ")"] @font-lock-type-face) :?
+               (longtycon) @font-lock-type-face)
+     ;; HOL
+     ([(hol_atomic_type) (hol_list_ty) (hol_fun_ty)] @font-lock-type-face))
+
+   :language 'holscript
+   :feature 'number
+   '(;; SML
+     [(integer_scon) (word_scon) (real_scon)] @font-lock-number-face)))
+
+;;;###autoload
+(define-derived-mode holscript-ts-mode prog-mode "HOLScript[ts]"
+  "Major mode for editing HOL Script.sml files with tree-sitter."
+  :syntax-table holscript-ts-mode--syntax-table
+
+  (when (treesit-ready-p 'holscript)
+    (treesit-parser-create 'holscript)
+
+    ;; Font-Locking
+    (setq-local treesit-font-lock-settings
+                holscript-ts-mode--font-lock-settings)
+    (setq-local treesit-font-lock-feature-list
+                holscript-ts-mode--font-lock-feature-list)
+
+    (treesit-major-mode-setup)))
+
+(provide 'holscript-ts-mode)
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.editorconfig b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.editorconfig
new file mode 100644
index 0000000000..7756ee9511
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.editorconfig
@@ -0,0 +1,43 @@
+root = true
+
+[*]
+charset = utf-8
+
+[*.{json,toml,yml,gyp}]
+indent_style = space
+indent_size = 2
+
+[*.js]
+indent_style = space
+indent_size = 2
+
+[*.scm]
+indent_style = space
+indent_size = 2
+
+[*.{c,cc,h}]
+indent_style = space
+indent_size = 4
+
+[*.rs]
+indent_style = space
+indent_size = 4
+
+[*.{py,pyi}]
+indent_style = space
+indent_size = 4
+
+[*.swift]
+indent_style = space
+indent_size = 4
+
+[*.go]
+indent_style = tab
+indent_size = 8
+
+[Makefile]
+indent_style = tab
+indent_size = 8
+
+[parser.c]
+indent_size = 2
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.gitattributes b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.gitattributes
new file mode 100644
index 0000000000..9d5c5d499a
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.gitattributes
@@ -0,0 +1,13 @@
+* text=auto eol=lf
+
+src/*.json linguist-generated
+src/parser.c linguist-generated
+src/tree_sitter/* linguist-generated
+
+bindings/** linguist-generated
+binding.gyp linguist-generated
+setup.py linguist-generated
+Makefile linguist-generated
+CMakeLists.txt linguist-generated
+Package.swift linguist-generated
+go.mod linguist-generated
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.gitignore b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.gitignore
new file mode 100644
index 0000000000..4ab3968cbc
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/.gitignore
@@ -0,0 +1,45 @@
+# Files created by tree-sitter generate
+src/grammar.json
+src/node-types.json
+src/parser.c
+
+# Rust artifacts
+target/
+
+# Node artifacts
+build/
+prebuilds/
+node_modules/
+
+# Swift artifacts
+.build/
+
+# Go artifacts
+_obj/
+
+# Python artifacts
+.venv/
+dist/
+*.egg-info
+*.whl
+
+# C artifacts
+*.a
+*.so
+*.so.*
+*.dylib
+*.dll
+*.pc
+
+# Example dirs
+/examples/*/
+
+# Grammar volatiles
+*.wasm
+*.obj
+*.o
+
+# Archives
+*.tar.gz
+*.tgz
+*.zip
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/CMakeLists.txt b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/CMakeLists.txt
new file mode 100644
index 0000000000..1d41a240b6
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/CMakeLists.txt
@@ -0,0 +1,60 @@
+cmake_minimum_required(VERSION 3.13)
+
+project(tree-sitter-holscript
+        VERSION "0.1.0"
+        DESCRIPTION "HOLScript grammar for tree-sitter"
+        HOMEPAGE_URL "https://github.com/hol-theorem-prover/hol/"
+        LANGUAGES C)
+
+option(BUILD_SHARED_LIBS "Build using shared libraries" ON)
+option(TREE_SITTER_REUSE_ALLOCATOR "Reuse the library allocator" OFF)
+
+set(TREE_SITTER_ABI_VERSION 14 CACHE STRING "Tree-sitter ABI version")
+if(NOT ${TREE_SITTER_ABI_VERSION} MATCHES "^[0-9]+$")
+    unset(TREE_SITTER_ABI_VERSION CACHE)
+    message(FATAL_ERROR "TREE_SITTER_ABI_VERSION must be an integer")
+endif()
+
+find_program(TREE_SITTER_CLI tree-sitter DOC "Tree-sitter CLI")
+
+add_custom_command(OUTPUT "${CMAKE_CURRENT_SOURCE_DIR}/src/parser.c"
+                   DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/src/grammar.json"
+                   COMMAND "${TREE_SITTER_CLI}" generate src/grammar.json
+                            --abi=${TREE_SITTER_ABI_VERSION}
+                   WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+                   COMMENT "Generating parser.c")
+
+add_library(tree-sitter-holscript src/parser.c)
+if(EXISTS src/scanner.c)
+  target_sources(tree-sitter-holscript PRIVATE src/scanner.c)
+endif()
+target_include_directories(tree-sitter-holscript PRIVATE src)
+
+target_compile_definitions(tree-sitter-holscript PRIVATE
+                           $<$<BOOL:${TREE_SITTER_REUSE_ALLOCATOR}>:TREE_SITTER_REUSE_ALLOCATOR>
+                           $<$<CONFIG:Debug>:TREE_SITTER_DEBUG>)
+
+set_target_properties(tree-sitter-holscript
+                      PROPERTIES
+                      C_STANDARD 11
+                      POSITION_INDEPENDENT_CODE ON
+                      SOVERSION "${TREE_SITTER_ABI_VERSION}.${PROJECT_VERSION_MAJOR}"
+                      DEFINE_SYMBOL "")
+
+configure_file(bindings/c/tree-sitter-holscript.pc.in
+               "${CMAKE_CURRENT_BINARY_DIR}/tree-sitter-holscript.pc" @ONLY)
+
+include(GNUInstallDirs)
+
+install(FILES bindings/c/tree-sitter-holscript.h
+        DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}/tree_sitter")
+install(FILES "${CMAKE_CURRENT_BINARY_DIR}/tree-sitter-holscript.pc"
+        DESTINATION "${CMAKE_INSTALL_DATAROOTDIR}/pkgconfig")
+install(TARGETS tree-sitter-holscript
+        LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}")
+
+add_custom_target(test "${TREE_SITTER_CLI}" test
+                  WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
+                  COMMENT "tree-sitter test")
+
+# vim:ft=cmake:
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Cargo.toml b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Cargo.toml
new file mode 100644
index 0000000000..ee295a8ec5
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Cargo.toml
@@ -0,0 +1,27 @@
+[package]
+name = "tree-sitter-holscript"
+description = "HOLScript grammar for tree-sitter"
+version = "0.1.0"
+authors = ["Daniel Nezamabadi"]
+license = "MIT"
+readme = "README.md"
+keywords = ["incremental", "parsing", "tree-sitter", "holscript"]
+categories = ["parsing", "text-editors"]
+repository = "https://github.com/hol-theorem-prover/hol/"
+edition = "2021"
+autoexamples = false
+
+build = "bindings/rust/build.rs"
+include = ["bindings/rust/*", "grammar.js", "queries/*", "src/*"]
+
+[lib]
+path = "bindings/rust/lib.rs"
+
+[dependencies]
+tree-sitter-language = "0.1"
+
+[build-dependencies]
+cc = "1.1.22"
+
+[dev-dependencies]
+tree-sitter = "0.24.3"
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Makefile b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Makefile
new file mode 100644
index 0000000000..574245a7d2
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Makefile
@@ -0,0 +1,94 @@
+ifeq ($(OS),Windows_NT)
+$(error Windows is not supported)
+endif
+
+LANGUAGE_NAME := tree-sitter-holscript
+HOMEPAGE_URL := https://github.com/hol-theorem-prover/hol/
+VERSION := 0.1.0
+
+# repository
+SRC_DIR := src
+
+TS ?= tree-sitter
+
+# install directory layout
+PREFIX ?= /usr/local
+INCLUDEDIR ?= $(PREFIX)/include
+LIBDIR ?= $(PREFIX)/lib
+PCLIBDIR ?= $(LIBDIR)/pkgconfig
+
+# source/object files
+PARSER := $(SRC_DIR)/parser.c
+EXTRAS := $(filter-out $(PARSER),$(wildcard $(SRC_DIR)/*.c))
+OBJS := $(patsubst %.c,%.o,$(PARSER) $(EXTRAS))
+
+# flags
+ARFLAGS ?= rcs
+override CFLAGS += -I$(SRC_DIR) -std=c11 -fPIC
+
+# ABI versioning
+SONAME_MAJOR = $(shell sed -n 's/\#define LANGUAGE_VERSION //p' $(PARSER))
+SONAME_MINOR = $(word 1,$(subst ., ,$(VERSION)))
+
+# OS-specific bits
+ifeq ($(shell uname),Darwin)
+	SOEXT = dylib
+	SOEXTVER_MAJOR = $(SONAME_MAJOR).$(SOEXT)
+	SOEXTVER = $(SONAME_MAJOR).$(SONAME_MINOR).$(SOEXT)
+	LINKSHARED = -dynamiclib -Wl,-install_name,$(LIBDIR)/lib$(LANGUAGE_NAME).$(SOEXTVER),-rpath,@executable_path/../Frameworks
+else
+	SOEXT = so
+	SOEXTVER_MAJOR = $(SOEXT).$(SONAME_MAJOR)
+	SOEXTVER = $(SOEXT).$(SONAME_MAJOR).$(SONAME_MINOR)
+	LINKSHARED = -shared -Wl,-soname,lib$(LANGUAGE_NAME).$(SOEXTVER)
+endif
+ifneq ($(filter $(shell uname),FreeBSD NetBSD DragonFly),)
+	PCLIBDIR := $(PREFIX)/libdata/pkgconfig
+endif
+
+all: lib$(LANGUAGE_NAME).a lib$(LANGUAGE_NAME).$(SOEXT) $(LANGUAGE_NAME).pc
+
+lib$(LANGUAGE_NAME).a: $(OBJS)
+	$(AR) $(ARFLAGS) $@ $^
+
+lib$(LANGUAGE_NAME).$(SOEXT): $(OBJS)
+	$(CC) $(LDFLAGS) $(LINKSHARED) $^ $(LDLIBS) -o $@
+ifneq ($(STRIP),)
+	$(STRIP) $@
+endif
+
+$(LANGUAGE_NAME).pc: bindings/c/$(LANGUAGE_NAME).pc.in
+	sed -e 's|@PROJECT_VERSION@|$(VERSION)|' \
+		-e 's|@CMAKE_INSTALL_LIBDIR@|$(LIBDIR:$(PREFIX)/%=%)|' \
+		-e 's|@CMAKE_INSTALL_INCLUDEDIR@|$(INCLUDEDIR:$(PREFIX)/%=%)|' \
+		-e 's|@PROJECT_DESCRIPTION@|$(DESCRIPTION)|' \
+		-e 's|@PROJECT_HOMEPAGE_URL@|$(HOMEPAGE_URL)|' \
+		-e 's|@CMAKE_INSTALL_PREFIX@|$(PREFIX)|' $< > $@
+
+$(PARSER): $(SRC_DIR)/grammar.json
+	$(TS) generate $^
+
+install: all
+	install -d '$(DESTDIR)$(INCLUDEDIR)'/tree_sitter '$(DESTDIR)$(PCLIBDIR)' '$(DESTDIR)$(LIBDIR)'
+	install -m644 bindings/c/$(LANGUAGE_NAME).h '$(DESTDIR)$(INCLUDEDIR)'/tree_sitter/$(LANGUAGE_NAME).h
+	install -m644 $(LANGUAGE_NAME).pc '$(DESTDIR)$(PCLIBDIR)'/$(LANGUAGE_NAME).pc
+	install -m644 lib$(LANGUAGE_NAME).a '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).a
+	install -m755 lib$(LANGUAGE_NAME).$(SOEXT) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER)
+	ln -sf lib$(LANGUAGE_NAME).$(SOEXTVER) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER_MAJOR)
+	ln -sf lib$(LANGUAGE_NAME).$(SOEXTVER_MAJOR) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXT)
+
+uninstall:
+	$(RM) '$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).a \
+		'$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER) \
+		'$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXTVER_MAJOR) \
+		'$(DESTDIR)$(LIBDIR)'/lib$(LANGUAGE_NAME).$(SOEXT) \
+		'$(DESTDIR)$(INCLUDEDIR)'/tree_sitter/$(LANGUAGE_NAME).h \
+		'$(DESTDIR)$(PCLIBDIR)'/$(LANGUAGE_NAME).pc
+
+clean:
+	$(RM) $(OBJS) $(LANGUAGE_NAME).pc lib$(LANGUAGE_NAME).a lib$(LANGUAGE_NAME).$(SOEXT)
+
+test:
+	$(TS) test
+
+.PHONY: all install uninstall clean test
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Package.swift b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Package.swift
new file mode 100644
index 0000000000..8b32ac2f54
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/Package.swift
@@ -0,0 +1,37 @@
+// swift-tools-version:5.3
+import PackageDescription
+
+let package = Package(
+    name: "TreeSitterHolscript",
+    products: [
+        .library(name: "TreeSitterHolscript", targets: ["TreeSitterHolscript"]),
+    ],
+    dependencies: [
+        .package(url: "https://github.com/ChimeHQ/SwiftTreeSitter", from: "0.8.0"),
+    ],
+    targets: [
+        .target(
+            name: "TreeSitterHolscript",
+            dependencies: [],
+            path: ".",
+            sources: [
+                "src/parser.c",
+                // NOTE: if your language has an external scanner, add it here.
+            ],
+            resources: [
+                .copy("queries")
+            ],
+            publicHeadersPath: "bindings/swift",
+            cSettings: [.headerSearchPath("src")]
+        ),
+        .testTarget(
+            name: "TreeSitterHolscriptTests",
+            dependencies: [
+                "SwiftTreeSitter",
+                "TreeSitterHolscript",
+            ],
+            path: "bindings/swift/TreeSitterHolscriptTests"
+        )
+    ],
+    cLanguageStandard: .c11
+)
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/binding.gyp b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/binding.gyp
new file mode 100644
index 0000000000..cd5baa0ce1
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/binding.gyp
@@ -0,0 +1,30 @@
+{
+  "targets": [
+    {
+      "target_name": "tree_sitter_holscript_binding",
+      "dependencies": [
+        "<!(node -p \"require('node-addon-api').targets\"):node_addon_api_except",
+      ],
+      "include_dirs": [
+        "src",
+      ],
+      "sources": [
+        "bindings/node/binding.cc",
+        "src/parser.c",
+        # NOTE: if your language has an external scanner, add it here.
+      ],
+      "conditions": [
+        ["OS!='win'", {
+          "cflags_c": [
+            "-std=c11",
+          ],
+        }, { # OS == "win"
+          "cflags_c": [
+            "/std:c11",
+            "/utf-8",
+          ],
+        }],
+      ],
+    }
+  ]
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/c/tree-sitter-holscript.h b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/c/tree-sitter-holscript.h
new file mode 100644
index 0000000000..8d1c60acd1
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/c/tree-sitter-holscript.h
@@ -0,0 +1,16 @@
+#ifndef TREE_SITTER_HOLSCRIPT_H_
+#define TREE_SITTER_HOLSCRIPT_H_
+
+typedef struct TSLanguage TSLanguage;
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+const TSLanguage *tree_sitter_holscript(void);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // TREE_SITTER_HOLSCRIPT_H_
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/c/tree-sitter-holscript.pc.in b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/c/tree-sitter-holscript.pc.in
new file mode 100644
index 0000000000..f0bf1ce40e
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/c/tree-sitter-holscript.pc.in
@@ -0,0 +1,11 @@
+prefix=@CMAKE_INSTALL_PREFIX@
+libdir=${prefix}/@CMAKE_INSTALL_LIBDIR@
+includedir=${prefix}/@CMAKE_INSTALL_INCLUDEDIR@
+
+Name: tree-sitter-holscript
+Description: @PROJECT_DESCRIPTION@
+URL: @PROJECT_HOMEPAGE_URL@
+Version: @PROJECT_VERSION@
+Requires: @TS_REQUIRES@
+Libs: -L${libdir} -ltree-sitter-holscript
+Cflags: -I${includedir}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/go/binding.go b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/go/binding.go
new file mode 100644
index 0000000000..540725c264
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/go/binding.go
@@ -0,0 +1,13 @@
+package tree_sitter_holscript
+
+// #cgo CFLAGS: -std=c11 -fPIC
+// #include "../../src/parser.c"
+// // NOTE: if your language has an external scanner, add it here.
+import "C"
+
+import "unsafe"
+
+// Get the tree-sitter Language for this grammar.
+func Language() unsafe.Pointer {
+	return unsafe.Pointer(C.tree_sitter_holscript())
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/go/binding_test.go b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/go/binding_test.go
new file mode 100644
index 0000000000..00331dc8ae
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/go/binding_test.go
@@ -0,0 +1,15 @@
+package tree_sitter_holscript_test
+
+import (
+	"testing"
+
+	tree_sitter "github.com/tree-sitter/go-tree-sitter"
+	tree_sitter_holscript "github.com/hol-theorem-prover/hol//bindings/go"
+)
+
+func TestCanLoadGrammar(t *testing.T) {
+	language := tree_sitter.NewLanguage(tree_sitter_holscript.Language())
+	if language == nil {
+		t.Errorf("Error loading Holscript grammar")
+	}
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/binding.cc b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/binding.cc
new file mode 100644
index 0000000000..91523f08bc
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/binding.cc
@@ -0,0 +1,20 @@
+#include <napi.h>
+
+typedef struct TSLanguage TSLanguage;
+
+extern "C" TSLanguage *tree_sitter_holscript();
+
+// "tree-sitter", "language" hashed with BLAKE2
+const napi_type_tag LANGUAGE_TYPE_TAG = {
+    0x8AF2E5212AD58ABF, 0xD5006CAD83ABBA16
+};
+
+Napi::Object Init(Napi::Env env, Napi::Object exports) {
+    exports["name"] = Napi::String::New(env, "holscript");
+    auto language = Napi::External<TSLanguage>::New(env, tree_sitter_holscript());
+    language.TypeTag(&LANGUAGE_TYPE_TAG);
+    exports["language"] = language;
+    return exports;
+}
+
+NODE_API_MODULE(tree_sitter_holscript_binding, Init)
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/binding_test.js b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/binding_test.js
new file mode 100644
index 0000000000..afede30a7b
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/binding_test.js
@@ -0,0 +1,9 @@
+/// <reference types="node" />
+
+const assert = require("node:assert");
+const { test } = require("node:test");
+
+test("can load grammar", () => {
+  const parser = new (require("tree-sitter"))();
+  assert.doesNotThrow(() => parser.setLanguage(require(".")));
+});
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/index.d.ts b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/index.d.ts
new file mode 100644
index 0000000000..efe259eed0
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/index.d.ts
@@ -0,0 +1,28 @@
+type BaseNode = {
+  type: string;
+  named: boolean;
+};
+
+type ChildNode = {
+  multiple: boolean;
+  required: boolean;
+  types: BaseNode[];
+};
+
+type NodeInfo =
+  | (BaseNode & {
+      subtypes: BaseNode[];
+    })
+  | (BaseNode & {
+      fields: { [name: string]: ChildNode };
+      children: ChildNode[];
+    });
+
+type Language = {
+  name: string;
+  language: unknown;
+  nodeTypeInfo: NodeInfo[];
+};
+
+declare const language: Language;
+export = language;
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/index.js b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/index.js
new file mode 100644
index 0000000000..6657bcf42d
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/node/index.js
@@ -0,0 +1,7 @@
+const root = require("path").join(__dirname, "..", "..");
+
+module.exports = require("node-gyp-build")(root);
+
+try {
+  module.exports.nodeTypeInfo = require("../../src/node-types.json");
+} catch (_) {}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tests/test_binding.py b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tests/test_binding.py
new file mode 100644
index 0000000000..ab82006cd7
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tests/test_binding.py
@@ -0,0 +1,11 @@
+from unittest import TestCase
+
+import tree_sitter, tree_sitter_holscript
+
+
+class TestLanguage(TestCase):
+    def test_can_load_grammar(self):
+        try:
+            tree_sitter.Language(tree_sitter_holscript.language())
+        except Exception:
+            self.fail("Error loading Holscript grammar")
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/__init__.py b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/__init__.py
new file mode 100644
index 0000000000..7fda7dfb25
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/__init__.py
@@ -0,0 +1,42 @@
+"""HOLScript grammar for tree-sitter"""
+
+from importlib.resources import files as _files
+
+from ._binding import language
+
+
+def _get_query(name, file):
+    query = _files(f"{__package__}.queries") / file
+    globals()[name] = query.read_text()
+    return globals()[name]
+
+
+def __getattr__(name):
+    # NOTE: uncomment these to include any queries that this grammar contains:
+
+    # if name == "HIGHLIGHTS_QUERY":
+    #     return _get_query("HIGHLIGHTS_QUERY", "highlights.scm")
+    # if name == "INJECTIONS_QUERY":
+    #     return _get_query("INJECTIONS_QUERY", "injections.scm")
+    # if name == "LOCALS_QUERY":
+    #     return _get_query("LOCALS_QUERY", "locals.scm")
+    # if name == "TAGS_QUERY":
+    #     return _get_query("TAGS_QUERY", "tags.scm")
+
+    raise AttributeError(f"module {__name__!r} has no attribute {name!r}")
+
+
+__all__ = [
+    "language",
+    # "HIGHLIGHTS_QUERY",
+    # "INJECTIONS_QUERY",
+    # "LOCALS_QUERY",
+    # "TAGS_QUERY",
+]
+
+
+def __dir__():
+    return sorted(__all__ + [
+        "__all__", "__builtins__", "__cached__", "__doc__", "__file__",
+        "__loader__", "__name__", "__package__", "__path__", "__spec__",
+    ])
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/__init__.pyi b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/__init__.pyi
new file mode 100644
index 0000000000..abf6633f32
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/__init__.pyi
@@ -0,0 +1,10 @@
+from typing import Final
+
+# NOTE: uncomment these to include any queries that this grammar contains:
+
+# HIGHLIGHTS_QUERY: Final[str]
+# INJECTIONS_QUERY: Final[str]
+# LOCALS_QUERY: Final[str]
+# TAGS_QUERY: Final[str]
+
+def language() -> object: ...
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/binding.c b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/binding.c
new file mode 100644
index 0000000000..2f04d27fa3
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/binding.c
@@ -0,0 +1,27 @@
+#include <Python.h>
+
+typedef struct TSLanguage TSLanguage;
+
+TSLanguage *tree_sitter_holscript(void);
+
+static PyObject* _binding_language(PyObject *Py_UNUSED(self), PyObject *Py_UNUSED(args)) {
+    return PyCapsule_New(tree_sitter_holscript(), "tree_sitter.Language", NULL);
+}
+
+static PyMethodDef methods[] = {
+    {"language", _binding_language, METH_NOARGS,
+     "Get the tree-sitter language for this grammar."},
+    {NULL, NULL, 0, NULL}
+};
+
+static struct PyModuleDef module = {
+    .m_base = PyModuleDef_HEAD_INIT,
+    .m_name = "_binding",
+    .m_doc = NULL,
+    .m_size = -1,
+    .m_methods = methods
+};
+
+PyMODINIT_FUNC PyInit__binding(void) {
+    return PyModule_Create(&module);
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/py.typed b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/python/tree_sitter_holscript/py.typed
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/rust/build.rs b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/rust/build.rs
new file mode 100644
index 0000000000..6732794ae3
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/rust/build.rs
@@ -0,0 +1,22 @@
+fn main() {
+    let src_dir = std::path::Path::new("src");
+
+    let mut c_config = cc::Build::new();
+    c_config.std("c11").include(src_dir);
+
+    #[cfg(target_env = "msvc")]
+    c_config.flag("-utf-8");
+
+    let parser_path = src_dir.join("parser.c");
+    c_config.file(&parser_path);
+    println!("cargo:rerun-if-changed={}", parser_path.to_str().unwrap());
+
+    // NOTE: if your language uses an external scanner, uncomment this block:
+    /*
+    let scanner_path = src_dir.join("scanner.c");
+    c_config.file(&scanner_path);
+    println!("cargo:rerun-if-changed={}", scanner_path.to_str().unwrap());
+    */
+
+    c_config.compile("tree-sitter-holscript");
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/rust/lib.rs b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/rust/lib.rs
new file mode 100644
index 0000000000..16beee3ba1
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/rust/lib.rs
@@ -0,0 +1,53 @@
+//! This crate provides Holscript language support for the [tree-sitter][] parsing library.
+//!
+//! Typically, you will use the [LANGUAGE][] constant to add this language to a
+//! tree-sitter [Parser][], and then use the parser to parse some code:
+//!
+//! ```
+//! let code = r#"
+//! "#;
+//! let mut parser = tree_sitter::Parser::new();
+//! let language = tree_sitter_holscript::LANGUAGE;
+//! parser
+//!     .set_language(&language.into())
+//!     .expect("Error loading Holscript parser");
+//! let tree = parser.parse(code, None).unwrap();
+//! assert!(!tree.root_node().has_error());
+//! ```
+//!
+//! [Parser]: https://docs.rs/tree-sitter/*/tree_sitter/struct.Parser.html
+//! [tree-sitter]: https://tree-sitter.github.io/
+
+use tree_sitter_language::LanguageFn;
+
+extern "C" {
+    fn tree_sitter_holscript() -> *const ();
+}
+
+/// The tree-sitter [`LanguageFn`][LanguageFn] for this grammar.
+///
+/// [LanguageFn]: https://docs.rs/tree-sitter-language/*/tree_sitter_language/struct.LanguageFn.html
+pub const LANGUAGE: LanguageFn = unsafe { LanguageFn::from_raw(tree_sitter_holscript) };
+
+/// The content of the [`node-types.json`][] file for this grammar.
+///
+/// [`node-types.json`]: https://tree-sitter.github.io/tree-sitter/using-parsers#static-node-types
+pub const NODE_TYPES: &str = include_str!("../../src/node-types.json");
+
+// NOTE: uncomment these to include any queries that this grammar contains:
+
+// pub const HIGHLIGHTS_QUERY: &str = include_str!("../../queries/highlights.scm");
+// pub const INJECTIONS_QUERY: &str = include_str!("../../queries/injections.scm");
+// pub const LOCALS_QUERY: &str = include_str!("../../queries/locals.scm");
+// pub const TAGS_QUERY: &str = include_str!("../../queries/tags.scm");
+
+#[cfg(test)]
+mod tests {
+    #[test]
+    fn test_can_load_grammar() {
+        let mut parser = tree_sitter::Parser::new();
+        parser
+            .set_language(&super::LANGUAGE.into())
+            .expect("Error loading Holscript parser");
+    }
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/swift/TreeSitterHolscript/holscript.h b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/swift/TreeSitterHolscript/holscript.h
new file mode 100644
index 0000000000..8d1c60acd1
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/swift/TreeSitterHolscript/holscript.h
@@ -0,0 +1,16 @@
+#ifndef TREE_SITTER_HOLSCRIPT_H_
+#define TREE_SITTER_HOLSCRIPT_H_
+
+typedef struct TSLanguage TSLanguage;
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+const TSLanguage *tree_sitter_holscript(void);
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // TREE_SITTER_HOLSCRIPT_H_
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/swift/TreeSitterHolscriptTests/TreeSitterHolscriptTests.swift b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/swift/TreeSitterHolscriptTests/TreeSitterHolscriptTests.swift
new file mode 100644
index 0000000000..a1991074f1
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/bindings/swift/TreeSitterHolscriptTests/TreeSitterHolscriptTests.swift
@@ -0,0 +1,12 @@
+import XCTest
+import SwiftTreeSitter
+import TreeSitterHolscript
+
+final class TreeSitterHolscriptTests: XCTestCase {
+    func testCanLoadGrammar() throws {
+        let parser = Parser()
+        let language = Language(language: tree_sitter_holscript())
+        XCTAssertNoThrow(try parser.setLanguage(language),
+                         "Error loading Holscript grammar")
+    }
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/go.mod b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/go.mod
new file mode 100644
index 0000000000..bb11aeb251
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/go.mod
@@ -0,0 +1,5 @@
+module github.com/hol-theorem-prover/hol/
+
+go 1.22
+
+require github.com/tree-sitter/go-tree-sitter v0.23.1
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/grammar.js b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/grammar.js
new file mode 100644
index 0000000000..145aef8110
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/grammar.js
@@ -0,0 +1,1280 @@
+/**
+ * @file HOLScript grammar for tree-sitter
+ * @author Daniel Nezamabadi
+ * @license MIT
+ */
+
+// Adapted tree-sitter-sml by Matthew Fluet, released under the MIT license.
+
+/* eslint-disable require-jsdoc */
+
+/// <reference types="tree-sitter-cli/dsl" />
+// @ts-check
+
+// ******************************************************** //
+// Extensions
+// ******************************************************** //
+
+const EXTENSIONS = true;
+
+function ifExtElse(ext, resExt, resStd) {
+    if (Array.isArray(EXTENSIONS) ?
+        (Array.isArray(ext) ?
+         ext.some((ext) => EXTENSIONS.includes(ext)) :
+         EXTENSIONS.includes(ext)) :
+        EXTENSIONS) {
+        return resExt;
+    } else {
+        return resStd;
+    }
+}
+
+function ifExtAlt(ext, resExt) {
+    return ifExtElse(ext, resExt, choice());
+}
+function ifExtOpt(ext, resExt) {
+    return ifExtElse(ext, optional(resExt), blank());
+}
+
+const optBar = ifExtOpt('optBar', '|');
+
+// ******************************************************** //
+// Regular Expressions for Constants
+// ******************************************************** //
+
+const decDigitRE = '[0-9]';
+const decNumRE = ifExtElse(
+    'extendedNumConst',
+    `${decDigitRE}(?:_*${decDigitRE})*`,
+    `${decDigitRE}+`,
+);
+const hexDigitRE = '[A-Fa-f0-9]';
+const hexNumRE = ifExtElse(
+    'extendedNumConst',
+    `${hexDigitRE}(?:_*${hexDigitRE})*`,
+    `${hexDigitRE}+`,
+);
+const binDigitRE = '[01]';
+const binNumRE = ifExtElse(
+    'extendedNumConst',
+    `${binDigitRE}(?:_*${binDigitRE})*`,
+    `${binDigitRE}+`,
+);
+const integerConstRE = ifExtElse(
+    'extendedNumConst',
+    `~?${decNumRE}|~?0x${hexNumRE}|~?0b${binNumRE}`,
+    `~?${decNumRE}|~?0x${hexNumRE}`,
+);
+const wordConstRE = ifExtElse(
+    'extendedNumConst',
+    `0w${decNumRE}|0wx${hexNumRE}|0wb${binNumRE}`,
+    `0w${decNumRE}|0wx${hexNumRE}`,
+);
+const fracRE = `[.]${decNumRE}`;
+const expRE = `[eE]~?${decNumRE}`;
+const realConstRE = `~?${decNumRE}${fracRE}(?:${expRE})?|~?${decNumRE}(?:${fracRE})?${expRE}`;
+
+const stringConstRE = '"(?:[^"\\\\]|\\\\[^\\s]|\\\\\\s*\\\\)*"';
+const charConstRE = '#"(?:[^"\\\\]|\\\\[^\\s]|\\\\\\s*\\\\)*"';
+
+// ******************************************************** //
+// Regular Expressions Identifiers
+// ******************************************************** //
+
+const alphaNumericIdentSuffixRE = /[A-Za-z0-9_']*/.source;
+const alphaAlphaNumericIdentRE = `[A-Za-z]${alphaNumericIdentSuffixRE}`;
+const primeAlphaNumericIdentRE = `'${alphaNumericIdentSuffixRE}`;
+const symbolicIdentRE = /[!%&$#+\-/:<=>?@\\~`^|*]+/.source;
+
+// ******************************************************** //
+// "Separated By"
+// ******************************************************** //
+
+const commaSep = {name: 'Comma', token: ','};
+const semicolonSep = {name: 'Semicolon', token: ';'};
+
+function mkSepByAux(cnt, pre, sep, elt, pst) {
+    if (cnt > 0) {
+        return seq(
+            pre ? sep : blank(),
+            elt,
+            mkSepByAux(cnt - 1, true, sep, elt, pst),
+        );
+    } else {
+        if (pre) {
+            if (pst) {
+                return seq(repeat(seq(sep, elt)), pst(true));
+            } else {
+                return repeat(seq(sep, elt));
+            }
+        } else {
+            if (pst) {
+                return choice(pst(false), seq(elt, repeat(seq(sep, elt)), pst(true)));
+            } else {
+                return optional(seq(elt, repeat(seq(sep, elt))));
+            }
+        }
+    }
+}
+
+function mkSepByCntFstLst(sep, elt, cnt, fst, lst) {
+    let optSep = false; let empSep = false;
+    let preSep; let pstSep;
+    if (typeof sep === 'string') {
+        preSep = blank();
+        pstSep = blank();
+    } else {
+        if (ifExtElse('emp'.concat(sep.name), true, false)) {
+            empSep = true;
+            optSep = true;
+        } else if (ifExtElse('opt'.concat(sep.name), true, false)) {
+            optSep = true;
+        }
+        sep = sep.token;
+        if (empSep) {
+            sep = repeat1(sep);
+        }
+        if (optSep) {
+            preSep = optional(sep);
+            pstSep = optional(sep);
+        } else {
+            preSep = blank();
+            pstSep = blank();
+        }
+    }
+
+    let pst;
+    if (lst) {
+        pst = (pre) => {
+            if (lst.rqd) {
+                if (pre) {
+                    return seq(sep, lst.elt, pstSep);
+                } else {
+                    return seq(lst.elt, pstSep);
+                }
+            } else {
+                if (pre) {
+                    return seq(optional(seq(sep, lst.elt)), pstSep);
+                } else {
+                    return optional(seq(lst.elt, pstSep));
+                }
+            }
+        };
+    } else if (optSep) {
+        pst = (pre) => {
+            if (pre) {
+                return pstSep;
+            } else {
+                return blank();
+            }
+        };
+    } else {
+        pst = false;
+    };
+
+    if (fst) {
+        if (fst.rqd) {
+            return seq(preSep, fst.elt, mkSepByAux(cnt, true, sep, elt, pst));
+        } else {
+            return choice(
+                seq(preSep, fst.elt, mkSepByAux(cnt, true, sep, elt, pst)),
+                seq(preSep, mkSepByAux(cnt, false, sep, elt, pst)),
+            );
+        }
+    } else {
+        return seq(preSep, mkSepByAux(cnt, false, sep, elt, pst));
+    };
+}
+
+// function mkSepByCnt(sep, elt, cnt) {
+//   return mkSepByCntFstLst(sep, elt, cnt, false, false);
+// }
+
+function mkSepBy(sep, elt, cnt) {
+    return mkSepByCntFstLst(sep, elt, 0, false, false);
+}
+
+function mkSepBy1(sep, elt, cnt) {
+    return mkSepByCntFstLst(sep, elt, 1, false, false);
+}
+
+function mkSepBy2(sep, elt, cnt) {
+    return mkSepByCntFstLst(sep, elt, 2, false, false);
+}
+
+function mkBrakSepByCntFstLst(opn, sep, elt, cnt, fst, lst, cls) {
+    return seq(opn, mkSepByCntFstLst(sep, elt, cnt, fst, lst), cls);
+}
+
+function mkBrakSepBy(opn, sep, elt, cls) {
+    return seq(opn, mkSepBy(sep, elt), cls);
+}
+
+function mkBrakSepBy1(opn, sep, elt, cls) {
+    return seq(opn, mkSepBy1(sep, elt), cls);
+}
+
+function mkSeqAux(clsSing, clsSep) {
+    return choice(clsSing, mkBrakSepBy1('(', ',', clsSep, ')'));
+}
+
+function mkSeq(cls) {
+    return mkSeqAux(cls, cls);
+}
+
+// ******************************************************** //
+// Grammar
+// ******************************************************** //
+
+module.exports = grammar({
+    name: 'holscript',
+
+    extras: $ => [
+        /\s+/,
+        $.block_comment,
+        ...ifExtElse('lineComment', [$.line_comment], []),
+    ],
+
+    externals: $ => [
+        $.block_comment,
+        $.line_comment,
+    ],
+
+    supertypes: $ => [
+        $._scon,
+        $._exp,
+        $._dec,
+        $._pat,
+        $._ty,
+        $._strexp,
+        $._strdec,
+        $._sigexp,
+        $._sigdec,
+        $._spec,
+        $._fctdec,
+        $._topdec,
+    ],
+
+    inline: $ => [
+    ],
+
+    conflicts: $ => [
+        [
+            // Two tokens of lookahead required.
+            $.wheretype_sigexp,
+        ],
+        // HOL
+        [$.hol_pcons, $.hol_ptuple]
+    ],
+
+    // HACK Causes problem when we add HOL things
+    // word: $ => $._alphaAlphaNumeric_ident,
+
+    rules: {
+        source_file: $ => optional($._program),
+
+        comment: $ => choice(
+            $.block_comment,
+            ifExtAlt('lineComment', $.line_comment),
+        ),
+
+        // ******************************************************** //
+        // Special Constants
+        // ******************************************************** //
+
+        _scon: $ => choice(
+            $.integer_scon,
+            $.word_scon,
+            $.real_scon,
+            $.string_scon,
+            $.char_scon,
+        ),
+
+        integer_scon: $ => new RegExp(integerConstRE),
+        word_scon: $ => new RegExp(wordConstRE),
+        real_scon: $ => new RegExp(realConstRE),
+        string_scon: $ => new RegExp(stringConstRE),
+        char_scon: $ => new RegExp(charConstRE),
+
+        // ******************************************************** //
+        // Identifier Classes (Core)
+        // ******************************************************** //
+
+        _alphaAlphaNumeric_ident: $ => new RegExp(alphaAlphaNumericIdentRE),
+        _primeAlphaNumeric_ident: $ => new RegExp(primeAlphaNumericIdentRE),
+        _symbolic_ident: $ => new RegExp(symbolicIdentRE),
+
+        tyvar: $ => choice($._primeAlphaNumeric_ident),
+        tyvarseq: $ => mkSeq($.tyvar),
+        vid: $ => choice($._alphaAlphaNumeric_ident, $._symbolic_ident),
+        longvid: $ => seq(repeat(seq($.strid, '.')), $.vid),
+        tycon: $ => choice($._alphaAlphaNumeric_ident, $._symbolic_ident),
+        longtycon: $ => seq(repeat(seq($.strid, '.')), $.tycon),
+        lab: $ => choice($._alphaAlphaNumeric_ident, $._symbolic_ident, /[1-9][0-9]*/),
+
+        // ******************************************************** //
+        // Expressions and Matches (Core)
+        // ******************************************************** //
+
+        _atexp: $ => choice(
+            $.scon_exp,
+            $.vid_exp,
+            $.record_exp,
+            $.recordsel_exp,
+            $.unit_exp,
+            $.tuple_exp,
+            $.list_exp,
+            ifExtAlt('vectorExp', $.vec_exp),
+            $.sequence_exp,
+            $.let_exp,
+            $.paren_exp,
+            // HOL
+            $.quoted_term,
+            $.quoted_type,
+            $.backquote
+        ),
+
+        scon_exp: $ => $._scon,
+        vid_exp: $ => seq(optional('op'), $.longvid),
+        record_exp: $ => mkBrakSepByCntFstLst(
+            '{',
+            commaSep,
+            $._exprow, 0,
+            false,
+            ifExtElse('recordExt', {elt: $.ellipsis_exprow, rqd: false}, false),
+            '}',
+        ),
+        _exprow: $ => choice(
+            $.exprow,
+            ifExtAlt('recordExpPun', $.labvar_exprow),
+        ),
+        exprow: $ => seq($.lab, '=', $._exp),
+        labvar_exprow: $ => seq($.vid, optional(seq(':', $._ty))),
+        ellipsis_exprow: $ => seq('...', '=', $._exp),
+        recordsel_exp: $ => seq('#', $.lab),
+        unit_exp: $ => prec(1, seq('(', ')')),
+        tuple_exp: $ => mkBrakSepBy('(', commaSep, $._exp, ')'),
+        list_exp: $ => mkBrakSepByCntFstLst(
+            '[',
+            commaSep,
+            $._exp, 0,
+            false,
+            ifExtElse('listEllipsis', {elt: $.ellipsis_listexp, rqd: false}, false),
+            ']',
+        ),
+        ellipsis_listexp: $ => seq('...', '=', $._exp),
+        vec_exp: $ => mkBrakSepBy('#[', commaSep, $._exp, ']'),
+        sequence_exp: $ => mkBrakSepBy('(', semicolonSep, $._exp, ')'),
+        let_exp: $ => seq(
+            'let',
+            repeat(choice(';', field('dec', $._dec))),
+            'in',
+            mkSepBy1(semicolonSep, field('body', $._exp)),
+            'end',
+        ),
+        paren_exp: $ => prec(1, seq('(', $._exp, ')')),
+
+        // The Definition orders by decreasing precedence
+        _exp: $ => choice(
+            $._atexp,
+            $.app_exp,
+            $.typed_exp,
+            $.conj_exp,
+            $.disj_exp,
+            $.handle_exp,
+            $.raise_exp,
+            $.cond_exp,
+            $.iter_exp,
+            $.case_exp,
+            $.fn_exp,
+        ),
+
+        app_exp: $ => prec(10, seq($._atexp, repeat1($._atexp))),
+        typed_exp: $ => prec(9, seq($._exp, ':', $._ty)),
+        conj_exp: $ => prec.left(8, seq($._exp, 'andalso', $._exp)),
+        disj_exp: $ => prec.left(7, seq($._exp, 'orelse', $._exp)),
+        handle_exp: $ => prec(6, seq($._exp, 'handle', $._match)),
+        raise_exp: $ => prec(5, seq('raise', $._exp)),
+        cond_exp: $ => prec.right(4, seq(
+            'if', field('if_exp', $._exp),
+            'then', field('then_exp', $._exp),
+            ifExtElse('optElse',
+                      optional(seq('else', field('else_exp', $._exp))),
+                      seq('else', field('else_exp', $._exp))),
+        )),
+        iter_exp: $ => prec(3, seq('while', field('while_exp', $._exp), 'do', field('do_exp', $._exp))),
+        case_exp: $ => prec(2, seq('case', $._exp, 'of', $._match)),
+        fn_exp: $ => prec(1, seq('fn', $._match)),
+
+        _match: $ => prec.right(seq(optBar, mkSepBy1('|', $.mrule))),
+        mrule: $ => seq($._pat, '=>', $._exp),
+
+        // ******************************************************** //
+        // Declarations and Bindings (Core)
+        // ******************************************************** //
+
+        _dec: $ => choice(
+            $._dec_no_local,
+            $.local_dec,
+        ),
+        _dec_no_local: $ => choice(
+            ifExtAlt('doDec', $.do_dec),
+            $.val_dec,
+            $.fun_dec,
+            $.type_dec,
+            $.datatype_dec,
+            $.datarepl_dec,
+            $.abstype_dec,
+            $.exception_dec,
+            // $.local_dec,
+            $.open_dec,
+            $.infix_dec,
+            $.infixr_dec,
+            $.nonfix_dec,
+        ),
+
+        do_dec: $ => seq('do', $._exp),
+
+        val_dec: $ => seq(
+            'val',
+            optional('rec'),
+            optional($.tyvarseq),
+            $._valbind,
+        ),
+        _valbind: $ => mkSepBy1('and', $.valbind),
+        valbind: $ => seq(field('pat', $._pat), '=', field('def', $._exp)),
+
+        fun_dec: $ => seq(
+            'fun',
+            optional($.tyvarseq),
+            $._fvalbind,
+        ),
+        _fvalbind: $ => mkSepBy1('and', $.fvalbind),
+        fvalbind: $ => $._fmatch,
+        _fmatch: $ => seq(optBar, mkSepBy1('|', $.fmrule)),
+        fmrule: $ => seq(
+            choice(
+                prec(2, seq(optional('op'), field('name', $.vid), repeat1(field('arg', $._atpat)))),
+                prec(2, seq('(', field('argl', $._atpat), field('name', $.vid), field('argr', $._atpat), ')', repeat(field('arg', $._atpat)))),
+                prec(0, seq(field('argl', $._atpat), field('name', $.vid), field('argr', $._atpat))),
+            ),
+            optional(seq(':', field('ty', $._ty))),
+            '=',
+            field('def', $._exp),
+        ),
+
+        type_dec: $ => seq('type', $._typbind),
+        _typbind: $ => mkSepBy1('and', $.typbind),
+        typbind: $ => seq(
+            optional($.tyvarseq),
+            field('name', $.tycon),
+            '=',
+            field('def', $._ty),
+        ),
+
+        datatype_dec: $ => seq(
+            'datatype',
+            $._datbind,
+            optional(seq('withtype', field('withtype', $._typbind))),
+        ),
+        _datbind: $ => mkSepBy1('and', $.datbind),
+        datbind: $ => seq(
+            optional($.tyvarseq),
+            field('name', $.tycon),
+            '=',
+            field('def', $._conbind),
+        ),
+        _conbind: $ => seq(optBar, mkSepBy1('|', $.conbind)),
+        conbind: $ => seq(
+            seq(optional('op'), field('name', $.vid)),
+            optional(seq('of', field('ty', $._ty))),
+        ),
+
+        datarepl_dec: $ => seq(
+            'datatype',
+            field('name', $.tycon),
+            '=',
+            'datatype',
+            field('def', $.longtycon),
+        ),
+
+        abstype_dec: $ => seq(
+            'abstype',
+            $._datbind,
+            optional(seq('withtype', field('withtype', $._typbind))),
+            'with',
+            repeat(choice(';', field('dec', $._dec))),
+            'end',
+        ),
+
+        exception_dec: $ => seq('exception', $._exbind),
+        _exbind: $ => mkSepBy1('and', $.exbind),
+        exbind: $ => choice(
+            seq(
+                seq(optional('op'), field('name', $.vid)),
+                optional(seq('of', field('ty', $._ty))),
+            ),
+            seq(
+                seq(optional('op'), field('name', $.vid)),
+                '=',
+                seq(optional('op'), field('def', $.longvid)),
+            ),
+        ),
+
+        local_dec: $ => seq(
+            'local',
+            repeat(choice(';', field('dec', $._dec))),
+            'in',
+            repeat(choice(';', field('body', $._dec))),
+            'end',
+        ),
+
+        open_dec: $ => seq('open', repeat1($.longstrid)),
+
+        infix_dec: $ => seq('infix', optional(/[0-9]/), repeat1($.vid)),
+        infixr_dec: $ => seq('infixr', optional(/[0-9]/), repeat1($.vid)),
+        nonfix_dec: $ => seq('nonfix', repeat1($.vid)),
+
+        // ******************************************************** //
+        // Patterns (Core)
+        // ******************************************************** //
+
+        _atpat: $ => choice(
+            $.wildcard_pat,
+            $.scon_pat,
+            $.vid_pat,
+            $.record_pat,
+            $.unit_pat,
+            $.tuple_pat,
+            $.list_pat,
+            ifExtAlt('vectorPat', $.vec_pat),
+            $.paren_pat,
+        ),
+
+        wildcard_pat: $ => '_',
+        scon_pat: $ => $._scon,
+        vid_pat: $ => seq(optional('op'), $.longvid),
+        record_pat: $ => mkBrakSepByCntFstLst(
+            '{',
+            commaSep,
+            $._patrow, 0,
+            false,
+            {elt: $.ellipsis_patrow, rqd: false},
+            '}',
+        ),
+        _patrow: $ => choice($.patrow, $.labvar_patrow),
+        patrow: $ => seq($.lab, '=', $._pat),
+        labvar_patrow: $ => seq(
+            $.vid,
+            optional(seq(':', $._ty)),
+            optional(seq('as', $._pat)),
+        ),
+        ellipsis_patrow: $ => seq('...', ifExtOpt('recordExt', seq('=', $._pat))),
+        unit_pat: $ => prec(1, seq('(', ')')),
+        tuple_pat: $ => mkBrakSepBy('(', commaSep, $._pat, ')'),
+        list_pat: $ => mkBrakSepByCntFstLst(
+            '[',
+            commaSep,
+            $._pat, 0,
+            false,
+            ifExtElse('listEllipsis', {elt: $.ellipsis_listpat, rqd: false}, false),
+            ']'),
+        ellipsis_listpat: $ => seq('...', '=', $._pat),
+        vec_pat: $ => mkBrakSepBy('#[', commaSep, $._pat, ')'),
+        paren_pat: $ => prec(1, seq('(', $._pat, ')')),
+
+        // The Definition orders by decreasing precedence
+        _pat: $ => choice(
+            $._atpat,
+            $.app_pat,
+            $.typed_pat,
+            ifExtElse('conjPat', $.conj_pat, $.as_pat),
+            ifExtAlt(['orPat', 'disjPat'], $.disj_pat),
+        ),
+
+        app_pat: $ => prec(4, seq($._atpat, repeat1($._atpat))),
+        typed_pat: $ => prec(3, seq($._pat, ':', $._ty)),
+        as_pat: $ => prec.right(2, seq(optional('op'), $.vid, optional(seq(':', $._ty)), 'as', $._pat)),
+        conj_pat: $ => prec.right(2, seq($._pat, 'as', $._pat)),
+        disj_pat: $ => prec.left(1, seq($._pat, '|', $._pat)),
+
+        // ******************************************************** //
+        // Type expressions (Core)
+        // ******************************************************** //
+
+        _ty: $ => $._fn_ty,
+        tyseq: $ => mkSeqAux($._atty, $._ty),
+
+        _fn_ty: $ => choice($.fn_ty, $._tuple_ty),
+        fn_ty: $ => seq($._tuple_ty, '->', $._fn_ty),
+
+        _tuple_ty: $ => choice($.tuple_ty, $._paren_ty),
+        tuple_ty: $ => mkSepBy2('*', $._paren_ty),
+
+        _paren_ty: $ => choice($.paren_ty, $._atty),
+        paren_ty: $ => seq('(', $._ty, ')'),
+
+        _atty: $ => choice(
+            $.tyvar_ty,
+            $.record_ty,
+            $.tycon_ty,
+        ),
+
+        tyvar_ty: $ => $.tyvar,
+        record_ty: $ => mkBrakSepByCntFstLst(
+            '{',
+            commaSep,
+            $.tyrow, 0,
+            false,
+            ifExtElse('recordExt', {elt: $.ellipsis_tyrow, rqd: false}, false),
+            '}',
+        ),
+        tyrow: $ => seq($.lab, ':', $._ty),
+        ellipsis_tyrow: $ => seq('...', ':', $._ty),
+        tycon_ty: $ => seq(
+            optional($.tyseq),
+            $.longtycon,
+        ),
+
+        // ******************************************************** //
+        // Identifier Classes (Modules)
+        // ******************************************************** //
+
+        strid: $ => choice($._alphaAlphaNumeric_ident),
+        longstrid: $ => seq(repeat(seq($.strid, '.')), $.strid),
+        sigid: $ => choice($._alphaAlphaNumeric_ident),
+        fctid: $ => choice($._alphaAlphaNumeric_ident),
+
+        // ******************************************************** //
+        // Structure Expressions (Modules)
+        // ******************************************************** //
+
+        _strexp: $ => choice(
+            $.struct_strexp,
+            $.strid_strexp,
+            $.constr_strexp,
+            $.fctapp_strexp,
+            $.let_strexp,
+        ),
+
+        struct_strexp: $ => seq(
+            'struct',
+            repeat(choice(';', field('strdec', $._strdec))),
+            'end',
+        ),
+        strid_strexp: $ => $.longstrid,
+        constr_strexp: $ => seq($._strexp, choice(':', ':>'), $._sigexp),
+        fctapp_strexp: $ => seq(
+            field('name', $.fctid),
+            '(',
+            field('arg',
+                  choice(
+                      $._strexp,
+                      repeat(choice(';', $._strdec)),
+                  ),
+                 ),
+            ')',
+        ),
+        let_strexp: $ => seq(
+            'let',
+            repeat(choice(';', field('dec', $._strdec))),
+            'in',
+            field('body', $._strexp),
+            'end',
+        ),
+
+        _strdec: $ => choice(
+            $._dec_no_local,
+            $.structure_strdec,
+            $.local_strdec,
+        ),
+
+        structure_strdec: $ => seq('structure', $._strbind),
+        _strbind: $ => mkSepBy1('and', $.strbind),
+        strbind: $ => seq(
+            field('name', $.strid),
+            optional(seq(choice(':', ':>'), field('sig', $._sigexp))),
+            '=',
+            field('def', $._strexp),
+        ),
+
+        local_strdec: $ => seq(
+            'local',
+            repeat(choice(';', field('dec', $._strdec))),
+            'in',
+            repeat(choice(';', field('body', $._strdec))),
+            'end',
+        ),
+
+        // ******************************************************** //
+        // Signature Expressions (Modules)
+        // ******************************************************** //
+
+        _sigexp: $ => choice(
+            $.sig_sigexp,
+            $.sigid_sigexp,
+            $.wheretype_sigexp,
+        ),
+
+        sig_sigexp: $ => seq(
+            'sig',
+            repeat(choice(';', field('spec', $._spec))),
+            'end',
+        ),
+        sigid_sigexp: $ => $.sigid,
+        wheretype_sigexp: $ => seq(
+            $._sigexp,
+            'where',
+            mkSepBy1('and', seq(
+                'type',
+                optional($.tyvarseq),
+                $.longtycon,
+                '=',
+                $._ty,
+            )),
+        ),
+
+        _sigdec: $ => choice(
+            $.signature_sigdec,
+        ),
+        signature_sigdec: $ => seq('signature', $._sigbind),
+        _sigbind: $ => mkSepBy1('and', $.sigbind),
+        sigbind: $ => seq(
+            field('name', $.sigid),
+            '=',
+            field('def', $._sigexp),
+        ),
+
+        // ******************************************************** //
+        // Specifications (Modules)
+        // ******************************************************** //
+
+        _spec: $ => choice(
+            $.val_spec,
+            $.type_spec,
+            $.eqtype_spec,
+            $.datatype_spec,
+            $.datarepl_spec,
+            $.exception_spec,
+            $.structure_spec,
+            $.include_spec,
+            $.sharingtype_spec,
+            $.sharing_spec,
+        ),
+
+        val_spec: $ => seq('val', $._valdesc),
+        _valdesc: $ => mkSepBy1('and', $.valdesc),
+        valdesc: $ => seq(field('name', $.vid), ':', field('ty', $._ty)),
+
+        type_spec: $ => seq('type', choice($._typedesc, $._typbind)),
+        _typedesc: $ => mkSepBy1('and', $.typedesc),
+        typedesc: $ => seq(
+            optional($.tyvarseq),
+            field('name', $.tycon),
+        ),
+
+        eqtype_spec: $ => seq('eqtype', $._typedesc),
+
+        datatype_spec: $ => seq(
+            'datatype',
+            $._datdesc,
+            ifExtOpt('sigWithtype', seq('withtype', field('withtype', $._typbind))),
+        ),
+        _datdesc: $ => mkSepBy1('and', $.datdesc),
+        datdesc: $ => seq(
+            optional($.tyvarseq),
+            field('name', $.tycon),
+            '=',
+            field('def', $._condesc),
+        ),
+        _condesc: $ => seq(optBar, mkSepBy1('|', $.condesc)),
+        condesc: $ => seq(
+            field('name', $.vid),
+            optional(seq('of', field('ty', $._ty))),
+        ),
+
+        datarepl_spec: $ => seq(
+            'datatype',
+            field('name', $.tycon),
+            '=',
+            'datatype',
+            field('def', $.longtycon),
+        ),
+
+        exception_spec: $ => seq('exception', $._exdesc),
+        _exdesc: $ => mkSepBy1('and', $.exdesc),
+        exdesc: $ => seq(
+            field('name', $.vid),
+            optional(seq('of', field('ty', $._ty))),
+        ),
+
+        structure_spec: $ => seq('structure', $._strdesc),
+        _strdesc: $ => mkSepBy1('and', $.strdesc),
+        strdesc: $ => seq(field('name', $.strid), ':', field('sig', $._sigexp)),
+
+        include_spec: $ => seq('include', choice($._sigexp, seq($.sigid, repeat1($.sigid)))),
+
+        sharingtype_spec: $ => seq('sharing', 'type', mkSepBy2('=', $.longtycon)),
+
+        sharing_spec: $ => seq('sharing', mkSepBy2('=', $.longstrid)),
+
+        // ******************************************************** //
+        // Functors (Modules)
+        // ******************************************************** //
+
+        _fctdec: $ => choice(
+            $.functor_fctdec,
+        ),
+        functor_fctdec: $ => seq('functor', $._fctbind),
+        _fctbind: $ => mkSepBy1('and', $.fctbind),
+        fctbind: $ => seq(
+            field('name', $.fctid),
+            '(',
+            field('arg',
+                  choice(
+                      seq($.strid, ':', $._sigexp),
+                      repeat(choice(';', $._spec)),
+                  ),
+                 ),
+            ')',
+            optional(seq(choice(':', ':>'), field('sig', $._sigexp))),
+            '=',
+            field('def', $._strexp),
+        ),
+
+        // ******************************************************** //
+        // Topdecs
+        // ******************************************************** //
+
+        _topdec: $ => choice(
+            $._strdec,
+            $._sigdec,
+            $._fctdec,
+            // HOL
+            $.hol_definition,
+            $.hol_definition_with_proof,
+            $.hol_datatype,
+            $.hol_theorem_with_proof
+        ),
+
+        // ******************************************************** //
+        // Programs
+        // ******************************************************** //
+
+        _program: $ => seq(
+            choice(repeat1($._topdec), $._exp),
+            optional(seq(';', optional($._program))),
+        ),
+
+
+        // ******************************************************** //
+        // HOL
+        // ******************************************************** //
+        antiquoted: $ => choice(
+            seq('^', '(', $._exp, ')'),
+            seq('^', alias($._alphaAlphaNumeric_ident, $.sml_variable))
+        ),
+
+        quoted_term: $ => seq('“', $._hol_term, '”'),
+
+        quoted_type: $ => seq('“', ':', $._hol_type, '”'),
+
+        _quote_content: $ => choice(
+            alias(/([^\^`‘’]|\^\^|\^\`)+/, $.quoted),
+            $.antiquoted
+        ),
+
+        backquote: $ => choice(
+            seq('‘', repeat($._quote_content), '’'),
+            seq('`', repeat($._quote_content), '`'),
+        ),
+
+        hol_attributes: $ => seq(
+            '[',
+            mkSepBy1(',', alias($._alphaAlphaNumeric_ident, $.attribute)),
+            ']'
+        ),
+
+        hol_definition: $ => seq(
+            'Definition',
+            alias($._alphaAlphaNumeric_ident, $.hol_defname),
+            optional($.hol_attributes),
+            ':',
+            $.hol_fn_spec,
+            'End'
+        ),
+
+        hol_definition_with_proof: $ => seq(
+            'Definition',
+            alias($._alphaAlphaNumeric_ident, $.hol_defname),
+            optional($.hol_attributes),
+            ':',
+            $.hol_fn_spec,
+            'Termination',
+            $.tactic,
+            'End'
+        ),
+
+        hol_datatype: $ => seq(
+            'Datatype:',
+            $.hol_binding,
+            'End'
+        ),
+
+        hol_theorem_with_proof: $ => seq(
+            'Theorem',
+            alias($._alphaAlphaNumeric_ident, $.hol_thmname),
+            optional($.hol_attributes),
+            ':',
+            alias($._hol_term, $.hol_thmstmt),
+            'Proof',
+            $.tactic,
+            'QED'
+        ),
+
+        // TODO Unsure about this (in particular THEN)
+        _atomic_tactic: $ => choice(
+            $._exp,
+            seq('(', $.THEN, ')')
+        ),
+
+        tactic: $ => choice(
+            $._atomic_tactic,
+            $.THEN
+        ),
+
+        THEN: $ => prec.left(mkSepBy2('\\\\', $._atomic_tactic)),
+
+        hol_binding: $ => seq(
+            $.hol_identifier,
+            '=',
+            $.hol_constructor
+        ),
+
+        hol_constructor: $ => mkSepBy1('|', $.hol_clause),
+
+        hol_clause: $ => seq(
+            $.hol_identifier,
+            repeat($._hol_ty_spec)
+        ),
+
+        _hol_ty_spec: $ => choice(
+            $.hol_atomic_type,
+            seq('(', $._hol_type ,')')
+        ),
+
+        hol_fn_spec: $ => choice(
+            mkSepBy1('∧', choice($.hol_eqn, seq('(', $.hol_eqn, ')'))),
+            mkSepBy1('\/\\', choice($.hol_eqn, seq('(', $.hol_eqn, ')')))
+        ),
+
+        // TODO Sort out precedence levels properly
+        // NOTE hol_eqn has higher precedence to avoid conjunction being
+        //   "consumed" by the term
+        hol_eqn: $ => prec(450, seq(
+            $.hol_identifier,
+            repeat($.hol_pat),
+            '=',
+            alias($._hol_term, $.hol_term))),
+
+        hol_pat: $ => choice(
+            $._hol_pat,
+            seq('(',
+                $._hol_pat,
+                ':',
+                alias($._hol_ty_spec, $.hol_pannotation),
+                ')'
+               )
+        ),
+
+        _hol_pat: $ => choice(
+            $.hol_variable,
+            $.hol_wildcard,
+            $._hol_literal,
+            $.hol_cname_alphanumeric,
+            $.hol_pcons,
+            $.hol_ptuple,
+            $.hol_plist,
+            seq('(', $.hol_cname_alphanumeric, repeat1($.hol_pat), ')')
+        ),
+
+        hol_pcons: $ => seq('(', mkSepBy1('::', $.hol_pat), ')'),
+
+        hol_ptuple: $ => seq('(', mkSepBy1(',', $.hol_pat), ')'),
+
+        hol_plist: $ => seq(
+            '[',
+            mkSepBy(';', $.hol_pat),
+            ']'
+        ),
+
+        hol_identifier: $ => choice(
+            $._hol_alphanumeric,
+            $._hol_symbolic
+        ),
+
+        hol_wildcard: $ => '_',
+
+        // TODO Missing unicode subscript and superscript
+        // TODO Make this more readable?
+        _hol_alphanumeric: $ => /[a-zA-Z\u0370-\u03BA\u03BC-\u03FF][a-zA-Z\u0370-\u03BA\u03BC-\u03FF0-9\'_]*/,
+
+        _hol_symbolic: $ => token(
+            choice(
+                // TODO Add support for ^ and `
+                repeat1(choice('#', '?', '+', '*', '/', '\\', '=', '<', '>',
+                               '&', '%', '@', '!', ':', '|', '-')),
+                repeat1('$')
+            )
+        ),
+
+        // HACK trying to disambiguate variables and constructors
+        // start with uppercase letter
+        // TODO Maybe just get rid of this and hol_variable
+        hol_cname_alphanumeric: $ => /[A-Z][a-zA-Z\u0370-\u03BA\u03BC-\u03FF0-9\'_]*/,
+
+        // start with lowercase letter
+        hol_variable: $ => /[a-z][a-zA-Z\u0370-\u03BA\u03BC-\u03FF0-9\'_]*/,
+
+        _hol_term: $ => choice(
+            $._hol_literal,
+            $.hol_tuple,
+            $.hol_list,
+            $.hol_set,
+            $._hol_application_lhs,
+            $.hol_cond,
+            $.hol_case,
+            $.hol_binder,
+            $.hol_left_unary_term,
+            $.hol_binary_term,
+            $.hol_annotated,
+            prec(2500, seq('(', $._hol_term, ')'))
+        ),
+
+        // TODO Look into applying this pattern
+        //   https://github.com/tree-sitter/tree-sitter-c/blob/6c7f459ddc0bcf78b615d3a3f4e8fed87b8b3b1b/grammar.js#L1034
+        //   term_grammar: binders, binary expressions, ...
+
+        _hol_application_lhs: $ => choice(
+            $.hol_application,
+            $.hol_identifier,
+        ),
+
+        // TODO Define this using repeat1 somehow
+        hol_application: $ => prec.left(
+            2000,
+            seq(
+                $._hol_application_lhs,
+                choice($._hol_application_lhs, $._hol_term)
+            )
+        ),
+
+        hol_cond: $ => prec(
+            70,
+            seq('if', $._hol_term, 'then', $._hol_term, 'else', $._hol_term)
+        ),
+
+        hol_case: $ => prec.right(
+            1,
+            seq(
+                'case',
+                alias($._hol_term, $.hol_term),
+                'of',
+                optional('|'), mkSepBy1('|', $.hol_match)
+            )
+        ),
+
+        // TODO Feels hacky
+        _hol_pcon_nopare: $ => seq($.hol_cname_alphanumeric, repeat1($.hol_pat)),
+
+        hol_match: $ => seq(
+            alias(
+                choice(
+                    $._hol_pat,
+                    $._hol_pcon_nopare
+                ),
+                $.hol_pat
+            ),
+            "=>",
+            alias($._hol_term, $.hol_term),
+        ),
+
+        // TODO find better names for (_)hol_bvar
+        hol_bvar: $ => choice(
+            seq('(', $._hol_bvar, ')'),
+            $._hol_bvar,
+        ),
+
+        _hol_bvar: $ => seq(
+            alias($._hol_alphanumeric, $.hol_alphanumeric),
+            optional(seq(':', $._hol_type))
+        ),
+
+        // Permanently borrowed (and adapted) from tree-sitter/tree-sitter-c,
+        // which is released under the MIT license.
+        hol_binder: $ => {
+            const table = [
+                'OLEAST', 'LEAST', 'some', '?!!', '∃!', '?!', '∃', '?', '∀',
+                '!', '@', 'λ', '\\'
+            ];
+
+            return choice(...table.map(
+                (binder) => {
+                    return seq(
+                        binder,
+                        repeat1($.hol_bvar),
+                        '.',
+                        $._hol_term
+                    )
+            }));
+        },
+
+        hol_left_unary_term: $ => {
+            const table = [
+                ['-', 900],
+                ['¬', 900],
+                ['~', 900],
+            ];
+
+            return choice(...table.map(
+                ([operator, precedence]) => {
+                    return prec(
+                        precedence,
+                        seq(
+                            field('operator', operator),
+                            field('term', $._hol_term),
+                        )
+                    );
+
+            }));
+        },
+
+        hol_binary_term: $ => {
+            const table = [
+                ['⇎', 100, 'N'],
+                ['<=/=>', 100, 'N'],
+                ['<=>', 100, 'N'],
+                ['⇔', 100, 'N'],
+                ['==>', 200, 'L'],
+                ['⇒', 200, 'L'],
+                ['\\\/', 300, 'R'],
+                ['∨', 300, 'R'],
+                ['\/\\', 400, 'R'],
+                ['∧', 400, 'R'],
+                ['∉', 400, 'N'],
+                ['NOTIN', 400, 'N'],
+                ['∈', 400, 'N'],
+                ['IN', 400, 'N'],
+                ['≼', 450, 'N'],
+                ['<<=', 450, 'N'],
+                ['PERMUTES', 450, 'N'],
+                ['HAS_SIZE', 450, 'N'],
+                ['⊂', 450, 'N'],
+                ['PSUBSET', 450, 'N'],
+                ['⊆', 450, 'N'],
+                ['≥', 450, 'N'],
+                ['>=', 450, 'N'],
+                ['≤', 450, 'N'],
+                ['<=', 450, 'N'],
+                ['>', 450, 'N'],
+                ['<', 450, 'N'],
+                ['⊆ᵣ', 450, 'N'],
+                ['RSUBSET', 450, 'N'],
+                ['≠', 450, 'N'],
+                ['<>', 450, 'N'],
+                ['=', 450, 'N'],
+                ['$', 460, 'R'],
+                ['::', 490, 'R'],
+                ['INSERT', 490, 'R'],
+                ['+', 500, 'L'],
+                ['o', 800, 'R']
+            ];
+
+            return choice(...table.map(
+                ([operator, precedence, associativity]) => {
+                    const rule = seq(
+                        field('left', $._hol_term),
+                        field('operator', operator),
+                        field('right', $._hol_term),
+                    );
+
+                    switch (associativity) {
+                    case 'L':
+                        return prec.left(precedence, rule);
+                    case 'R':
+                        return prec.right(precedence, rule);
+                    default:
+                        // TODO Deal with non-associativity properly
+                        return prec.left(precedence, rule);
+                    }
+            }));
+        },
+
+        hol_annotated: $ => prec(
+            899,
+            seq($._hol_term, ':', $._hol_type)
+        ),
+
+        _hol_type: $ => choice(
+            $.hol_atomic_type,
+            $.hol_list_ty,
+            $.hol_fun_ty,
+            seq('(', $._hol_type, ')')
+        ),
+
+        hol_list_ty: $ => seq($._hol_type, 'list'),
+
+        hol_fun_ty: $ => prec.right(
+            50,
+            seq($._hol_type, '->', $._hol_type)
+        ),
+
+        hol_atomic_type: $ => choice(
+            'num',
+            'string',
+            // BUG? Allows 'f'oo as a type variable
+            /\'[a-zA-Z\u0370-\u03BA\u03BC-\u03FF0-9\'_]+/,
+            $._hol_alphanumeric
+        ),
+
+        hol_tuple: $ => seq(
+            '(',
+            optional(mkSepBy2(',', $._hol_term)),
+            ')'
+        ),
+
+        hol_list: $ => seq(
+            '[',
+            mkSepBy(';', $._hol_term),
+            ']'
+        ),
+
+        hol_set: $ => seq(
+            '{',
+            mkSepBy(';', $._hol_term),
+            '}'
+        ),
+
+        _hol_literal: $ => choice(
+            $.hol_number,
+            $.hol_string,
+            $.hol_character,
+            $.hol_true,
+            $.hol_false
+        ),
+
+        hol_true: $ => 'T',
+
+        hol_false: $ => 'F',
+
+        hol_number: $ => /\d[\d_]*/,
+
+        // https://gist.github.com/cellularmitosis/6fd5fc2a65225364f72d3574abd9d5d5
+        // TODO These regexes may be incorrect; alternatives were posted on
+        //   Discord
+        hol_string: $ => /\"([^\"\\]|\\.)*\"/,
+
+        // HACK Does not make sure the string is of length 1
+        hol_character: $ => /#\"([^\"\\]|\\.)*\"/
+    },
+});
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/package.json b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/package.json
new file mode 100644
index 0000000000..75bad53e00
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/package.json
@@ -0,0 +1,55 @@
+{
+  "name": "tree-sitter-holscript",
+  "version": "0.1.0",
+  "description": "HOLScript grammar for tree-sitter",
+  "repository": "github:tree-sitter/tree-sitter-holscript",
+  "license": "MIT",
+  "author": {
+    "name": "Daniel Nezamabadi"
+  },
+  "main": "bindings/node",
+  "types": "bindings/node",
+  "keywords": [
+    "incremental",
+    "parsing",
+    "tree-sitter",
+    "holscript"
+  ],
+  "files": [
+    "grammar.js",
+    "binding.gyp",
+    "prebuilds/**",
+    "bindings/node/*",
+    "queries/*",
+    "src/**",
+    "*.wasm"
+  ],
+  "dependencies": {
+    "node-addon-api": "^8.1.0",
+    "node-gyp-build": "^4.8.2"
+  },
+  "devDependencies": {
+    "prebuildify": "^6.0.1",
+    "tree-sitter-cli": "^0.24.3"
+  },
+  "peerDependencies": {
+    "tree-sitter": "^0.21.1"
+  },
+  "peerDependenciesMeta": {
+    "tree-sitter": {
+      "optional": true
+    }
+  },
+  "scripts": {
+    "install": "node-gyp-build",
+    "prestart": "tree-sitter build --wasm",
+    "start": "tree-sitter playground",
+    "test": "node --test bindings/node/*_test.js"
+  },
+  "tree-sitter": [
+    {
+      "scope": "source.holscript",
+      "injection-regex": "^holscript$"
+    }
+  ]
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/pyproject.toml b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/pyproject.toml
new file mode 100644
index 0000000000..34e45258f6
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/pyproject.toml
@@ -0,0 +1,30 @@
+[build-system]
+requires = ["setuptools>=42", "wheel"]
+build-backend = "setuptools.build_meta"
+
+[project]
+name = "tree-sitter-holscript"
+description = "HOLScript grammar for tree-sitter"
+version = "0.1.0"
+keywords = ["incremental", "parsing", "tree-sitter", "holscript"]
+classifiers = [
+  "Intended Audience :: Developers",
+  "License :: OSI Approved :: MIT License",
+  "Topic :: Software Development :: Compilers",
+  "Topic :: Text Processing :: Linguistic",
+  "Typing :: Typed",
+]
+authors = [{ name = "Daniel Nezamabadi" }]
+requires-python = ">=3.9"
+license.text = "MIT"
+readme = "README.md"
+
+[project.urls]
+Homepage = "https://github.com/hol-theorem-prover/hol/"
+
+[project.optional-dependencies]
+core = ["tree-sitter~=0.22"]
+
+[tool.cibuildwheel]
+build = "cp39-*"
+build-frontend = "build"
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/setup.py b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/setup.py
new file mode 100644
index 0000000000..f0e9f30c73
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/setup.py
@@ -0,0 +1,62 @@
+from os.path import isdir, join
+from platform import system
+
+from setuptools import Extension, find_packages, setup
+from setuptools.command.build import build
+from wheel.bdist_wheel import bdist_wheel
+
+
+class Build(build):
+    def run(self):
+        if isdir("queries"):
+            dest = join(self.build_lib, "tree_sitter_holscript", "queries")
+            self.copy_tree("queries", dest)
+        super().run()
+
+
+class BdistWheel(bdist_wheel):
+    def get_tag(self):
+        python, abi, platform = super().get_tag()
+        if python.startswith("cp"):
+            python, abi = "cp39", "abi3"
+        return python, abi, platform
+
+
+setup(
+    packages=find_packages("bindings/python"),
+    package_dir={"": "bindings/python"},
+    package_data={
+        "tree_sitter_holscript": ["*.pyi", "py.typed"],
+        "tree_sitter_holscript.queries": ["*.scm"],
+    },
+    ext_package="tree_sitter_holscript",
+    ext_modules=[
+        Extension(
+            name="_binding",
+            sources=[
+                "bindings/python/tree_sitter_holscript/binding.c",
+                "src/parser.c",
+                # NOTE: if your language uses an external scanner, add it here.
+            ],
+            extra_compile_args=[
+                "-std=c11",
+                "-fvisibility=hidden",
+            ] if system() != "Windows" else [
+                "/std:c11",
+                "/utf-8",
+            ],
+            define_macros=[
+                ("Py_LIMITED_API", "0x03090000"),
+                ("PY_SSIZE_T_CLEAN", None),
+                ("TREE_SITTER_HIDE_SYMBOLS", None),
+            ],
+            include_dirs=["src"],
+            py_limited_api=True,
+        )
+    ],
+    cmdclass={
+        "build": Build,
+        "bdist_wheel": BdistWheel
+    },
+    zip_safe=False
+)
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/scanner.c b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/scanner.c
new file mode 100644
index 0000000000..a656667386
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/scanner.c
@@ -0,0 +1,135 @@
+// Adapted tree-sitter-sml by Matthew Fluet, released under the MIT license.
+#include <wctype.h>
+#include <tree_sitter/parser.h>
+
+enum TokenType {
+  BLOCK_COMMENT,
+  LINE_COMMENT,
+};
+
+void * tree_sitter_holscript_external_scanner_create() {
+  return NULL;
+}
+
+void tree_sitter_holscript_external_scanner_destroy(__attribute__ ((unused)) void *payload) {
+  return;
+}
+
+unsigned tree_sitter_holscript_external_scanner_serialize(__attribute__ ((unused)) void *payload, __attribute__ ((unused)) char *buffer) {
+  return 0;
+}
+
+void tree_sitter_holscript_external_scanner_deserialize(__attribute__ ((unused)) void *payload, __attribute__ ((unused)) const char *buffer, __attribute__ ((unused)) unsigned length) {
+  return;
+}
+
+bool tree_sitter_holscript_external_scanner_finish_line_comment(TSLexer *lexer) {
+  while (true) {
+    if (lexer->eof(lexer)) return false;
+    switch (lexer->lookahead) {
+    case '\n':
+      lexer->advance(lexer, false);
+      return true;
+    case '\r':
+      lexer->advance(lexer, false);
+      if (!lexer->eof(lexer) && lexer->lookahead == '\n') {
+        lexer->advance(lexer, false);
+      }
+      return true;
+    default:
+      lexer->advance(lexer, false);
+      continue;
+    }
+  }
+}
+
+bool tree_sitter_holscript_external_scanner_finish_block_comment(TSLexer *lexer, bool line_comment) {
+  unsigned depth = 1;
+  while (true) {
+    if (lexer->eof(lexer)) return false;
+    switch (lexer->lookahead) {
+    case '(':
+      lexer->advance(lexer, false);
+      if (lexer->eof(lexer)) return false;
+      if (lexer->lookahead == '*') {
+        lexer->advance(lexer, false);
+        if (lexer->eof(lexer)) return false;
+        if (line_comment && lexer->lookahead == ')') {
+          lexer->advance(lexer, false);
+          if (tree_sitter_holscript_external_scanner_finish_line_comment(lexer)) {
+            continue;
+          } else {
+            return false;
+          }
+        } else {
+          depth += 1;
+          continue;
+        }
+      } else {
+        continue;
+      };
+    case '*':
+      lexer->advance(lexer, false);
+      if (lexer->eof(lexer)) return false;
+      if (lexer->lookahead == ')') {
+        lexer->advance(lexer, false);
+        depth -= 1;
+        if (depth == 0) {
+          return true;
+        } else {
+          continue;
+        }
+      } else {
+        continue;
+      };
+    default:
+      lexer->advance(lexer, false);
+      continue;
+    }
+  }
+}
+
+bool tree_sitter_holscript_external_scanner_scan_comment(TSLexer *lexer, bool block_comment, bool line_comment) {
+  while (!lexer->eof(lexer) && iswspace(lexer->lookahead)) {
+    lexer->advance(lexer, true);
+  }
+  if (lexer->eof(lexer)) return false;
+  if (lexer->lookahead == '(') {
+    lexer->advance(lexer, false);
+    if (lexer->eof(lexer)) return false;
+    if (lexer->lookahead == '*') {
+      lexer->advance(lexer, false);
+      if (lexer->eof(lexer)) return false;
+      if (line_comment && lexer->lookahead == ')') {
+        lexer->advance(lexer, false);
+        if (tree_sitter_holscript_external_scanner_finish_line_comment(lexer)) {
+          lexer->result_symbol = LINE_COMMENT;
+          return true;
+        } else {
+          return false;
+        }
+      } else if (block_comment) {
+        if (tree_sitter_holscript_external_scanner_finish_block_comment(lexer, line_comment)) {
+          lexer->result_symbol = BLOCK_COMMENT;
+          return true;
+        } else {
+          return false;
+        }
+      } else {
+        return false;
+      }
+    } else {
+      return false;
+    }
+  } else {
+    return false;
+  }
+}
+
+bool tree_sitter_holscript_external_scanner_scan(__attribute__ ((unused)) void *payload, TSLexer *lexer, const bool *valid_symbols) {
+  if (valid_symbols[BLOCK_COMMENT] || valid_symbols[LINE_COMMENT]) {
+    return tree_sitter_holscript_external_scanner_scan_comment(lexer, valid_symbols[BLOCK_COMMENT], valid_symbols[LINE_COMMENT]);
+  } else {
+    return false;
+  }
+}
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/alloc.h b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/alloc.h
new file mode 100644
index 0000000000..1abdd12015
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/alloc.h
@@ -0,0 +1,54 @@
+#ifndef TREE_SITTER_ALLOC_H_
+#define TREE_SITTER_ALLOC_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+
+// Allow clients to override allocation functions
+#ifdef TREE_SITTER_REUSE_ALLOCATOR
+
+extern void *(*ts_current_malloc)(size_t size);
+extern void *(*ts_current_calloc)(size_t count, size_t size);
+extern void *(*ts_current_realloc)(void *ptr, size_t size);
+extern void (*ts_current_free)(void *ptr);
+
+#ifndef ts_malloc
+#define ts_malloc  ts_current_malloc
+#endif
+#ifndef ts_calloc
+#define ts_calloc  ts_current_calloc
+#endif
+#ifndef ts_realloc
+#define ts_realloc ts_current_realloc
+#endif
+#ifndef ts_free
+#define ts_free    ts_current_free
+#endif
+
+#else
+
+#ifndef ts_malloc
+#define ts_malloc  malloc
+#endif
+#ifndef ts_calloc
+#define ts_calloc  calloc
+#endif
+#ifndef ts_realloc
+#define ts_realloc realloc
+#endif
+#ifndef ts_free
+#define ts_free    free
+#endif
+
+#endif
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif // TREE_SITTER_ALLOC_H_
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/array.h b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/array.h
new file mode 100644
index 0000000000..15a3b233bb
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/array.h
@@ -0,0 +1,290 @@
+#ifndef TREE_SITTER_ARRAY_H_
+#define TREE_SITTER_ARRAY_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include "./alloc.h"
+
+#include <assert.h>
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdlib.h>
+#include <string.h>
+
+#ifdef _MSC_VER
+#pragma warning(disable : 4101)
+#elif defined(__GNUC__) || defined(__clang__)
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Wunused-variable"
+#endif
+
+#define Array(T)       \
+  struct {             \
+    T *contents;       \
+    uint32_t size;     \
+    uint32_t capacity; \
+  }
+
+/// Initialize an array.
+#define array_init(self) \
+  ((self)->size = 0, (self)->capacity = 0, (self)->contents = NULL)
+
+/// Create an empty array.
+#define array_new() \
+  { NULL, 0, 0 }
+
+/// Get a pointer to the element at a given `index` in the array.
+#define array_get(self, _index) \
+  (assert((uint32_t)(_index) < (self)->size), &(self)->contents[_index])
+
+/// Get a pointer to the first element in the array.
+#define array_front(self) array_get(self, 0)
+
+/// Get a pointer to the last element in the array.
+#define array_back(self) array_get(self, (self)->size - 1)
+
+/// Clear the array, setting its size to zero. Note that this does not free any
+/// memory allocated for the array's contents.
+#define array_clear(self) ((self)->size = 0)
+
+/// Reserve `new_capacity` elements of space in the array. If `new_capacity` is
+/// less than the array's current capacity, this function has no effect.
+#define array_reserve(self, new_capacity) \
+  _array__reserve((Array *)(self), array_elem_size(self), new_capacity)
+
+/// Free any memory allocated for this array. Note that this does not free any
+/// memory allocated for the array's contents.
+#define array_delete(self) _array__delete((Array *)(self))
+
+/// Push a new `element` onto the end of the array.
+#define array_push(self, element)                            \
+  (_array__grow((Array *)(self), 1, array_elem_size(self)), \
+   (self)->contents[(self)->size++] = (element))
+
+/// Increase the array's size by `count` elements.
+/// New elements are zero-initialized.
+#define array_grow_by(self, count) \
+  do { \
+    if ((count) == 0) break; \
+    _array__grow((Array *)(self), count, array_elem_size(self)); \
+    memset((self)->contents + (self)->size, 0, (count) * array_elem_size(self)); \
+    (self)->size += (count); \
+  } while (0)
+
+/// Append all elements from one array to the end of another.
+#define array_push_all(self, other)                                       \
+  array_extend((self), (other)->size, (other)->contents)
+
+/// Append `count` elements to the end of the array, reading their values from the
+/// `contents` pointer.
+#define array_extend(self, count, contents)                    \
+  _array__splice(                                               \
+    (Array *)(self), array_elem_size(self), (self)->size, \
+    0, count,  contents                                        \
+  )
+
+/// Remove `old_count` elements from the array starting at the given `index`. At
+/// the same index, insert `new_count` new elements, reading their values from the
+/// `new_contents` pointer.
+#define array_splice(self, _index, old_count, new_count, new_contents)  \
+  _array__splice(                                                       \
+    (Array *)(self), array_elem_size(self), _index,                \
+    old_count, new_count, new_contents                                 \
+  )
+
+/// Insert one `element` into the array at the given `index`.
+#define array_insert(self, _index, element) \
+  _array__splice((Array *)(self), array_elem_size(self), _index, 0, 1, &(element))
+
+/// Remove one element from the array at the given `index`.
+#define array_erase(self, _index) \
+  _array__erase((Array *)(self), array_elem_size(self), _index)
+
+/// Pop the last element off the array, returning the element by value.
+#define array_pop(self) ((self)->contents[--(self)->size])
+
+/// Assign the contents of one array to another, reallocating if necessary.
+#define array_assign(self, other) \
+  _array__assign((Array *)(self), (const Array *)(other), array_elem_size(self))
+
+/// Swap one array with another
+#define array_swap(self, other) \
+  _array__swap((Array *)(self), (Array *)(other))
+
+/// Get the size of the array contents
+#define array_elem_size(self) (sizeof *(self)->contents)
+
+/// Search a sorted array for a given `needle` value, using the given `compare`
+/// callback to determine the order.
+///
+/// If an existing element is found to be equal to `needle`, then the `index`
+/// out-parameter is set to the existing value's index, and the `exists`
+/// out-parameter is set to true. Otherwise, `index` is set to an index where
+/// `needle` should be inserted in order to preserve the sorting, and `exists`
+/// is set to false.
+#define array_search_sorted_with(self, compare, needle, _index, _exists) \
+  _array__search_sorted(self, 0, compare, , needle, _index, _exists)
+
+/// Search a sorted array for a given `needle` value, using integer comparisons
+/// of a given struct field (specified with a leading dot) to determine the order.
+///
+/// See also `array_search_sorted_with`.
+#define array_search_sorted_by(self, field, needle, _index, _exists) \
+  _array__search_sorted(self, 0, _compare_int, field, needle, _index, _exists)
+
+/// Insert a given `value` into a sorted array, using the given `compare`
+/// callback to determine the order.
+#define array_insert_sorted_with(self, compare, value) \
+  do { \
+    unsigned _index, _exists; \
+    array_search_sorted_with(self, compare, &(value), &_index, &_exists); \
+    if (!_exists) array_insert(self, _index, value); \
+  } while (0)
+
+/// Insert a given `value` into a sorted array, using integer comparisons of
+/// a given struct field (specified with a leading dot) to determine the order.
+///
+/// See also `array_search_sorted_by`.
+#define array_insert_sorted_by(self, field, value) \
+  do { \
+    unsigned _index, _exists; \
+    array_search_sorted_by(self, field, (value) field, &_index, &_exists); \
+    if (!_exists) array_insert(self, _index, value); \
+  } while (0)
+
+// Private
+
+typedef Array(void) Array;
+
+/// This is not what you're looking for, see `array_delete`.
+static inline void _array__delete(Array *self) {
+  if (self->contents) {
+    ts_free(self->contents);
+    self->contents = NULL;
+    self->size = 0;
+    self->capacity = 0;
+  }
+}
+
+/// This is not what you're looking for, see `array_erase`.
+static inline void _array__erase(Array *self, size_t element_size,
+                                uint32_t index) {
+  assert(index < self->size);
+  char *contents = (char *)self->contents;
+  memmove(contents + index * element_size, contents + (index + 1) * element_size,
+          (self->size - index - 1) * element_size);
+  self->size--;
+}
+
+/// This is not what you're looking for, see `array_reserve`.
+static inline void _array__reserve(Array *self, size_t element_size, uint32_t new_capacity) {
+  if (new_capacity > self->capacity) {
+    if (self->contents) {
+      self->contents = ts_realloc(self->contents, new_capacity * element_size);
+    } else {
+      self->contents = ts_malloc(new_capacity * element_size);
+    }
+    self->capacity = new_capacity;
+  }
+}
+
+/// This is not what you're looking for, see `array_assign`.
+static inline void _array__assign(Array *self, const Array *other, size_t element_size) {
+  _array__reserve(self, element_size, other->size);
+  self->size = other->size;
+  memcpy(self->contents, other->contents, self->size * element_size);
+}
+
+/// This is not what you're looking for, see `array_swap`.
+static inline void _array__swap(Array *self, Array *other) {
+  Array swap = *other;
+  *other = *self;
+  *self = swap;
+}
+
+/// This is not what you're looking for, see `array_push` or `array_grow_by`.
+static inline void _array__grow(Array *self, uint32_t count, size_t element_size) {
+  uint32_t new_size = self->size + count;
+  if (new_size > self->capacity) {
+    uint32_t new_capacity = self->capacity * 2;
+    if (new_capacity < 8) new_capacity = 8;
+    if (new_capacity < new_size) new_capacity = new_size;
+    _array__reserve(self, element_size, new_capacity);
+  }
+}
+
+/// This is not what you're looking for, see `array_splice`.
+static inline void _array__splice(Array *self, size_t element_size,
+                                 uint32_t index, uint32_t old_count,
+                                 uint32_t new_count, const void *elements) {
+  uint32_t new_size = self->size + new_count - old_count;
+  uint32_t old_end = index + old_count;
+  uint32_t new_end = index + new_count;
+  assert(old_end <= self->size);
+
+  _array__reserve(self, element_size, new_size);
+
+  char *contents = (char *)self->contents;
+  if (self->size > old_end) {
+    memmove(
+      contents + new_end * element_size,
+      contents + old_end * element_size,
+      (self->size - old_end) * element_size
+    );
+  }
+  if (new_count > 0) {
+    if (elements) {
+      memcpy(
+        (contents + index * element_size),
+        elements,
+        new_count * element_size
+      );
+    } else {
+      memset(
+        (contents + index * element_size),
+        0,
+        new_count * element_size
+      );
+    }
+  }
+  self->size += new_count - old_count;
+}
+
+/// A binary search routine, based on Rust's `std::slice::binary_search_by`.
+/// This is not what you're looking for, see `array_search_sorted_with` or `array_search_sorted_by`.
+#define _array__search_sorted(self, start, compare, suffix, needle, _index, _exists) \
+  do { \
+    *(_index) = start; \
+    *(_exists) = false; \
+    uint32_t size = (self)->size - *(_index); \
+    if (size == 0) break; \
+    int comparison; \
+    while (size > 1) { \
+      uint32_t half_size = size / 2; \
+      uint32_t mid_index = *(_index) + half_size; \
+      comparison = compare(&((self)->contents[mid_index] suffix), (needle)); \
+      if (comparison <= 0) *(_index) = mid_index; \
+      size -= half_size; \
+    } \
+    comparison = compare(&((self)->contents[*(_index)] suffix), (needle)); \
+    if (comparison == 0) *(_exists) = true; \
+    else if (comparison < 0) *(_index) += 1; \
+  } while (0)
+
+/// Helper macro for the `_sorted_by` routines below. This takes the left (existing)
+/// parameter by reference in order to work with the generic sorting function above.
+#define _compare_int(a, b) ((int)*(a) - (int)(b))
+
+#ifdef _MSC_VER
+#pragma warning(default : 4101)
+#elif defined(__GNUC__) || defined(__clang__)
+#pragma GCC diagnostic pop
+#endif
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif  // TREE_SITTER_ARRAY_H_
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/parser.h b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/parser.h
new file mode 100644
index 0000000000..799f599bd4
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/src/tree_sitter/parser.h
@@ -0,0 +1,266 @@
+#ifndef TREE_SITTER_PARSER_H_
+#define TREE_SITTER_PARSER_H_
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+#include <stdbool.h>
+#include <stdint.h>
+#include <stdlib.h>
+
+#define ts_builtin_sym_error ((TSSymbol)-1)
+#define ts_builtin_sym_end 0
+#define TREE_SITTER_SERIALIZATION_BUFFER_SIZE 1024
+
+#ifndef TREE_SITTER_API_H_
+typedef uint16_t TSStateId;
+typedef uint16_t TSSymbol;
+typedef uint16_t TSFieldId;
+typedef struct TSLanguage TSLanguage;
+#endif
+
+typedef struct {
+  TSFieldId field_id;
+  uint8_t child_index;
+  bool inherited;
+} TSFieldMapEntry;
+
+typedef struct {
+  uint16_t index;
+  uint16_t length;
+} TSFieldMapSlice;
+
+typedef struct {
+  bool visible;
+  bool named;
+  bool supertype;
+} TSSymbolMetadata;
+
+typedef struct TSLexer TSLexer;
+
+struct TSLexer {
+  int32_t lookahead;
+  TSSymbol result_symbol;
+  void (*advance)(TSLexer *, bool);
+  void (*mark_end)(TSLexer *);
+  uint32_t (*get_column)(TSLexer *);
+  bool (*is_at_included_range_start)(const TSLexer *);
+  bool (*eof)(const TSLexer *);
+  void (*log)(const TSLexer *, const char *, ...);
+};
+
+typedef enum {
+  TSParseActionTypeShift,
+  TSParseActionTypeReduce,
+  TSParseActionTypeAccept,
+  TSParseActionTypeRecover,
+} TSParseActionType;
+
+typedef union {
+  struct {
+    uint8_t type;
+    TSStateId state;
+    bool extra;
+    bool repetition;
+  } shift;
+  struct {
+    uint8_t type;
+    uint8_t child_count;
+    TSSymbol symbol;
+    int16_t dynamic_precedence;
+    uint16_t production_id;
+  } reduce;
+  uint8_t type;
+} TSParseAction;
+
+typedef struct {
+  uint16_t lex_state;
+  uint16_t external_lex_state;
+} TSLexMode;
+
+typedef union {
+  TSParseAction action;
+  struct {
+    uint8_t count;
+    bool reusable;
+  } entry;
+} TSParseActionEntry;
+
+typedef struct {
+  int32_t start;
+  int32_t end;
+} TSCharacterRange;
+
+struct TSLanguage {
+  uint32_t version;
+  uint32_t symbol_count;
+  uint32_t alias_count;
+  uint32_t token_count;
+  uint32_t external_token_count;
+  uint32_t state_count;
+  uint32_t large_state_count;
+  uint32_t production_id_count;
+  uint32_t field_count;
+  uint16_t max_alias_sequence_length;
+  const uint16_t *parse_table;
+  const uint16_t *small_parse_table;
+  const uint32_t *small_parse_table_map;
+  const TSParseActionEntry *parse_actions;
+  const char * const *symbol_names;
+  const char * const *field_names;
+  const TSFieldMapSlice *field_map_slices;
+  const TSFieldMapEntry *field_map_entries;
+  const TSSymbolMetadata *symbol_metadata;
+  const TSSymbol *public_symbol_map;
+  const uint16_t *alias_map;
+  const TSSymbol *alias_sequences;
+  const TSLexMode *lex_modes;
+  bool (*lex_fn)(TSLexer *, TSStateId);
+  bool (*keyword_lex_fn)(TSLexer *, TSStateId);
+  TSSymbol keyword_capture_token;
+  struct {
+    const bool *states;
+    const TSSymbol *symbol_map;
+    void *(*create)(void);
+    void (*destroy)(void *);
+    bool (*scan)(void *, TSLexer *, const bool *symbol_whitelist);
+    unsigned (*serialize)(void *, char *);
+    void (*deserialize)(void *, const char *, unsigned);
+  } external_scanner;
+  const TSStateId *primary_state_ids;
+};
+
+static inline bool set_contains(TSCharacterRange *ranges, uint32_t len, int32_t lookahead) {
+  uint32_t index = 0;
+  uint32_t size = len - index;
+  while (size > 1) {
+    uint32_t half_size = size / 2;
+    uint32_t mid_index = index + half_size;
+    TSCharacterRange *range = &ranges[mid_index];
+    if (lookahead >= range->start && lookahead <= range->end) {
+      return true;
+    } else if (lookahead > range->end) {
+      index = mid_index;
+    }
+    size -= half_size;
+  }
+  TSCharacterRange *range = &ranges[index];
+  return (lookahead >= range->start && lookahead <= range->end);
+}
+
+/*
+ *  Lexer Macros
+ */
+
+#ifdef _MSC_VER
+#define UNUSED __pragma(warning(suppress : 4101))
+#else
+#define UNUSED __attribute__((unused))
+#endif
+
+#define START_LEXER()           \
+  bool result = false;          \
+  bool skip = false;            \
+  UNUSED                        \
+  bool eof = false;             \
+  int32_t lookahead;            \
+  goto start;                   \
+  next_state:                   \
+  lexer->advance(lexer, skip);  \
+  start:                        \
+  skip = false;                 \
+  lookahead = lexer->lookahead;
+
+#define ADVANCE(state_value) \
+  {                          \
+    state = state_value;     \
+    goto next_state;         \
+  }
+
+#define ADVANCE_MAP(...)                                              \
+  {                                                                   \
+    static const uint16_t map[] = { __VA_ARGS__ };                    \
+    for (uint32_t i = 0; i < sizeof(map) / sizeof(map[0]); i += 2) {  \
+      if (map[i] == lookahead) {                                      \
+        state = map[i + 1];                                           \
+        goto next_state;                                              \
+      }                                                               \
+    }                                                                 \
+  }
+
+#define SKIP(state_value) \
+  {                       \
+    skip = true;          \
+    state = state_value;  \
+    goto next_state;      \
+  }
+
+#define ACCEPT_TOKEN(symbol_value)     \
+  result = true;                       \
+  lexer->result_symbol = symbol_value; \
+  lexer->mark_end(lexer);
+
+#define END_STATE() return result;
+
+/*
+ *  Parse Table Macros
+ */
+
+#define SMALL_STATE(id) ((id) - LARGE_STATE_COUNT)
+
+#define STATE(id) id
+
+#define ACTIONS(id) id
+
+#define SHIFT(state_value)            \
+  {{                                  \
+    .shift = {                        \
+      .type = TSParseActionTypeShift, \
+      .state = (state_value)          \
+    }                                 \
+  }}
+
+#define SHIFT_REPEAT(state_value)     \
+  {{                                  \
+    .shift = {                        \
+      .type = TSParseActionTypeShift, \
+      .state = (state_value),         \
+      .repetition = true              \
+    }                                 \
+  }}
+
+#define SHIFT_EXTRA()                 \
+  {{                                  \
+    .shift = {                        \
+      .type = TSParseActionTypeShift, \
+      .extra = true                   \
+    }                                 \
+  }}
+
+#define REDUCE(symbol_name, children, precedence, prod_id) \
+  {{                                                       \
+    .reduce = {                                            \
+      .type = TSParseActionTypeReduce,                     \
+      .symbol = symbol_name,                               \
+      .child_count = children,                             \
+      .dynamic_precedence = precedence,                    \
+      .production_id = prod_id                             \
+    },                                                     \
+  }}
+
+#define RECOVER()                    \
+  {{                                 \
+    .type = TSParseActionTypeRecover \
+  }}
+
+#define ACCEPT_INPUT()              \
+  {{                                \
+    .type = TSParseActionTypeAccept \
+  }}
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif  // TREE_SITTER_PARSER_H_
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/datatype.txt b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/datatype.txt
new file mode 100644
index 0000000000..778f60ea7f
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/datatype.txt
@@ -0,0 +1,123 @@
+========================
+One 0-Arity Constructor
+========================
+
+Datatype:
+  nil = Nil
+End
+
+---
+
+(source_file
+  (hol_datatype
+    (hol_binding
+      (hol_identifier)
+      (hol_constructor
+        (hol_clause
+          (hol_identifier))))))
+
+
+=================
+Extended Numbers
+=================
+
+Datatype:
+  extnum = FinNum num | PosInf
+End
+
+---
+
+(source_file
+  (hol_datatype
+    (hol_binding
+      (hol_identifier)
+      (hol_constructor
+        (hol_clause
+          (hol_identifier)
+          (hol_atomic_type))
+        (hol_clause
+          (hol_identifier))))))
+
+
+=====================
+Simple Type Variable
+=====================
+
+Datatype:
+  foo = Foo 'a
+End
+
+---
+
+(source_file
+  (hol_datatype
+    (hol_binding
+      (hol_identifier)
+      (hol_constructor
+        (hol_clause
+          (hol_identifier)
+          (hol_atomic_type))))))
+
+
+=====================
+'g_a_p Type Variable
+=====================
+
+Datatype:
+  foo = Foo 'g_a_p
+End
+
+---
+
+(source_file
+  (hol_datatype
+    (hol_binding
+      (hol_identifier)
+      (hol_constructor
+        (hol_clause
+          (hol_identifier)
+          (hol_atomic_type))))))
+
+
+============
+String Type
+============
+
+Datatype:
+  foo = Foo string
+End
+
+---
+
+(source_file
+  (hol_datatype
+    (hol_binding
+      (hol_identifier)
+      (hol_constructor
+        (hol_clause
+          (hol_identifier)
+          (hol_atomic_type))))))
+
+
+===============
+"Complex" Type
+===============
+
+Datatype:
+  sexp = Atom string | Expr (sexp list)
+End
+
+---
+
+(source_file
+  (hol_datatype
+    (hol_binding
+      (hol_identifier)
+      (hol_constructor
+        (hol_clause
+          (hol_identifier)
+          (hol_atomic_type))
+        (hol_clause
+          (hol_identifier)
+          (hol_list_ty
+            (hol_atomic_type)))))))
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/definition.txt b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/definition.txt
new file mode 100644
index 0000000000..ec72aa3c71
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/definition.txt
@@ -0,0 +1,285 @@
+=============
+Alphanumeric
+=============
+
+Definition foo_def:
+  foo = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+            (hol_number))))))
+
+
+==============
+Parenthesized
+==============
+
+Definition foo_def:
+  (foo = 0)
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+            (hol_number))))))
+
+
+========
+Dollars
+========
+
+Definition dollars_def:
+  $$ = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+            (hol_number))))))
+
+
+============
+Bad Dollars
+
+:error
+============
+
+Definition dollars_def:
+  $dollar$dollar = 0
+End
+
+
+=========
+Symbolic
+=========
+
+Definition symbols_def:
+  #?+*/\=<>&%@!:|- = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+            (hol_number))))))
+
+=========
+Variable
+=========
+
+Definition foo_def:
+  foo x = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+            (hol_number))))))
+
+=========
+Wildcard
+=========
+
+Definition foo_def:
+  foo _ x = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_wildcard))
+        (hol_pat
+          (hol_variable))
+        (hol_term
+            (hol_number))))))
+
+
+=========================
+Alphanumeric Constructor
+=========================
+
+Definition foo_def:
+  foo NONE = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_cname_alphanumeric))
+        (hol_term
+            (hol_number))))))
+
+
+==============
+Tuple Pattern
+==============
+
+Definition fst_def:
+  fst (a, b) = a
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_ptuple
+            (hol_pat
+              (hol_variable))
+            (hol_pat
+              (hol_variable))))
+        (hol_term
+            (hol_identifier))))))
+
+
+================
+Nested Patterns
+================
+
+Definition foo_def:
+  foo (SOME x) = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_cname_alphanumeric)
+          (hol_pat
+            (hol_variable)))
+        (hol_term
+            (hol_number))))))
+
+
+===================
+Multiple Equations
+===================
+
+Definition foo_def:
+  foo (SOME x) = 0 ∧
+  foo NONE = 1
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_cname_alphanumeric)
+          (hol_pat
+            (hol_variable)))
+        (hol_term
+            (hol_number)))
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_cname_alphanumeric))
+        (hol_term
+            (hol_number))))))
+
+
+=================
+With Termination
+=================
+
+Definition foo_def:
+  foo = 0
+Termination
+  gvs
+End
+
+---
+
+(source_file
+  (hol_definition_with_proof
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+            (hol_number))))
+    (tactic
+      (vid_exp
+            (longvid
+              (vid))))))
+
+
+===========
+Attributes
+===========
+
+Definition foo_def[simp, bar]:
+  foo = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_attributes
+      (attribute)
+      (attribute))
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+            (hol_number))))))
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/quote.txt b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/quote.txt
new file mode 100644
index 0000000000..fce67dee3e
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/quote.txt
@@ -0,0 +1,89 @@
+======
+Basic
+======
+
+val _ = ‘a’
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (backquote
+        (quoted)))))
+
+
+======
+ASCII
+======
+
+val _ = `a`
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (backquote
+        (quoted)))))
+
+
+==========
+Antiquote
+==========
+
+val _ = ‘^x’
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (backquote
+        (antiquoted
+          (sml_variable))))))
+
+
+========================
+Antiquote (Parentheses)
+========================
+
+val _ = ‘^(x)’
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (backquote
+        (antiquoted
+          (vid_exp
+            (longvid
+              (vid))))))))
+
+
+======
+Mixed
+======
+
+val _ = ‘foo ^x ^(x) bar’
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (backquote
+        (quoted)
+        (antiquoted
+          (sml_variable))
+        (antiquoted
+          (vid_exp
+            (longvid
+              (vid))))
+        (quoted)))))
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/term.txt b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/term.txt
new file mode 100644
index 0000000000..cde3bcf6cd
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/term.txt
@@ -0,0 +1,955 @@
+===============
+String Literal
+===============
+
+Definition strlit_def:
+  strlit = "cake"
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+          (hol_string))))))
+
+
+==================
+Character Literal
+==================
+
+Definition charlit_def:
+  charlit = #"c"
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+          (hol_character))))))
+
+
+========
+0-Tuple
+========
+
+Definition tuple0_def:
+  tuple0 = ()
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+          (hol_tuple))))))
+
+
+========
+2-Tuple
+========
+
+Definition tuple2_def:
+  tuple2 x y = (x, y)
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_tuple
+            (hol_identifier)
+            (hol_identifier)))))))
+
+
+========
+3-Tuple
+========
+
+Definition tuple3_def:
+  tuple3 x y = (x, y, 1)
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_tuple
+            (hol_identifier)
+            (hol_identifier)
+            (hol_number)))))))
+
+
+===========
+Empty List
+===========
+
+Definition empty_list_def:
+  empty_list = []
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+          (hol_list))))))
+
+===============
+Singleton List
+===============
+
+Definition singleton_list_def:
+  singleton_list = [1]
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+          (hol_list
+            (hol_number)))))))
+
+
+==========
+Cons List
+==========
+
+Definition foo_def:
+  foo = (x::1::[])
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+          (hol_binary_term
+            (hol_identifier)
+            (hol_binary_term
+              (hol_number)
+              (hol_list))))))))
+=====
+List
+=====
+
+Definition list_def:
+  list x = [1; x]
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_list
+            (hol_number)
+            (hol_identifier)))))))
+
+
+==========
+Increment
+==========
+
+Definition incr_def:
+  incr x = x + 1
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_binary_term
+            (hol_identifier)
+            (hol_number)))))))
+
+
+===================
+Empty List Pattern
+===================
+
+Definition empty_def:
+  empty [] = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_plist))
+        (hol_term
+          (hol_number))))))
+
+
+=======================
+Singleton List Pattern
+=======================
+
+Definition singleton_def:
+  singleton [e] = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_plist
+            (hol_pat
+              (hol_variable))))
+        (hol_term
+          (hol_number))))))
+
+
+=============
+List Pattern
+=============
+
+Definition list_def:
+  list [e; f] = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_plist
+            (hol_pat
+              (hol_variable))
+            (hol_pat
+              (hol_variable))))
+        (hol_term
+          (hol_number))))))
+
+
+=============
+Cons Pattern
+=============
+
+Definition cons_def:
+  cons (x::xs) = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_pcons
+            (hol_pat
+              (hol_variable))
+            (hol_pat
+              (hol_variable))))
+        (hol_term
+          (hol_number))))))
+
+
+===================
+More Cons Patterns
+===================
+
+Definition cons_def:
+  cons (x::x'::[]) = 0
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_pcons
+            (hol_pat
+              (hol_variable))
+            (hol_pat
+              (hol_variable))
+            (hol_pat
+              (hol_plist))))
+        (hol_term
+          (hol_number))))))
+
+
+=======================
+Number Literal Pattern
+=======================
+
+Definition foo_def:
+  foo 2 = 2
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_number))
+        (hol_term
+          (hol_number))))))
+
+
+==========================
+Character Literal Pattern
+==========================
+
+Definition foo_def:
+  foo #"c" = 2
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_character))
+        (hol_term
+          (hol_number))))))
+
+
+=======================
+String Literal Pattern
+=======================
+
+Definition foo_def:
+  foo "foo" = 2
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_string))
+        (hol_term
+          (hol_number))))))
+
+
+=====================
+Function Application
+=====================
+
+Definition foo_def:
+  foo x = incr x
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_application
+            (hol_identifier)
+            (hol_identifier)))))))
+
+
+==========================
+More Function Application
+==========================
+
+Definition foo_def:
+  foo x = add x 2
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_application
+            (hol_application
+              (hol_identifier)
+              (hol_identifier))
+            (hol_number)))))))
+
+
+==================
+Annotated Pattern
+==================
+
+Definition foo_def:
+  foo (x : num) = 2
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable)
+          (hol_pannotation
+            (hol_atomic_type)))
+        (hol_term
+          (hol_number))))))
+
+
+============
+Conditional
+============
+
+Definition foo_def:
+  foo x = if bar x then 0 else 1
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_cond
+            (hol_application
+              (hol_identifier)
+              (hol_identifier))
+            (hol_number)
+            (hol_number)))))))
+
+
+=================
+Case Distinction
+=================
+
+Definition foo_def:
+  foo x = case x of SOME x => x | NONE => ARB
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_case
+            (hol_term
+              (hol_identifier))
+            (hol_match
+              (hol_pat
+                (hol_cname_alphanumeric)
+                (hol_pat
+                  (hol_variable)))
+              (hol_term
+                (hol_identifier)))
+            (hol_match
+              (hol_pat
+                (hol_cname_alphanumeric))
+              (hol_term
+                (hol_identifier)))))))))
+
+
+=================================
+Case Distinction with Extra Pipe
+=================================
+
+Definition foo_def:
+  foo x = case x of
+    | SOME x => x
+    | NONE => ARB
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_pat
+          (hol_variable))
+        (hol_term
+          (hol_case
+            (hol_term
+              (hol_identifier))
+            (hol_match
+              (hol_pat
+                (hol_cname_alphanumeric)
+                (hol_pat
+                  (hol_variable)))
+              (hol_term
+                (hol_identifier)))
+            (hol_match
+              (hol_pat
+                (hol_cname_alphanumeric))
+              (hol_term
+                (hol_identifier)))))))))
+
+
+============
+Nested Case
+============
+
+Definition foo_def:
+  foo = case x of NONE => case x of NONE => ARB | NONE => ARB
+End
+
+---
+
+(source_file
+  (hol_definition
+    (hol_defname)
+    (hol_fn_spec
+      (hol_eqn
+        (hol_identifier)
+        (hol_term
+          (hol_case
+            (hol_term
+              (hol_identifier))
+            (hol_match
+              (hol_pat
+                (hol_cname_alphanumeric))
+              (hol_term
+                (hol_case
+                  (hol_term
+                    (hol_identifier))
+                  (hol_match
+                    (hol_pat
+                       (hol_cname_alphanumeric))
+                    (hol_term
+                      (hol_identifier)))
+                  (hol_match
+                    (hol_pat
+                       (hol_cname_alphanumeric))
+                    (hol_term
+                      (hol_identifier))))))))))))
+
+
+==============================
+Implication + Less Than Equal
+==============================
+
+Theorem foo:
+  ∀x. read_quoted_aux cs acc = foo ⇒ LENGTH y ≤ LENGTH cs
+Proof
+  cheat
+QED
+
+---
+
+(source_file
+  (hol_theorem_with_proof
+    (hol_thmname)
+    (hol_thmstmt
+      (hol_binder
+      (hol_bvar
+            (hol_alphanumeric))
+        (hol_binary_term
+          (hol_binary_term
+            (hol_application
+              (hol_application
+                (hol_identifier)
+                (hol_identifier))
+              (hol_identifier))
+            (hol_identifier))
+          (hol_binary_term
+            (hol_application
+              (hol_identifier)
+              (hol_identifier))
+            (hol_application
+              (hol_identifier)
+              (hol_identifier))))))
+    (tactic
+      (vid_exp
+        (longvid
+          (vid))))))
+
+
+=======
+Dollar
+=======
+
+val _ = “a $ b $ c”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binary_term
+          (hol_identifier)
+          (hol_binary_term
+            (hol_identifier)
+            (hol_identifier)))))))
+
+
+============
+Composition
+============
+
+val _ = “a o b o c”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binary_term
+          (hol_identifier)
+          (hol_binary_term
+            (hol_identifier)
+            (hol_identifier)))))))
+
+
+============
+Parentheses
+============
+
+val _ = “(hello)”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_identifier)))))
+
+
+=====
+True
+=====
+
+val _ = “T”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_true)))))
+
+
+======
+False
+======
+
+val _ = “F”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_false)))))
+
+
+=======
+Forall
+=======
+
+val _ = “∀h t. P h t”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binder
+          (hol_bvar
+            (hol_alphanumeric))
+          (hol_bvar
+            (hol_alphanumeric))
+          (hol_application
+            (hol_application
+              (hol_identifier)
+              (hol_identifier))
+            (hol_identifier)))))))
+
+
+=============
+Forall ASCII
+=============
+
+val _ = “!h t. P h t”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binder
+          (hol_bvar
+            (hol_alphanumeric))
+          (hol_bvar
+            (hol_alphanumeric))
+          (hol_application
+            (hol_application
+              (hol_identifier)
+              (hol_identifier))
+            (hol_identifier)))))))
+
+
+===================
+Forall (Annotated)
+===================
+
+val _ = “∀x:num. T”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binder
+          (hol_bvar
+            (hol_alphanumeric)
+            (hol_atomic_type))
+          (hol_true))))))
+
+
+==================================
+Forall (Annotated, Parenthesized)
+==================================
+
+val _ = “∀(x:num). T”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binder
+          (hol_bvar
+            (hol_alphanumeric)
+            (hol_atomic_type))
+          (hol_true))))))
+
+
+============================
+Conjunction and Disjunction
+============================
+
+val _ = “T ∧ F ∨ T”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binary_term
+          (hol_binary_term
+            (hol_true)
+            (hol_false))
+          (hol_true))))))
+
+
+=======
+Lambda
+=======
+
+val _ = “λx. x + 1”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_binder
+          (hol_bvar
+            (hol_alphanumeric))
+          (hol_binary_term
+            (hol_identifier)
+            (hol_number)))))))
+
+
+====
+Not
+====
+
+val _ = “¬F”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_left_unary_term
+          (hol_false))))))
+
+
+==========
+Empty Set
+==========
+
+val _ = “{}”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_set)))))
+
+
+====
+Set
+====
+
+val _ = “{1; 2}”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_set
+          (hol_number)
+          (hol_number))))))
+
+
+================
+Type Annotation
+================
+
+val _ = “x:num”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_term
+        (hol_annotated
+          (hol_identifier)
+          (hol_atomic_type))))))
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/theorem.txt b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/theorem.txt
new file mode 100644
index 0000000000..61e1bc19e0
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/theorem.txt
@@ -0,0 +1,84 @@
+=============================
+Simple Theorem + Termination
+=============================
+
+Theorem foo:
+  ∀x. x = x
+Proof
+  gvs []
+QED
+
+---
+
+(source_file
+  (hol_theorem_with_proof
+    (hol_thmname)
+    (hol_thmstmt
+      (hol_binder
+        (hol_bvar
+          (hol_alphanumeric))
+        (hol_binary_term
+          (hol_identifier)
+          (hol_identifier))))
+    (tactic
+      (app_exp
+        (vid_exp
+          (longvid
+            (vid)))
+        (list_exp)))))
+
+
+=====
+THEN
+=====
+
+Theorem foo:
+  foo
+Proof
+  tac1 \\ tac2 \\ tac3
+QED
+
+---
+
+(source_file
+  (hol_theorem_with_proof
+    (hol_thmname)
+    (hol_thmstmt
+      (hol_identifier))
+    (tactic
+      (THEN
+        (vid_exp
+          (longvid
+            (vid)))
+        (vid_exp
+          (longvid
+            (vid)))
+        (vid_exp
+          (longvid
+            (vid)))))))
+
+
+==========
+Attribute
+==========
+
+Theorem foo[bar,foobar]:
+  T
+Proof
+  tac1
+QED
+
+---
+
+(source_file
+  (hol_theorem_with_proof
+    (hol_thmname)
+    (hol_attributes
+      (attribute)
+      (attribute))
+    (hol_thmstmt
+      (hol_true))
+    (tactic
+      (vid_exp
+          (longvid
+            (vid))))))
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/type.txt b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/type.txt
new file mode 100644
index 0000000000..9fe37f2ed8
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/test/corpus/type.txt
@@ -0,0 +1,53 @@
+====
+Num
+====
+
+val _ = “:num”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_type
+        (hol_atomic_type)))))
+
+
+==========
+List Type
+==========
+
+val _ = “:'a list”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_type
+        (hol_list_ty
+          (hol_atomic_type))))))
+
+
+==============
+Function Type
+==============
+
+val _ = “:'a -> ('a -> 'b) -> 'b”
+
+---
+
+(source_file
+  (val_dec
+    (valbind
+      (wildcard_pat)
+      (quoted_type
+        (hol_fun_ty
+          (hol_atomic_type)
+          (hol_fun_ty
+            (hol_fun_ty
+              (hol_atomic_type)
+              (hol_atomic_type))
+            (hol_atomic_type)))))))
diff --git a/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/tree-sitter.json b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/tree-sitter.json
new file mode 100644
index 0000000000..6948b10afe
--- /dev/null
+++ b/tools/editor-modes/emacs/tree-sitter/tree-sitter-holscript/tree-sitter.json
@@ -0,0 +1,33 @@
+{
+  "grammars": [
+    {
+      "name": "holscript",
+      "camelcase": "HOLScript",
+      "scope": "source.holscript",
+      "path": ".",
+      "file-types": null,
+      "injection-regex": "^holscript$"
+    }
+  ],
+  "metadata": {
+    "version": "0.1.0",
+    "license": "MIT",
+    "description": "HOLScript grammar for tree-sitter",
+    "authors": [
+      {
+        "name": "Daniel Nezamabadi"
+      }
+    ],
+    "links": {
+      "repository": "https://github.com/HOL-Theorem-Prover/HOL/"
+    }
+  },
+  "bindings": {
+    "c": true,
+    "go": true,
+    "node": true,
+    "python": true,
+    "rust": true,
+    "swift": true
+  }
+}
\ No newline at end of file