mirror of
https://git.savannah.gnu.org/git/emacs/org-mode.git
synced 2024-07-16 06:16:27 +00:00
f0bf77e82a
* lisp/ob-C.el (org-babel-prep-session:C): (org-babel-load-session:C): * lisp/ob-J.el: (org-babel-expand-body:J): (org-babel-execute:J): * lisp/ob-R.el: (org-babel-expand-body:R): * lisp/ob-abc.el: (org-babel-execute:abc): (org-babel-prep-session:abc): * lisp/ob-asymptote.el: (org-babel-execute:asymptote): (org-babel-prep-session:asymptote): * lisp/ob-awk.el: (org-babel-expand-body:awk): * lisp/ob-calc.el: (org-babel-expand-body:calc): * lisp/ob-clojure.el: * lisp/ob-comint.el: (org-babel-comint-in-buffer): (org-babel-comint-with-output): (org-babel-comint-eval-invisibly-and-wait-for-file): * lisp/ob-coq.el: * lisp/ob-css.el: (org-babel-execute:css): (org-babel-prep-session:css): * lisp/ob-ditaa.el: (org-babel-execute:ditaa): (org-babel-prep-session:ditaa): * lisp/ob-dot.el: (org-babel-execute:dot): (org-babel-prep-session:dot): * lisp/ob-ebnf.el: * lisp/ob-emacs-lisp.el: * lisp/ob-eval.el: * lisp/ob-forth.el: * lisp/ob-fortran.el: (org-babel-execute:fortran): (org-babel-prep-session:fortran): (org-babel-load-session:fortran): * lisp/ob-gnuplot.el: (org-babel-expand-body:gnuplot): (org-babel-prep-session:gnuplot): (org-babel-gnuplot-initiate-session): * lisp/ob-groovy.el: (org-babel-prep-session:groovy): (org-babel-groovy-initiate-session): * lisp/ob-haskell.el: (org-babel-haskell-initiate-session): * lisp/ob-io.el: (org-babel-prep-session:io): (org-babel-io-initiate-session): * lisp/ob-java.el: (org-babel-execute:java): * lisp/ob-js.el: * lisp/ob-keys.el: * lisp/ob-latex.el: (org-babel-prep-session:latex): * lisp/ob-ledger.el: (org-babel-execute:ledger): (org-babel-prep-session:ledger): * lisp/ob-lilypond.el: (org-babel-lilypond-commands): (org-babel-lilypond-process-basic): (org-babel-prep-session:lilypond): (org-babel-lilypond-parse-line-num): * lisp/ob-lisp.el: * lisp/ob-makefile.el: (org-babel-execute:makefile): (org-babel-prep-session:makefile): * lisp/ob-matlab.el: * lisp/ob-maxima.el: (org-babel-prep-session:maxima): * lisp/ob-mscgen.el: (org-babel-prep-session:mscgen): * lisp/ob-ocaml.el: (org-babel-execute:ocaml): (org-babel-prep-session:ocaml): * lisp/ob-octave.el: (org-babel-execute:octave): (org-babel-octave-initiate-session): * lisp/ob-org.el: (org-babel-prep-session:org): * lisp/ob-perl.el: (org-babel-prep-session:perl): (org-babel-perl--var-to-perl): (org-babel-perl-initiate-session): * lisp/ob-picolisp.el: (org-babel-expand-body:picolisp): (org-babel-execute:picolisp): * lisp/ob-plantuml.el: (org-babel-execute:plantuml): (org-babel-prep-session:plantuml): * lisp/ob-processing.el: (org-babel-prep-session:processing): * lisp/ob-python.el: (org-babel-python-initiate-session): * lisp/ob-ref.el: (org-babel-ref-resolve): * lisp/ob-ruby.el: (org-babel-ruby-initiate-session): * lisp/ob-sass.el: (org-babel-execute:sass): (org-babel-prep-session:sass): * lisp/ob-scala.el: (org-babel-execute:scala): (org-babel-prep-session:scala): (org-babel-scala-initiate-session): * lisp/ob-scheme.el: * lisp/ob-screen.el: (org-babel-prep-session:screen): (org-babel-screen-session-write-temp-file): (org-babel-screen-test): * lisp/ob.el: * lisp/org-colview.el: (org-columns-todo): (org-columns-set-tags-or-toggle): (org-columns-new): (org-columns-uncompile-format): (org-agenda-colview-summarize): * lisp/org-footnote.el: (electric-indent-mode): * lisp/org-indent.el: (org-indent-refresh-maybe): * lisp/org-list.el: * lisp/org-macro.el: (org-macro--collect-macros): * lisp/org-src.el: * lisp/org-table.el: (sort-fold-case): (org-table-create): (org-table-field-info): (org-table-transpose-table-at-point): (org-table-remove-rectangle-highlight): (orgtbl-create-or-convert-from-region): (org-define-lookup-function): * lisp/ox-ascii.el: (org-ascii-format-drawer-function): (org-ascii--has-caption-p): (org-ascii-bold): (org-ascii-center-block): (org-ascii-clock): (org-ascii-code): (org-ascii-dynamic-block): (org-ascii-entity): (org-ascii-example-block): (org-ascii-export-snippet): (org-ascii-export-block): (org-ascii-fixed-width): (org-ascii-footnote-reference): (org-ascii-horizontal-rule): (org-ascii-inline-src-block): (org-ascii-format-inlinetask-default): (org-ascii-italic): (org-ascii-keyword): (org-ascii-latex-environment): (org-ascii-latex-fragment): (org-ascii-line-break): (org-ascii-node-property): (org-ascii-planning): (org-ascii-quote-block): (org-ascii-radio-target): (org-ascii-special-block): (org-ascii-src-block): (org-ascii-statistics-cookie): (org-ascii-subscript): (org-ascii-superscript): (org-ascii-strike-through): (org-ascii-timestamp): (org-ascii-underline): (org-ascii-verbatim): (org-ascii-verse-block): (org-ascii-filter-headline-blank-lines): (org-ascii-filter-paragraph-spacing): (org-ascii-filter-comment-spacing): Use lexical binding.
78 lines
2.6 KiB
EmacsLisp
78 lines
2.6 KiB
EmacsLisp
;;; ob-coq.el --- Babel Functions for Coq -*- lexical-binding: t; -*-
|
|
|
|
;; Copyright (C) 2010-2015 Free Software Foundation, Inc.
|
|
|
|
;; Author: Eric Schulte
|
|
;; Keywords: literate programming, reproducible research
|
|
;; Homepage: http://orgmode.org
|
|
|
|
;; This file is 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 <http://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.
|
|
;;
|
|
;; http://coq.inria.fr/
|
|
|
|
;;; Code:
|
|
(require 'ob)
|
|
|
|
(declare-function run-coq "ext:coq-inferior.el" (cmd))
|
|
(declare-function coq-proc "ext:coq-inferior.el" ())
|
|
|
|
(defvar org-babel-coq-buffer "*coq*"
|
|
"Buffer in which to evaluate coq code blocks.")
|
|
|
|
(defvar org-babel-coq-eoe "org-babel-coq-eoe")
|
|
|
|
(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 "coqtop"))
|
|
(sit-for 0.1)
|
|
(get-buffer org-babel-coq-buffer))
|
|
|
|
(provide 'ob-coq)
|