diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-17 12:55:55 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-17 12:55:55 +0000 |
| commit | a893053a2949e94d54eddb53aa31b61fb31b3679 (patch) | |
| tree | 6cffa76f53b7ecbab4995b27c42b53b45d7efddd /doc/PG-adapting.texi | |
| parent | 61b1f84e96eee6042f17bb4e8681216cf2d3ca51 (diff) | |
Fix included file
Diffstat (limited to 'doc/PG-adapting.texi')
| -rw-r--r-- | doc/PG-adapting.texi | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index ac8ad8d4..ee3a75c7 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -3932,7 +3932,7 @@ Proof General. @lisp @c FIXME: MAGIC NEEDED TO INCLUDE FILE VERBATIM -@c @includeverbatim ../demoisa/demoisa-easy.el +@c @includeverbatim ../demoisa/demoisa.el ;; demoisa.el Example Proof General instance for Isabelle ;; ;; Copyright (C) 1999 LFCS Edinburgh. @@ -4076,19 +4076,6 @@ Proof General. ;; add highlighting, or some of the proof by pointing markup ;; configuration for the goals buffer. -;; The final piece of magic here is a hook which configures settings -;; to get the proof shell running. Proof General needs to know the -;; name of the program to run, and the modes for the shell, response, -;; and goals buffers. - -(add-hook 'proof-pre-shell-start-hook 'demoisa-pre-shell-start) - -(defun demoisa-pre-shell-start () - (setq proof-prog-name isabelledemo-prog-name) - (setq proof-mode-for-shell 'demoisa-shell-mode) - (setq proof-mode-for-response 'demoisa-response-mode) - (setq proof-mode-for-goals 'demoisa-goals-mode)) - (provide 'demoisa) @end lisp |