| commit | author | age | ||
| 76bbd0 | 1 | ;;; ob-coq.el --- Babel Functions for Coq -*- lexical-binding: t; -*- |
| C | 2 | |
| 3 | ;; Copyright (C) 2010-2018 Free Software Foundation, Inc. | |
| 4 | ||
| 5 | ;; Author: Eric Schulte | |
| 6 | ;; Keywords: literate programming, reproducible research | |
| 7 | ;; Homepage: https://orgmode.org | |
| 8 | ||
| 9 | ;; This file is part of GNU Emacs. | |
| 10 | ||
| 11 | ;; GNU Emacs is free software: you can redistribute it and/or modify | |
| 12 | ;; it under the terms of the GNU General Public License as published by | |
| 13 | ;; the Free Software Foundation, either version 3 of the License, or | |
| 14 | ;; (at your option) any later version. | |
| 15 | ||
| 16 | ;; GNU Emacs is distributed in the hope that it will be useful, | |
| 17 | ;; but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| 18 | ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| 19 | ;; GNU General Public License for more details. | |
| 20 | ||
| 21 | ;; You should have received a copy of the GNU General Public License | |
| 22 | ;; along with GNU Emacs. If not, see <https://www.gnu.org/licenses/>. | |
| 23 | ||
| 24 | ;;; Commentary: | |
| 25 | ||
| 26 | ;; Rudimentary support for evaluating Coq code blocks. Currently only | |
| 27 | ;; session evaluation is supported. Requires both coq.el and | |
| 28 | ;; coq-inferior.el, both of which are distributed with Coq. | |
| 29 | ;; | |
| 30 | ;; http://coq.inria.fr/ | |
| 31 | ||
| 32 | ;;; Code: | |
| 33 | (require 'ob) | |
| 34 | ||
| 35 | (declare-function run-coq "ext:coq-inferior.el" (cmd)) | |
| 36 | (declare-function coq-proc "ext:coq-inferior.el" ()) | |
| 37 | ||
| 38 | (defvar coq-program-name "coqtop" | |
| 39 | "Name of the coq toplevel to run.") | |
| 40 | ||
| 41 | (defvar org-babel-coq-buffer "*coq*" | |
| 42 | "Buffer in which to evaluate coq code blocks.") | |
| 43 | ||
| 44 | (defun org-babel-coq-clean-prompt (string) | |
| 45 | (if (string-match "^[^[:space:]]+ < " string) | |
| 46 | (substring string 0 (match-beginning 0)) | |
| 47 | string)) | |
| 48 | ||
| 49 | (defun org-babel-execute:coq (body params) | |
| 50 | (let ((full-body (org-babel-expand-body:generic body params)) | |
| 51 | (session (org-babel-coq-initiate-session)) | |
| 52 | (pt (lambda () | |
| 53 | (marker-position | |
| 54 | (process-mark (get-buffer-process (current-buffer))))))) | |
| 55 | (org-babel-coq-clean-prompt | |
| 56 | (org-babel-comint-in-buffer session | |
| 57 | (let ((start (funcall pt))) | |
| 58 | (with-temp-buffer | |
| 59 | (insert full-body) | |
| 60 | (comint-send-region (coq-proc) (point-min) (point-max)) | |
| 61 | (comint-send-string (coq-proc) | |
| 62 | (if (string= (buffer-substring (- (point-max) 1) (point-max)) ".") | |
| 63 | "\n" | |
| 64 | ".\n"))) | |
| 65 | (while (equal start (funcall pt)) (sleep-for 0.1)) | |
| 66 | (buffer-substring start (funcall pt))))))) | |
| 67 | ||
| 68 | (defun org-babel-coq-initiate-session () | |
| 69 | "Initiate a coq session. | |
| 70 | If there is not a current inferior-process-buffer in SESSION then | |
| 71 | create one. Return the initialized session." | |
| 72 | (unless (fboundp 'run-coq) | |
| 73 | (error "`run-coq' not defined, load coq-inferior.el")) | |
| 74 | (save-window-excursion (run-coq coq-program-name)) | |
| 75 | (sit-for 0.1) | |
| 76 | (get-buffer org-babel-coq-buffer)) | |
| 77 | ||
| 78 | (provide 'ob-coq) | |
