diff options
Diffstat (limited to 'ob-acl2.el')
-rw-r--r-- | ob-acl2.el | 55 |
1 files changed, 55 insertions, 0 deletions
diff --git a/ob-acl2.el b/ob-acl2.el new file mode 100644 index 0000000..f57b17b --- /dev/null +++ b/ob-acl2.el @@ -0,0 +1,55 @@ +;;; ob-acl2.el --- org-babel functions for ACL2 + +;; Copyright (C) Masaya Tojo <masaya@tojo.tokyo> + +;; Author: Masaya Tojo +;; Keywords: literate programming, reproducible research +;; Homepage: https://git.tojo.tokyo/ob-acl2.git +;; Version: 0.01 + +;;; License: + +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation; either version 3, or (at your option) +;; any later version. +;; +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. +;; +;; You should have received a copy of the GNU General Public License +;; along with GNU Emacs. If not, see <https://www.gnu.org/licenses/>. + +;;; Commentary: + +;; This is implemented by pouring expressions into a *shell* buffer, which is a standard ACL2 execution environment. Please run acl2 with *shell* before using it. + + +;;; Code: +(require 'ob) + +(defun org-babel-acl2-clean-prompt (string) + (string-join (butlast (split-string string "\n")) "\n")) + +(defun org-babel-execute:acl2 (body params) + (let ((full-body (org-babel-expand-body:generic body params)) + ;;; XXX: I'm using *shell* for now. + (session (get-buffer "*shell*")) + (pt (lambda () + (marker-position + (process-mark (get-buffer-process (current-buffer))))))) + (org-babel-acl2-clean-prompt + (org-babel-comint-in-buffer session + (let ((start (funcall pt))) + (with-temp-buffer + (insert full-body) + (comint-send-region session (point-min) (point-max)) + (comint-send-string session "\n")) + (while (equal start (funcall pt)) (sleep-for 0.1)) + (buffer-substring start (funcall pt))))))) + +(provide 'ob-acl2) + +;;; ob-acl2.el ends here |