branch: elpa/org-contrib commit 3062acd0e350598727f8dac459ae3a5ee05db7c6 Author: Bastien Guerry <b...@gnu.org> Commit: Bastien Guerry <b...@gnu.org>
Remove ob-coq.el now maintained at https://github.com/sp1ff/ob-coq Thanks to Luc Pellissier for maintaining ob-coq.el so far. --- README.md | 1 - README.org | 1 - lisp/ob-coq.el | 81 ---------------------------------------------------------- 3 files changed, 83 deletions(-) diff --git a/README.md b/README.md index 775a7f1355..7d309aa250 100644 --- a/README.md +++ b/README.md @@ -101,7 +101,6 @@ minor or major release. ## Org Babel languages - **ob-abc.el:** Org-mode Babel Functions for ABC -- **ob-coq.el:** Org-mode Babel Functions for Coq - **ob-csharp.el:** Org-mode Babel Functions for csharp evaluation - **ob-ebnf.el:** Org-mode Babel Functions for EBNF - **ob-eukleides.el:** Org-mode Babel Functions for eukleides evaluation diff --git a/README.org b/README.org index 43cd2a3eed..12f0afc75f 100644 --- a/README.org +++ b/README.org @@ -91,7 +91,6 @@ minor or major release. *** Org Babel languages - ob-abc.el :: Org-mode Babel Functions for ABC -- ob-coq.el :: Org-mode Babel Functions for Coq - ob-csharp.el :: Org-mode Babel Functions for csharp evaluation - ob-ebnf.el :: Org-mode Babel Functions for EBNF - ob-eukleides.el :: Org-mode Babel Functions for eukleides evaluation diff --git a/lisp/ob-coq.el b/lisp/ob-coq.el deleted file mode 100644 index e05259565a..0000000000 --- a/lisp/ob-coq.el +++ /dev/null @@ -1,81 +0,0 @@ -;;; ob-coq.el --- Babel Functions for Coq -*- lexical-binding: t; -*- - -;; Copyright (C) 2010-2021 Free Software Foundation, Inc. - -;; Author: Eric Schulte -;; Maintainer: Luc Pellissier <luc.pelliss...@crans.org> -;; Keywords: literate programming, reproducible research -;; Homepage: https://git.sr.ht/~bzg/org-contrib - -;; This file is not part of GNU Emacs. - -;; GNU Emacs 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 of the License, or -;; (at your option) any later version. - -;; GNU Emacs 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: - -;; Rudimentary support for evaluating Coq code blocks. Currently only -;; session evaluation is supported. Requires both coq.el and -;; coq-inferior.el, both of which are distributed with Coq. -;; -;; https://coq.inria.fr/ - -;;; Code: -(require 'ob) - -(declare-function run-coq "ext:coq-inferior.el" (cmd)) -(declare-function coq-proc "ext:coq-inferior.el" ()) - -(defvar coq-program-name "coqtop" - "Name of the coq toplevel to run.") - -(defvar org-babel-coq-buffer "*coq*" - "Buffer in which to evaluate coq code blocks.") - -(defun org-babel-coq-clean-prompt (string) - (if (string-match "^[^[:space:]]+ < " string) - (substring string 0 (match-beginning 0)) - string)) - -(defun org-babel-execute:coq (body params) - (let ((full-body (org-babel-expand-body:generic body params)) - (session (org-babel-coq-initiate-session)) - (pt (lambda () - (marker-position - (process-mark (get-buffer-process (current-buffer))))))) - (org-babel-coq-clean-prompt - (org-babel-comint-in-buffer session - (let ((start (funcall pt))) - (with-temp-buffer - (insert full-body) - (comint-send-region (coq-proc) (point-min) (point-max)) - (comint-send-string (coq-proc) - (if (string= (buffer-substring (- (point-max) 1) (point-max)) ".") - "\n" - ".\n"))) - (while (equal start (funcall pt)) (sleep-for 0.1)) - (buffer-substring start (funcall pt))))))) - -(defun org-babel-coq-initiate-session () - "Initiate a coq session. -If there is not a current inferior-process-buffer in SESSION then -create one. Return the initialized session." - (unless (fboundp 'run-coq) - (error "`run-coq' not defined, load coq-inferior.el")) - (save-window-excursion (run-coq coq-program-name)) - (sit-for 0.1) - (get-buffer org-babel-coq-buffer)) - -(provide 'ob-coq) - -;;; ob-coq.el ends here