Second version of easy-config, without defvaralias use.

1 files changed, 29 insertions, 34 deletions

diff --git a/demoisa/demoisa-easy.el b/demoisa/demoisa-easy.el
index 7aee3db5..71262d03 100644
--- a/demoisa/demoisa-easy.el
+++ b/demoisa/demoisa-easy.el
@@ -1,4 +1,4 @@
-;; demoisa-easy.el Example Proof General instance for Isabelle
+;; proof-easy.el Example Proof General instance for Isabelle
 ;;
 ;; Copyright (C) 1999 LFCS Edinburgh. 
 ;;
@@ -8,51 +8,46 @@
 ;;
 ;; This is an alternative version of demoisa.el which uses the
 ;; proof-easy-config mechanism to avoid declaring derived modes, etc.
-;;
-;; NB: proof-easy-config is experimental, and only works with XEmacs.
+;; NB: proof-easy-config is experimental.
 ;;
 ;; See demoisa.el for documentation.
 ;;
 ;; To test this file you must rename it demoisa.el.
-;;
-;; It relies on this line in proof-assistant-table:
-;;  demoisa "Isabelle Demo" "\\.ML$"
-;;
 
 (require 'proof-easy-config)            ; easy configure mechanism
 
 (proof-easy-config 
  'demoisa "Isabelle Demo" 
- demoisa-prog-name		   "isabelle"
- demoisa-terminal-char             ?\;
- demoisa-comment-start             "(*"
- demoisa-comment-end               "*)"
- demoisa-goal-command-regexp       "^Goal"
- demoisa-save-command-regexp       "^qed"
- demoisa-goal-with-hole-regexp     "^Goal \\(\\(\"%s\"\\)\\)"
- demoisa-save-with-hole-regexp     "^qed \\(\\(\"%s\"\\)\\)"
- demoisa-non-undoables-regexp      "undo\\|back"
- demoisa-undo-n-times-cmd          "pg_repeat undo %s;"
- demoisa-showproof-command       "pr()"
- demoisa-goal-command              "Goal \"%s\";"
- demoisa-save-command              "qed \"%s\";"
- demoisa-kill-goal-command         "Goal \"PROP no_goal_set\";"
- demoisa-auto-multiple-files       t
- demoisa-shell-cd-cmd              "cd \"%s\""
- demoisa-shell-prompt-pattern      "[ML-=#>]+>? "
- demoisa-shell-interrupt-regexp    "Interrupt"
- demoisa-shell-start-goals-regexp  "Level [0-9]"
- demoisa-shell-end-goals-regexp    "val it"
- demoisa-shell-quit-cmd            "quit();"
- demoisa-assistant-home-page    
+ proof-prog-name		   "isabelle"
+ proof-terminal-char             ?\;
+ proof-comment-start             "(*"
+ proof-comment-end               "*)"
+ proof-goal-command-regexp       "^Goal"
+ proof-save-command-regexp       "^qed"
+ proof-goal-with-hole-regexp     "^Goal \\(\\(\"%s\"\\)\\)"
+ proof-save-with-hole-regexp     "^qed \\(\\(\"%s\"\\)\\)"
+ proof-non-undoables-regexp      "undo\\|back"
+ proof-undo-n-times-cmd          "pg_repeat undo %s;"
+ proof-showproof-command       "pr()"
+ proof-goal-command              "Goal \"%s\";"
+ proof-save-command              "qed \"%s\";"
+ proof-kill-goal-command         "Goal \"PROP no_goal_set\";"
+ proof-auto-multiple-files       t
+ proof-shell-cd-cmd              "cd \"%s\""
+ proof-shell-prompt-pattern      "[ML-=#>]+>? "
+ 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.html"
- demoisa-shell-annotated-prompt-regexp 
+ proof-shell-annotated-prompt-regexp 
  "^\\(val it = () : unit\n\\)?ML>? "
- demoisa-shell-error-regexp             
+ proof-shell-error-regexp             
  "\\*\\*\\*\\|^.*Error:\\|^uncaught exception \\|^Exception- "
- demoisa-shell-init-cmd  
+ proof-shell-init-cmd  
  "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"
- demoisa-shell-demoisa-completed-regexp   
+ proof-shell-proof-completed-regexp   
  "\\(\\(.\\|\n\\)*No subgoals!\n\\)"
- demoisa-shell-eager-annotation-start   
+ proof-shell-eager-annotation-start   
  "^\\[opening \\|^###\\|^Reading")