From acf6d48553a15b9440ddd3b29367834d3e06d5f1 Mon Sep 17 00:00:00 2001
From: David Christiansen <david@davidchristiansen.dk>
Date: Mon, 25 Jul 2016 09:29:07 -0400
Subject: [PATCH] Add subprocess to Emacs mode

The Emacs mode for cubical can now run cubical as a subprocess. The
keybinding "C-c C-l", which is the same as Agda and Idris, saves the
current buffer and loads it in cubical.

Additionally, a Customize setting is added to allow users to easily
customize the command to be used to invoke cubical.
---
 README.md    |  6 ++++++
 cubicaltt.el | 50 ++++++++++++++++++++++++++++++++++++++++++++++++--
 2 files changed, 54 insertions(+), 2 deletions(-)

diff --git a/README.md b/README.md
index bc42a30..20121cf 100644
--- a/README.md
+++ b/README.md
@@ -99,6 +99,12 @@ on emacs' ```load-path```, or else load it in advance, either manually with
 (load-file "cubicaltt.el")
 ```
 
+When using `ctt-mode` in Emacs, the command `ctt-load` will launch the
+interactive toplevel in an Emacs buffer and load the current file. It
+is bound to `C-c C-l` by default. If `cubical` is not on Emacs's
+`exec-path`, then set the variable `ctt-command` to the command that
+runs it.
+
 References and notes
 --------------------
 
diff --git a/cubicaltt.el b/cubicaltt.el
index 23923fe..d7665c5 100644
--- a/cubicaltt.el
+++ b/cubicaltt.el
@@ -42,6 +42,52 @@
        (modify-syntax-entry ?\n ">" st)
    st))
 
+
+(defgroup ctt nil "Options for ctt-mode for cubical type theory" :group 'languages)
+
+(defcustom ctt-command "cubical"
+  "The command to be run for cubical."
+  :group 'ctt
+  :type 'string
+  :options '("cubical" "cabal exec cubical"))
+
+(defvar *ctt-cubical-process* nil
+  "The subprocess buffer for cubical.")
+
+(defvar *ctt-loaded-buffer* nil
+  "The currently-loaded buffer for cubical.
+
+If no buffer is loaded, then this variable is nil.")
+
+
+(defun ctt-ensure-process ()
+  "Ensure that a process is running for cubical and return the process buffer."
+  (if (and *ctt-cubical-process* (get-buffer-process *ctt-cubical-process*))
+      *ctt-cubical-process*
+    (let ((process (make-comint "cubical" ctt-command)))
+      (setq *ctt-cubical-process* process)
+      process)))
+
+
+(defun ctt-load ()
+  "Start cubical if it is not running, and get the current buffer loaded."
+  (interactive)
+  (let ((file (buffer-file-name)))
+    (unless file
+      (error "The current buffer is not associated with a file"))
+    (let ((cubical-proc (ctt-ensure-process))
+          (dir (file-name-directory file))
+          (f (file-name-nondirectory file)))
+      (save-buffer)
+      ;; Get in the right working directory. No space-escaping is
+      ;; necessary for cubical.
+      (comint-send-string *ctt-cubical-process* (concat ":cd " dir "\n"))
+      ;; Load the file
+      (comint-send-string *ctt-cubical-process* (concat ":l " f "\n"))
+      ;; Show the buffer
+      (pop-to-buffer *ctt-cubical-process* '(display-buffer-use-some-window (inhibit-same-window . t))))))
+
+
 ;; define the mode
 (define-derived-mode ctt-mode fundamental-mode
   "ctt mode"
@@ -55,11 +101,11 @@
 
   ;; modify the keymap
   (define-key ctt-mode-map [remap comment-dwim] 'ctt-comment-dwim)
+  (define-key ctt-mode-map (kbd "C-c C-l") 'ctt-load)
 
   ;; clear memory
   (setq ctt-keywords-regexp nil)
   (setq ctt-operators-regexp nil)
-  (setq ctt-special-regexp nil)
-)
+  (setq ctt-special-regexp nil))
 
 (provide 'ctt-mode)
-- 
2.34.1