packages.lisp

(in-package :cl-user)

(defpackage #:pvs
  (:use :cl-user :common-lisp :make)
  (:export :*pvs-buffer-hook*
	   :*pvs-message-hook*
	   :*pvs-warning-hook*
	   :*pvs-error-hook*
	   :*pvs-y-or-n-hook*
	   :*pvs-query-hook*
	   :*pvs-dialog-hook*
	   :pvs-buffer
	   :pvs-error
	   :pvs-warning
	   :pvs-message
	   :pvs-display
	   :pvs-abort
	   :pvs-yn
	   :pvs-query
	   :pvs-emacs-eval
	   :output-proofstate
	   :pvs2json
	   :protect-emacs-output
	   :parse-error
	   :type-error
	   :set-pvs-tmp-file
	   :place
	   :place-list
	   :type-ambiguity
	   :type-incompatible
	   :pvs-locate
	   :write-to-temp-file
	   :*ps-control-info*
	   :make-ps-control-info
	   :psinfo-json-result
	   :psinfo-command
	   :psinfo-cmd-gate
	   :psinfo-res-gate
	   :psinfo-lock
	   :pvs-abort
	   :lisp
	   :xmlrpc-output-proofstate
	   :add-psinfo))