e1a327e Aug 27, 2010
67 lines (61 sloc) 2.42 KB
;; demoisa-easy.el --- Example Proof General instance for Isabelle
;; Copyright (C) 1999 LFCS Edinburgh.
;; Author: David Aspinall <>
;; $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.
(require 'proof-site) ; compilation for demoisa
(proof-ready-for-assistant 'demoisa))
(require 'proof)
(require 'proof-easy-config) ; easy configure mechanism
'demoisa "Isabelle Demo"
proof-prog-name "isabelle"
proof-terminal-string ";"
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 ""
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