1
0
mirror of https://git.savannah.gnu.org/git/emacs/org-mode.git synced 2024-12-04 08:47:03 +00:00
org-mode/lisp/ob-coq.el

81 lines
2.7 KiB
EmacsLisp
Raw Normal View History

Activate lexical binding in some libraries * 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.
2015-10-26 00:56:00 +00:00
;;; ob-coq.el --- Babel Functions for Coq -*- lexical-binding: t; -*-
2014-02-06 02:16:21 +00:00
2021-01-01 19:55:31 +00:00
;; Copyright (C) 2010-2021 Free Software Foundation, Inc.
2014-02-06 02:16:21 +00:00
;; Author: Eric Schulte
;; Keywords: literate programming, reproducible research
;; Homepage: https://orgmode.org
2014-02-06 02:16:21 +00:00
;; 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 <https://www.gnu.org/licenses/>.
2014-02-06 02:16:21 +00:00
;;; 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/
2014-02-06 02:16:21 +00:00
;;; Code:
(require 'ob)
2014-03-05 14:38:48 +00:00
(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.")
2014-02-06 02:16:21 +00:00
(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))
2014-02-06 02:16:21 +00:00
(sit-for 0.1)
(get-buffer org-babel-coq-buffer))
(provide 'ob-coq)
Tiny formatting fixes * lisp/ox.el (org-export-table-dimensions): * lisp/ox-texinfo.el (org-texinfo-template): * lisp/ox-md.el (org-md-link): * lisp/ox-icalendar.el (org-icalendar-use-UTC-date-time-p): * lisp/ox-ascii.el (org-ascii-fixed-width): * lisp/org.el (org-context): * lisp/org-table.el (org-table-eval-formula) (org-table-export): * lisp/org-refile.el: * lisp/org-plot.el (org-plot/gnuplot-to-grid-data): * lisp/org-num.el (org-num): * lisp/org-mouse.el (org-mouse-popup-global-menu) (org-mouse-context-menu): * lisp/org-macro.el (org-macro): * lisp/org-lint.el (org-lint): * lisp/org-keys.el (org-keys): * lisp/org-duration.el: * lisp/org-clock.el (org-clock-get-last-clock-out-time) (org-clock-update-mode-line, org-find-open-clocks): * lisp/org-agenda.el (org-diary) (org-agenda-check-for-timestamp-as-reason-to-ignore-todo-item) (org-agenda-highlight-todo, org-cmp-alpha) (org-agenda-filter-by-category): * lisp/ol.el (org-link-expand-abbrev, ol): * lisp/ol-docview.el (ol-docview): * lisp/ol-bibtex.el (org-execute-file-search-in-bibtex) (org-bibtex, org-bibtex-read): * lisp/ol-bbdb.el (org-bbdb-anniversary-description): * lisp/ob-tangle.el (org-babel-tangle-jump-to-org): * lisp/ob-table.el (org-babel-table-truncate-at-newline): * lisp/ob-stan.el: * lisp/ob-sqlite.el (org-babel-sqlite-table-or-scalar): * lisp/ob-sql.el: * lisp/ob-shen.el: * lisp/ob-shell.el (org-babel-prep-session:shell) (org-babel-prep-session:shell): * lisp/ob-sed.el (org-babel-execute:sed) (org-babel-execute:sed): * lisp/ob-screen.el: * lisp/ob-sass.el: * lisp/ob-ruby.el (org-babel-prep-session:ruby) (org-babel-prep-session:ruby): * lisp/ob-ref.el (org-babel-ref-resolve, ob-ref): * lisp/ob-python.el (org-babel-prep-session:python) (org-babel-prep-session:python): * lisp/ob-plantuml.el: * lisp/ob-picolisp.el: * lisp/ob-perl.el: * lisp/ob-org.el: * lisp/ob-octave.el (org-babel-prep-session:octave) (org-babel-prep-session:octave) (org-babel-octave-evaluate-session): * lisp/ob-ocaml.el: * lisp/ob-mscgen.el (org-babel-execute:mscgen) (org-babel-execute:mscgen): * lisp/ob-maxima.el: (ob-maxima): * lisp/ob-matlab.el: * lisp/ob-makefile.el: * lisp/ob-lua.el (org-babel-prep-session:lua) (org-babel-prep-session:lua): * lisp/ob-lisp.el: * lisp/ob-ledger.el: * lisp/ob-latex.el (org-babel-expand-body:latex) (org-babel-expand-body:latex, ob-latex): * lisp/ob-js.el: * lisp/ob-java.el: * lisp/ob-io.el (org-babel-prep-session:io) (org-babel-prep-session:io): * lisp/ob-hledger.el: * lisp/ob-haskell.el: * lisp/ob-groovy.el (org-babel-groovy-wrapper-method) (org-babel-groovy-evaluate): * lisp/ob-gnuplot.el: * lisp/ob-fortran.el (org-babel-expand-body:fortran) (org-babel-expand-body:fortran): * lisp/ob-forth.el (org-babel-forth-session-execute): * lisp/ob-exp.el (ob-exp): * lisp/ob-eval.el: * lisp/ob-emacs-lisp.el: * lisp/ob-ebnf.el: * lisp/ob-dot.el: * lisp/ob-ditaa.el: * lisp/ob-css.el: * lisp/ob-core.el (org-babel-put-rownames): * lisp/ob-coq.el: * lisp/ob-comint.el: * lisp/ob-calc.el: * lisp/ob-awk.el: * lisp/ob-asymptote.el: * lisp/ob-abc.el: * lisp/ob-R.el (org-babel-prep-session:R): Formatting fixes.
2020-02-18 21:57:37 +00:00
;;; ob-coq.el ends here