blob: f57b17b917acad2651075cd3ec7c7200b76e63c5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
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
|
