From 1ea70dc47bc23b0aca5faf4d9cd9a344c2f21401 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 13:57:58 +0200
Subject: [PATCH 01/14] Add spacemacs layer

---
 spacemacs/README.md                          |  43 ++++++
 spacemacs/k-framework/local/k-mode/k-mode.el | 142 +++++++++++++++++++
 spacemacs/k-framework/packages.el            |  26 ++++
 3 files changed, 211 insertions(+)
 create mode 100644 spacemacs/README.md
 create mode 100644 spacemacs/k-framework/local/k-mode/k-mode.el
 create mode 100644 spacemacs/k-framework/packages.el

diff --git a/spacemacs/README.md b/spacemacs/README.md
new file mode 100644
index 0000000..9ef1c0f
--- /dev/null
+++ b/spacemacs/README.md
@@ -0,0 +1,43 @@
+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/
+cd k-spacemacs-layer 
+mv 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 100644
index 0000000..22ba262
--- /dev/null
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -0,0 +1,142 @@
+;;; k-mode.el -- Emacs mode for the K Framework
+
+;; 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
+;; 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.
+
+;; 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
+
+;; Authors: Michael Ilseman & Rikard Hjort
+
+(require 'comint)
+
+;;;; 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-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 '("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.
+(setq 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"))
+
+;; 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)))
+
+;; Handle comments
+(defun set-comment-highlighting ()
+  "Set up comment highlighting"
+
+  ;; comment style "// ..." and "/* ... */"
+  (modify-syntax-entry ?\/ ". 124b" k-mode-syntax-table)
+  (modify-syntax-entry ?\n "> b" k-mode-syntax-table)
+  (modify-syntax-entry ?* ". 23" k-mode-syntax-table)
+
+  ;; comment style "-- ..."
+  (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-about ()
+  (interactive)
+  (message "k-mode for the K Framework")
+)
+
+(defun setup-k-mode-map ()
+  (setq k-mode-map (make-sparse-keymap))
+
+  ;; Keyboard shortcuts
+  (define-key k-mode-map (kbd "C-c C-c") 'compile)
+
+  ;; Define the menu
+  (define-key k-mode-map [menu-bar] (make-sparse-keymap))
+
+  (let ((menuMap (make-sparse-keymap "K Framework")))
+    (define-key k-mode-map [menu-bar k] (cons "K Framework" menuMap))
+    (define-key menuMap [about]
+      '("About k-mode" . k-mode-about))
+    ;; (define-key menuMap [customize]
+    ;;   '("Customize k-mode" . k-customize))
+    (define-key menuMap [separator]
+      '("--"))
+    (define-key menuMap [kompile]
+      '("kompile" . compile)))
+)
+
+
+
+
+
+;;;; K Mode ;;;;
+
+(define-derived-mode k-mode fundamental-mode
+  "k mode"
+  "Major Mode for the K framwork"
+  (setq font-lock-defaults '((k-font-lock-keywords)))
+
+  ;; Comment entries
+  (set-comment-highlighting)
+
+  ;; Set comment start characters
+  (setq comment-start "//")
+
+  ;; Shortcuts and menu
+  (setup-k-mode-map)
+  (use-local-map k-mode-map)
+)
+
+(provide 'k-mode)
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
+    )
+)

From 4cdb9967f60ec3e787258d6d052621286dfe8f5c Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 14:02:37 +0200
Subject: [PATCH 02/14] Use updated k-mode for spacemacs for regular emacs as
 well

---
 emacs/k-mode.el | 137 +-----------------------------------------------
 1 file changed, 1 insertion(+), 136 deletions(-)
 mode change 100644 => 120000 emacs/k-mode.el

diff --git a/emacs/k-mode.el b/emacs/k-mode.el
deleted file mode 100644
index 84d179b..0000000
--- a/emacs/k-mode.el
+++ /dev/null
@@ -1,136 +0,0 @@
-;;; 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
-
-
-;; Author: Michael Ilseman
-
-;; 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)
-
-;;;; 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."
-)
-
-;;;; 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)
-       )
-)
-
-;; Handle comments
-(defun set-comment-highlighting ()
-  "Set up comment highlighting"
-
-  ;; comment style "// ..." and "/* ... */"
-  (modify-syntax-entry ?\/ ". 124b" k-mode-syntax-table)
-  (modify-syntax-entry ?\n "> b" k-mode-syntax-table)
-  (modify-syntax-entry ?* ". 23" k-mode-syntax-table)
-
-  ;; comment style "-- ..."
-  (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
-;; )
-(defun k-mode-about ()
-  (interactive)
-  (message "k-mode for the K Framework")
-)
-
-(defun setup-k-mode-map ()
-  (setq k-mode-map (make-sparse-keymap))
-
-  ;; Keyboard shortcuts
-  (define-key k-mode-map (kbd "C-c C-c") 'compile)
-
-  ;; Define the menu
-  (define-key k-mode-map [menu-bar] (make-sparse-keymap))
-
-  (let ((menuMap (make-sparse-keymap "K Framework")))
-    (define-key k-mode-map [menu-bar k] (cons "K Framework" menuMap))
-    (define-key menuMap [about]
-      '("About k-mode" . k-mode-about))
-    ;; (define-key menuMap [customize]
-    ;;   '("Customize k-mode" . k-customize))
-    (define-key menuMap [separator]
-      '("--"))
-    (define-key menuMap [kompile]
-      '("kompile" . compile)))
-)
-
-
-
-
-
-;;;; K Mode ;;;;
-
-(define-derived-mode k-mode fundamental-mode
-  "k mode"
-  "Major Mode for the K framwork"
-  (setq font-lock-defaults '((k-font-lock-keywords)))
-
-  ;; Comment entries
-  (set-comment-highlighting)
-
-  ;; Shortcuts and menu
-  (setup-k-mode-map)
-  (use-local-map k-mode-map)
-
-  ;; Clear up memory
-  ;;(setq k-keywords nil k-keywords-regex nil)
-)
-
-(provide 'k-mode)
diff --git a/emacs/k-mode.el b/emacs/k-mode.el
new file mode 120000
index 0000000..1317093
--- /dev/null
+++ b/emacs/k-mode.el
@@ -0,0 +1 @@
+spacemacs/k-framework/local/k-mode/k-mode.el
\ No newline at end of file

From 611dad3c3842fc53434808963b264167c2c740bf Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 14:32:23 +0200
Subject: [PATCH 03/14] Marmalade package format for MELPA support

Based on this:
https://github.com/kframework/k-editor-support/pull/6/files
---
 spacemacs/k-framework/local/k-mode/k-mode.el | 20 ++++++++++++++++++--
 1 file changed, 18 insertions(+), 2 deletions(-)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index 22ba262..f4b2854 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -1,4 +1,11 @@
-;;; k-mode.el -- Emacs mode for the K Framework
+;;; 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
+;; Version: 0.2.0
+
+;; 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))
@@ -8,6 +15,8 @@
 ;;     (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
@@ -19,10 +28,11 @@
 ;;  - custom highlights through user-controlled variables
 ;; Also has a menu and compilation through C-c C-c
 
-;; Authors: Michael Ilseman & Rikard Hjort
 
 (require 'comint)
 
+;;; Code:
+
 ;;;; Options ;;;;
 (defvar k-dash-comments nil
   "Set to make \"--\" be used as a beginning of a line comment
@@ -123,6 +133,7 @@
 
 ;;;; K Mode ;;;;
 
+;;;###autoload
 (define-derived-mode k-mode fundamental-mode
   "k mode"
   "Major Mode for the K framwork"
@@ -139,4 +150,9 @@
   (use-local-map k-mode-map)
 )
 
+;;;###autoload
+(add-to-list 'auto-mode-alist '("\\.k$" . k-mode))
+
 (provide 'k-mode)
+
+;;; k-mode.el ends here

From cf47ea94dea817043c22201ed41f07c6688d84c8 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 14:32:57 +0200
Subject: [PATCH 04/14] Remove unnecessary comment

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 1 -
 1 file changed, 1 deletion(-)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index f4b2854..31c51de 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -10,7 +10,6 @@
 ;; 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
 ;; 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.

From d48511e66a20418ebf29abdc0c376d653d76ac1d Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 14:52:06 +0200
Subject: [PATCH 05/14] Address `checkdoc` issues

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index 31c51de..e30e49f 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -34,16 +34,15 @@
 
 ;;;; 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)"
+  "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\")\""
+  "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 \"<-\\|\\|->\""
+  "A list of words to highlight, beyond the builtin syntax. For example \"<-\\|\\|->\"."
   )
 
 ;;;; Syntax Highlighting ;;;;
@@ -81,7 +80,7 @@
 
 ;; Handle comments
 (defun set-comment-highlighting ()
-  "Set up comment highlighting"
+  "Set up comment highlighting."
 
   ;; comment style "// ..." and "/* ... */"
   (modify-syntax-entry ?\/ ". 124b" k-mode-syntax-table)
@@ -94,18 +93,20 @@
 
 ;;;; K Bindings and menu ;;;;
 (defvar k-prev-load-file nil
-  "Record the last directory and file used in loading or compiling"
+  "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"
+  "Determine if a buffer represents a k file."
 )
 
 (defun k-mode-about ()
+  "Show package info."
   (interactive)
   (message "k-mode for the K Framework")
 )
 
 (defun setup-k-mode-map ()
+  "Set up keyboard mapping for compilation."
   (setq k-mode-map (make-sparse-keymap))
 
   ;; Keyboard shortcuts

From 925f45ac501ae5d972bf011beb7a7e8eea931d35 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 16:15:52 +0200
Subject: [PATCH 06/14] Handle compile warnings

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 64 +++++++++++---------
 1 file changed, 34 insertions(+), 30 deletions(-)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index e30e49f..758e62b 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -46,37 +46,10 @@
   )
 
 ;;;; Syntax Highlighting ;;;;
-(setq k-keywords '("configuration" "context" "endmodule" "non-assoc" "ensures" "imports" "left" "module" "priorities" "require" "requires" "right" "rule" "sort" "syntax" "when"))
+(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.
-(setq 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"))
-
-;; 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)))
+(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 ()
@@ -137,6 +110,35 @@
 (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
@@ -148,7 +150,9 @@
   ;; Shortcuts and menu
   (setup-k-mode-map)
   (use-local-map k-mode-map)
-)
+
+  (setq k-keywords nil k-annotations nil)
+  )
 
 ;;;###autoload
 (add-to-list 'auto-mode-alist '("\\.k$" . k-mode))

From a9b5411bc2fd18dda1604ed41db6755cf9a36ce4 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 17:31:48 +0200
Subject: [PATCH 07/14] Remove unnecessary code

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index 758e62b..378ab9e 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -68,9 +68,6 @@
 (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-about ()
   "Show package info."
@@ -151,7 +148,6 @@
   (setup-k-mode-map)
   (use-local-map k-mode-map)
 
-  (setq k-keywords nil k-annotations nil)
   )
 
 ;;;###autoload

From f63b91486a6065e3a9293ab7448833ccbcb1f9a2 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 17:32:15 +0200
Subject: [PATCH 08/14] Specify syntax table variable

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index 378ab9e..4770119 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -52,6 +52,8 @@
 (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
+(defvar k-mode-syntax-table (make-syntax-table) "Syntax table for `k-mode'.")
+
 (defun set-comment-highlighting ()
   "Set up comment highlighting."
 

From 120aca48540c972dda3ba83a33f2db928278454d Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 18:03:58 +0200
Subject: [PATCH 09/14] Package documentation

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index 4770119..f1757b1 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -3,7 +3,9 @@
 ;; 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"))
 
 ;; This file is NOT part of GNU Emacs.
 

From ce637237cdf08724db5f1011e8bbb482fb2cafa8 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 18:04:59 +0200
Subject: [PATCH 10/14] Remove unused import

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index f1757b1..d2b61e3 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -29,9 +29,6 @@
 ;;  - custom highlights through user-controlled variables
 ;; Also has a menu and compilation through C-c C-c
 
-
-(require 'comint)
-
 ;;; Code:
 
 ;;;; Options ;;;;

From bffcf9cbac7a09bc96025086b8fe4d10ecc3d4d8 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Tue, 7 Jul 2020 18:11:40 +0200
Subject: [PATCH 11/14] Address package-lint issues

---
 spacemacs/k-framework/local/k-mode/k-mode.el | 38 ++++++++------------
 1 file changed, 14 insertions(+), 24 deletions(-)

diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
index d2b61e3..7645fc2 100644
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ b/spacemacs/k-framework/local/k-mode/k-mode.el
@@ -1,4 +1,4 @@
-;;; k-mode.el -- Emacs mode for the K Framework  -*- lexical-binding: t; -*-
+;;; k-mode.el --- Emacs mode for the K Framework  -*- lexical-binding: t; -*-
 
 ;; Author: Rikard Hjort & Michael Ilseman
 ;; Maintainer: Rikard Hjort <rikard.hjort@runtimeverification.com>
@@ -33,16 +33,13 @@
 
 ;;;; 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)."
-)
+  "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\")\"."
-  )
+  "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 \"<-\\|\\|->\"."
-  )
+  "A list of words to highlight, beyond the builtin syntax. For example \"<-\\|\\|->\".")
 
 ;;;; Syntax Highlighting ;;;;
 (defvar k-keywords '("configuration" "context" "endmodule" "non-assoc" "ensures" "imports" "left" "module" "priorities" "require" "requires" "right" "rule" "sort" "syntax" "when"))
@@ -53,7 +50,7 @@
 ;; Handle comments
 (defvar k-mode-syntax-table (make-syntax-table) "Syntax table for `k-mode'.")
 
-(defun set-comment-highlighting ()
+(defun k-set-comment-highlighting ()
   "Set up comment highlighting."
 
   ;; comment style "// ..." and "/* ... */"
@@ -62,21 +59,18 @@
   (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."
-)
+  "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))
 
@@ -95,8 +89,7 @@
     (define-key menuMap [separator]
       '("--"))
     (define-key menuMap [kompile]
-      '("kompile" . compile)))
-)
+      '("kompile" . compile))))
 
 
 
@@ -121,8 +114,7 @@
   ;; 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"
-        )
+        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
@@ -140,16 +132,14 @@
   (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))
 
 ;;;###autoload
 (add-to-list 'auto-mode-alist '("\\.k$" . k-mode))

From 712ba30245ab030bc1814a680cfd6d300d3b95b2 Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Wed, 8 Jul 2020 17:28:44 +0200
Subject: [PATCH 12/14] Update README

---
 spacemacs/README.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/spacemacs/README.md b/spacemacs/README.md
index 9ef1c0f..62e3dda 100644
--- a/spacemacs/README.md
+++ b/spacemacs/README.md
@@ -16,8 +16,7 @@ Installation
 
 ```sh
 git clone https://github.com/k-editor-support/
-cd k-spacemacs-layer 
-mv k-editor-support/spacemacs/k-framework $HOME/.emacs.d/private/local
+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.

From c52fb6b702db6c6aa59a94a28dfd639f2f0aca6e Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Wed, 8 Jul 2020 17:34:52 +0200
Subject: [PATCH 13/14] Have spacemacs depend on emacs instead of other way
 around

---
 emacs/k-mode.el                              | 150 ++++++++++++++++++-
 spacemacs/k-framework/local/k-mode/k-mode.el | 150 +------------------
 2 files changed, 150 insertions(+), 150 deletions(-)
 mode change 120000 => 100644 emacs/k-mode.el
 mode change 100644 => 120000 spacemacs/k-framework/local/k-mode/k-mode.el

diff --git a/emacs/k-mode.el b/emacs/k-mode.el
deleted file mode 120000
index 1317093..0000000
--- a/emacs/k-mode.el
+++ /dev/null
@@ -1 +0,0 @@
-spacemacs/k-framework/local/k-mode/k-mode.el
\ No newline at end of file
diff --git a/emacs/k-mode.el b/emacs/k-mode.el
new file mode 100644
index 0000000..7645fc2
--- /dev/null
+++ b/emacs/k-mode.el
@@ -0,0 +1,149 @@
+;;; 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"))
+
+;; 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")
+;; 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-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 ;;;;
+(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
+(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)
+  (modify-syntax-entry ?\n "> b" k-mode-syntax-table)
+  (modify-syntax-entry ?* ". 23" k-mode-syntax-table)
+
+  ;; comment style "-- ..."
+  (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.")
+
+(defun k-mode-about ()
+  "Show package info."
+  (interactive)
+  (message "k-mode for the K Framework"))
+
+(defun k-setup-k-mode-map ()
+  "Set up keyboard mapping for compilation."
+  (setq k-mode-map (make-sparse-keymap))
+
+  ;; Keyboard shortcuts
+  (define-key k-mode-map (kbd "C-c C-c") 'compile)
+
+  ;; Define the menu
+  (define-key k-mode-map [menu-bar] (make-sparse-keymap))
+
+  (let ((menuMap (make-sparse-keymap "K Framework")))
+    (define-key k-mode-map [menu-bar k] (cons "K Framework" menuMap))
+    (define-key menuMap [about]
+      '("About k-mode" . k-mode-about))
+    ;; (define-key menuMap [customize]
+    ;;   '("Customize k-mode" . k-customize))
+    (define-key menuMap [separator]
+      '("--"))
+    (define-key menuMap [kompile]
+      '("kompile" . compile))))
+
+
+
+
+
+;;;; 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
+  (k-set-comment-highlighting)
+
+  ;; Set comment start characters
+  (setq comment-start "//")
+
+  ;; Shortcuts and menu
+  (k-setup-k-mode-map)
+  (use-local-map k-mode-map))
+
+;;;###autoload
+(add-to-list 'auto-mode-alist '("\\.k$" . k-mode))
+
+(provide 'k-mode)
+
+;;; k-mode.el ends here
diff --git a/spacemacs/k-framework/local/k-mode/k-mode.el b/spacemacs/k-framework/local/k-mode/k-mode.el
deleted file mode 100644
index 7645fc2..0000000
--- a/spacemacs/k-framework/local/k-mode/k-mode.el
+++ /dev/null
@@ -1,149 +0,0 @@
-;;; 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"))
-
-;; 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")
-;; 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-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 ;;;;
-(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
-(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)
-  (modify-syntax-entry ?\n "> b" k-mode-syntax-table)
-  (modify-syntax-entry ?* ". 23" k-mode-syntax-table)
-
-  ;; comment style "-- ..."
-  (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.")
-
-(defun k-mode-about ()
-  "Show package info."
-  (interactive)
-  (message "k-mode for the K Framework"))
-
-(defun k-setup-k-mode-map ()
-  "Set up keyboard mapping for compilation."
-  (setq k-mode-map (make-sparse-keymap))
-
-  ;; Keyboard shortcuts
-  (define-key k-mode-map (kbd "C-c C-c") 'compile)
-
-  ;; Define the menu
-  (define-key k-mode-map [menu-bar] (make-sparse-keymap))
-
-  (let ((menuMap (make-sparse-keymap "K Framework")))
-    (define-key k-mode-map [menu-bar k] (cons "K Framework" menuMap))
-    (define-key menuMap [about]
-      '("About k-mode" . k-mode-about))
-    ;; (define-key menuMap [customize]
-    ;;   '("Customize k-mode" . k-customize))
-    (define-key menuMap [separator]
-      '("--"))
-    (define-key menuMap [kompile]
-      '("kompile" . compile))))
-
-
-
-
-
-;;;; 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
-  (k-set-comment-highlighting)
-
-  ;; Set comment start characters
-  (setq comment-start "//")
-
-  ;; Shortcuts and menu
-  (k-setup-k-mode-map)
-  (use-local-map k-mode-map))
-
-;;;###autoload
-(add-to-list 'auto-mode-alist '("\\.k$" . k-mode))
-
-(provide 'k-mode)
-
-;;; k-mode.el ends here
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

From 88f5b7d3a2603a94f475f5e54c0ffb175bfe584b Mon Sep 17 00:00:00 2001
From: hjorthjort <rikard.hjort@gmail.com>
Date: Wed, 8 Jul 2020 17:36:31 +0200
Subject: [PATCH 14/14] Update README

---
 spacemacs/README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/spacemacs/README.md b/spacemacs/README.md
index 62e3dda..247b5e1 100644
--- a/spacemacs/README.md
+++ b/spacemacs/README.md
@@ -16,7 +16,7 @@ Installation
 
 ```sh
 git clone https://github.com/k-editor-support/
-ln -s $(pwd)k-editor-support/spacemacs/k-framework $HOME/.emacs.d/private/local
+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.