diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 15:09:14 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 15:09:14 +0000 |
commit | 5233a76cd81bbfa426ee33b0e12c183ac69a59f3 (patch) | |
tree | 15fbcf3ee4470cbb884979ca6f3c86b81693d352 | |
parent | 8df4063948265c0f0b8e967eafb9c091feed1f76 (diff) |
Renamed from demoisa/demoisa-easy.el to obsolete/demoisa/demoisa-easy.el
-rw-r--r-- | demoisa/demoisa-easy.el | 66 |
1 files changed, 0 insertions, 66 deletions
diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el deleted file mode 100644 index 6631cebd..00000000 --- a/demoisa/demoisa-easy.el +++ /dev/null @@ -1,66 +0,0 @@ -;; demoisa-easy.el --- Example Proof General instance for Isabelle -;; -;; Copyright (C) 1999 LFCS Edinburgh. -;; -;; Author: David Aspinall <David.Aspinall@ed.ac.uk> -;; -;; $Id$ -;; -;; This is an alternative version of demoisa.el which uses the -;; proof-easy-config macro to do most of the work. -;; -;; This mechanism is recommended for new instantiations of -;; Proof General since it follows a regular pattern, and we can more -;; easily adapt it in the future to new versions of Proof General -;; using alternative architectures. It is still easy to augment -;; with additional elisp functions and other settings. -;; -;; The most important setting is `proof-shell-annotated-prompt-regexp' -;; used to recognize prompt texts from the prover. -;; -;; See demoisa.el and the Adapting Proof General manual for more -;; documentation. Please do read the documentation of the variables -;; to understand how things work. -;; -;; To test this file you must rename it demoisa.el. -;; - -(eval-and-compile - (require 'proof-site) ; compilation for demoisa - (proof-ready-for-assistant 'demoisa)) - -(require 'proof) -(require 'proof-easy-config) ; easy configure mechanism - -(proof-easy-config - 'demoisa "Isabelle Demo" - proof-prog-name "isabelle" - proof-terminal-char ?\; - proof-script-comment-start "(*" - proof-script-comment-end "*)" - proof-goal-command-regexp "^Goal" - proof-save-command-regexp "^qed" - proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" - proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" - proof-non-undoables-regexp "undo\\|back" - proof-goal-command "Goal \"%s\";" - proof-save-command "qed \"%s\";" - proof-kill-goal-command "Goal \"PROP no_goal_set\";" - proof-showproof-command "pr()" - proof-undo-n-times-cmd "pg_repeat undo %s;" - proof-auto-multiple-files t - proof-shell-cd-cmd "cd \"%s\"" - proof-shell-interrupt-regexp "Interrupt" - proof-shell-start-goals-regexp "Level [0-9]" - proof-shell-end-goals-regexp "val it" - proof-shell-quit-cmd "quit();" - proof-assistant-home-page "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/" - proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?\\(ML\\)?> " - proof-shell-error-regexp "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- " - proof-shell-init-cmd "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));" - proof-shell-proof-completed-regexp "^No subgoals!" - proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading") - -(provide 'demoisa) - -;;; demoisa-easy.el ends here |