Preprocessing commands in Proof-General (inspired from http://coq-blog.clarus.me/why-and-how-to-write-code-compatible-with-many-coq-versions.html)
(defun my-pg-preprocessor (coq-sentence) | |
"Run COQ-SENTENCE through preprocessor and return the result." | |
(let ((preprocessor (with-current-buffer proof-script-buffer | |
(expand-file-name "./preprocessor.rb")))) | |
(with-temp-buffer | |
(insert coq-sentence) | |
(call-process-region (point-min) (point-max) preprocessor t '(t nil) nil) | |
(buffer-string)))) | |
(defun my-pg-preprocessor-hook () | |
"Preprocess PG's current command." | |
(setq string (my-pg-preprocessor string))) | |
(add-hook 'proof-shell-insert-hook #'my-pg-preprocessor-hook) |
#!/usr/bin/env ruby | |
require 'erb' | |
version = `coqc -v`.match(/version ([^(]*) \(/)[1] | |
renderer = ERB.new(STDIN.read) | |
puts renderer.result() |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment