blob: 6ce20ab24db720fdf2e0f939a4931ef088dc54f2 (
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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
|
;;; ob-acl2.el --- org-babel functions for ACL2
;; Copyright (C) Masaya Tojo <masaya@tojo.tokyo>
;; Author: Masaya Tojo
;; Keywords: literate programming
;; Homepage: https://git.tojo.tokyo/ob-acl2.git
;; Version: 0.1.0
;;; 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.
;; Must 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: Using *shell* for now.
(session (get-buffer "*shell*"))
(pt (lambda ()
(marker-position
(process-mark (get-buffer-process (current-buffer))))))
(ob-babel-p (lambda ()
(goto-char (point-max))
(forward-line -1)
(beginning-of-line)
(let ((line (thing-at-point 'line t)))
(goto-char (point-max))
(and (< 9 (length line))
(equal (substring line -9 -1) "OB-BABEL"))))))
(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")
(comint-send-string session "'ob-babel\n"))
(while (or (equal start (funcall pt))
(not (funcall ob-babel-p)))
(sleep-for 0.1))
(goto-char (point-max))
(forward-line -1)
(beginning-of-line)
(let ((end (point)))
(goto-char (point-max))
(buffer-substring start end)))))))
(provide 'ob-acl2)
;;; ob-acl2.el ends here
|
