diff --git a/emacs/k-mode.el b/emacs/k-mode.el
index 84d179b..7645fc2 100644
--- a/emacs/k-mode.el
+++ b/emacs/k-mode.el
@@ -1,56 +1,57 @@
-;;; k-mode.el -- Emacs mode for the K Framework
-
-;; Currently has syntax highlighting for:
-;;  - keywords
-;;  - declarations (e.g. ops, syntax, etc)
-;;  - Quoted identifiers (e.g. for terminals in the syntax)
-;; Also has a menu and compilation through C-c C-c
+;;; k-mode.el --- Emacs mode for the K Framework  -*- lexical-binding: t; -*-
 
+;; Author: Rikard Hjort & Michael Ilseman
+;; Maintainer: Rikard Hjort <rikard.hjort@runtimeverification.com>
+;; Keywords: languages
+;; URL: https://github.com/kframework/k-editor-support
+;; Version: 0.2.0
+;; Package-Requires: ((emacs "25.1"))
 
-;; Author: Michael Ilseman
+;; This file is NOT part of GNU Emacs.
 
 ;; Usage: add the below to your .emacs file:
 ;;     (setq load-path (cons "path/to/this/file" load-path))
 ;;     (load-library "k-mode")
-;;     (add-to-list 'auto-mode-alist '("\\.k$" . k-mode)) ;; to launch k-mode for .k files
-(require 'comint)
+;; If you want to enable inline syntax highlighting in Markdown:
+;;     (use-package markdown-mode)
+;;     (push '("k" . k-mode) markdown-code-lang-modes) ;; Use C-c C-x C-f to turn on highlighting on and off.
+
+;;; Commentary:
+;;
+;; Currently has syntax highlighting for:
+;;  - keywords
+;;  - cells and rewrites
+;;  - comments
+;;  - declarations (e.g. ops, syntax, etc)
+;;  - quoted identifiers (e.g. for terminals in the syntax)
+;;  - annotations
+;;  - matching-logic symbols
+;;  - custom highlights through user-controlled variables
+;; Also has a menu and compilation through C-c C-c
+
+;;; Code:
 
 ;;;; Options ;;;;
 (defvar k-dash-comments nil
-  "Set to make \"--\" be used as a beginning of a line comment
-   (emacs's syntax table is unable to differentiate 3 character long comment beginners)"
-)
-(defvar k-path "~/k-framework"
-  "Path to the k-framework. Set if you wish to use kompile from emacs. Defaults to ~/k-framework.
-   Currently doesn't do anything."
-)
+  "Set to make \"--\" be used as a beginning of a line comment (emacs's syntax table is unable to differentiate 3 character long comment beginners).")
+
+(defvar k-custom-word-highlights nil
+  "A list of words to highlight, beyond the builtin syntax. For example \"'(\"andBool\" \"orBool\" \"+Int\")\".")
+
+(defvar k-custom-highlights-regex nil
+  "A list of words to highlight, beyond the builtin syntax. For example \"<-\\|\\|->\".")
 
 ;;;; Syntax Highlighting ;;;;
-(setq k-keywords
-      '("syntax" "kmod" "endkm" "including" ; "::=" "|"
-        "sort" "op" "subsort" "rule" "eq" "ceq" "load")
-      k-syntax-terminals-regex
-      "`\\w+"
-      k-declarations ;; Syntax highlight the name after a declaration
-      "\\(syntax\\|sort\\|op\\) \\([a-zA-Z{}\\-]+\\)"
-)
-
-;; Set up the regexes
-(setq k-keywords-regex
-      (regexp-opt k-keywords 'words)
-)
-
-;; Put them all together
-(setq k-font-lock-keywords
-      `((,k-declarations 2 font-lock-builtin-face)
-        (,k-keywords-regex . font-lock-keyword-face)
-        (,k-syntax-terminals-regex . font-lock-constant-face)
-       )
-)
+(defvar k-keywords '("configuration" "context" "endmodule" "non-assoc" "ensures" "imports" "left" "module" "priorities" "require" "requires" "right" "rule" "sort" "syntax" "when"))
+
+;; TODO: Only highlight these when inside square brackets.
+(defvar k-annotations '("alias" "alias-rec" "anywhere" "bracket" "concrete" "context" "cool" "freshGenerator" "function" "functional" "heat" "hook" "hybrid" "klabel" "left" "macro" "macro-rec" "memo" "owise" "priority" "result" "right" "seqstrict" "simplification" "smtlib" "strict" "symbol" "token" "unboundVariables"))
 
 ;; Handle comments
-(defun set-comment-highlighting ()
-  "Set up comment highlighting"
+(defvar k-mode-syntax-table (make-syntax-table) "Syntax table for `k-mode'.")
+
+(defun k-set-comment-highlighting ()
+  "Set up comment highlighting."
 
   ;; comment style "// ..." and "/* ... */"
   (modify-syntax-entry ?\/ ". 124b" k-mode-syntax-table)
@@ -58,39 +59,19 @@
   (modify-syntax-entry ?* ". 23" k-mode-syntax-table)
 
   ;; comment style "-- ..."
-  (if k-dash-comments (modify-syntax-entry ?- ". 1b2b" k-mode-syntax-table))
-)
-
+  (if k-dash-comments (modify-syntax-entry ?- ". 1b2b" k-mode-syntax-table)))
 
 ;;;; K Bindings and menu ;;;;
 (defvar k-prev-load-file nil
-  "Record the last directory and file used in loading or compiling"
-)
-(defcustom k-source-modes '(k-mode)
-  "Determine if a buffer represents a k file"
-)
-;; (defun k-mode-kompile (cmd)
-;;   ;; (interactive (comint-get-source "Kompile k file: " k-prev-load-file k-source-modes nil))
-;;   ;; (comint-check-source file-name) ; check to see if buffer has been modified and not saved
-;;   ;; (setq k-prev-load-file (cons (file-name-directory file-name)
-;;   ;;                              (file-name-nondirectory file-name)))
-;;   ;; ;; (comint-send-string (inferior-lisp-proc)
-;; 	;; ;; 	      (format inferior-lisp-load-command file-name))
-;;   ;; ;; (switch-to-lisp t))
-;;   ;; (message file-name)
-;;   ;; (setq kompile-buffer (make-comint "Kompile" "zsh" nil))
-;;   ;; (comint-send-string kompile-buffer "cd" nil (file-name-directory file-name))
-;;   ;; (comint-send-string kompile-buffer "~/k-framework/tools/kompile.pl" nil (file-name-nondirectory file-name))
-;;   (interactive "scmd")
-;;   (compile cmd)
-;;   nil
-;; )
+  "Record the last directory and file used in loading or compiling.")
+
 (defun k-mode-about ()
+  "Show package info."
   (interactive)
-  (message "k-mode for the K Framework")
-)
+  (message "k-mode for the K Framework"))
 
-(defun setup-k-mode-map ()
+(defun k-setup-k-mode-map ()
+  "Set up keyboard mapping for compilation."
   (setq k-mode-map (make-sparse-keymap))
 
   ;; Keyboard shortcuts
@@ -108,8 +89,7 @@
     (define-key menuMap [separator]
       '("--"))
     (define-key menuMap [kompile]
-      '("kompile" . compile)))
-)
+      '("kompile" . compile))))
 
 
 
@@ -117,20 +97,53 @@
 
 ;;;; K Mode ;;;;
 
+;;;###autoload
 (define-derived-mode k-mode fundamental-mode
   "k mode"
   "Major Mode for the K framwork"
+
+  ;; Set up the regexes
+
+  ;; Metalanguage.
+  (setq k-keywords-regex (regexp-opt k-keywords 'words)
+        k-annotations-regex (regexp-opt k-annotations 'symbols)
+        k-keywords-special-regex "::=\\||"
+        k-declarations "\\(syntax\\|sort\\|op\\) +\\(\\({.+} +\\)?[a-zA-Z{}\\-]+\\)"
+        k-rewrites-regex "=>\\|<[^>*/|\"_[:space:]]+>\\|</[^>*/|\"_[:space:]]+>\\|<[^>*/|\"_[:space:]]+/>")
+
+  ;; Common constructs.
+  (setq k-syntax-terminals-regex "\\.\\.\\.\\|~>\\||->\\|\\.\\s-\\|`\\w+"
+        k-custom-word-highlights-regex (regexp-opt k-custom-word-highlights 'words)
+        k-hash-symbols-regex "\\(#\\(?:And\\|Ceil\\|E\\(?:\\(?:qual\\|xist\\)s\\)\\|False\\|Not\\|Or\\|True\\|as\\|else\\|f\\(?:i\\|un\\)\\|if\\|then\\)\\)\\b")
+
+  ;; Put them all together
+  (setq k-font-lock-keywords
+        `((,k-custom-word-highlights-regex . font-lock-constant-face)
+          (,k-custom-highlights-regex      . font-lock-constant-face)
+          (,k-rewrites-regex               . font-lock-type-face)
+          (,k-syntax-terminals-regex       . font-lock-constant-face)
+          (,k-hash-symbols-regex           . font-lock-constant-face)
+          (,k-declarations                 2 font-lock-function-name-face)
+          (,k-keywords-regex               . font-lock-keyword-face)
+          (,k-keywords-special-regex       . font-lock-keyword-face)
+          (,k-annotations-regex            . font-lock-builtin-face)))
+
+
   (setq font-lock-defaults '((k-font-lock-keywords)))
 
   ;; Comment entries
-  (set-comment-highlighting)
+  (k-set-comment-highlighting)
+
+  ;; Set comment start characters
+  (setq comment-start "//")
 
   ;; Shortcuts and menu
-  (setup-k-mode-map)
-  (use-local-map k-mode-map)
+  (k-setup-k-mode-map)
+  (use-local-map k-mode-map))
 
-  ;; Clear up memory
-  ;;(setq k-keywords nil k-keywords-regex nil)
-)
+;;;###autoload
+(add-to-list 'auto-mode-alist '("\\.k$" . k-mode))
 
 (provide 'k-mode)
+
+;;; k-mode.el ends here
diff --git a/spacemacs/README.md b/spacemacs/README.md
new file mode 100644
index 0000000..247b5e1
--- /dev/null
+++ b/spacemacs/README.md
@@ -0,0 +1,42 @@
+K Spacemacs Layer
+=================
+
+This layer provides syntax highlighting for the K framework.
+It includes support for highlighting code blocks within Markdown files.
+
+Key Bindings and Commands
+=========================
+
+| Key                | Function                       |
+|--------------------|--------------------------------|
+| <kbd>SPC m c</kbd> | Compile with a custom command. |
+
+Installation
+============
+
+```sh
+git clone https://github.com/k-editor-support/
+ln -s $(pwd)/k-editor-support/spacemacs/k-framework $HOME/.emacs.d/private/local
+```
+
+Add `k-framework` to the list `dotspacemacs-configuration-layers` in your spacemacs config.
+
+Customization
+=============
+
+You can set variables for customizing the layer in.
+In the `dotspacemacs-configuration-layers` list, you can declare custom variables as follows.
+
+```elisp
+(k-framework :variables k-custom-word-highlights '("andBool" "orBool" "notBool") k-custom-highlights-regex "<-\\|\\|->")
+```
+
+| Variable                    | Use                                                       |
+|-----------------------------|-----------------------------------------------------------|
+| `k-custom-word-highlights`  | Any extra words you want highlighted.                     |
+| `k-custom-highlights-regex` | For more fine-grained control of your custom highlights.  |
+
+Updating
+========
+
+This tutorial is used as reference for updating the syntax highlighting: <http://ergoemacs.org/emacs/elisp_syntax_coloring.html>
diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
new file mode 120000
index 0000000..1597b2d
--- /dev/null
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -0,0 +1 @@
+emacs/k-mode.el
\ No newline at end of file
diff --git a/spacemacs/k-framework/packages.el b/spacemacs/k-framework/packages.el
new file mode 100644
index 0000000..cdf436f
--- /dev/null
+++ b/spacemacs/k-framework/packages.el
@@ -0,0 +1,26 @@
+;;; packages.el --- k-framework layer packages file for Spacemacs.
+
+(setq k-framework-packages
+  '(
+    (k-mode :location local)
+    markdown-mode
+   )
+)
+
+(defun k-framework/init-k-mode ()
+  (use-package k-mode
+    :defer t
+    :mode "\\.k\\'"
+  )
+)
+
+(defun k-framework/post-init-markdown-mode ()
+  (use-package markdown-mode)
+  (push '("k" . k-mode) markdown-code-lang-modes)
+)
+
+(defun k-framework/post-init-k-mode ()
+  (spacemacs/set-leader-keys-for-major-mode 'k-mode
+    "c" 'compile
+    )
+)