diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-08-29 15:31:04 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-08-29 15:31:04 +0000 |
| commit | 98c930356336fed071617601f8ed0e5cd81f893a (patch) | |
| tree | a0792a699a42e0eca58f9569043ffeeec745c940 /twelf | |
| parent | 992e695a99fa2adcf966c6c3fb537488f7c5b910 (diff) | |
A little bit of progress.
Diffstat (limited to 'twelf')
| -rw-r--r-- | twelf/twelf.el | 27 |
1 files changed, 17 insertions, 10 deletions
diff --git a/twelf/twelf.el b/twelf/twelf.el index 56f9341b..1ce03049 100644 --- a/twelf/twelf.el +++ b/twelf/twelf.el @@ -10,19 +10,25 @@ (require 'proof-easy-config) ; easy configure mechanism -(require 'twelf-font) ; font lock configuration +;; (require 'twelf-font) ; font lock configuration ;; (require 'twelf-old) ; port of parts of old code +;; FIXME: almost working, must modify syntax table so that comments +;; are recognized properly. + (proof-easy-config 'twelf "Twelf" proof-prog-name "twelf-server" proof-assistant-home-page "http://www.cs.cmu.edu/~twelf/" proof-terminal-char ?\. + proof-shell-auto-terminate-commands nil ; server commands don't end with . + ;; FIXME: must also cope with single line comments beginning with % proof-comment-start "%{" proof-comment-end "}%" proof-comment-start-regexp "%[%{\t\n\f]" proof-comment-end "" + ;; FIXME: these don't apply? proof-goal-command-regexp "^%theorem" proof-save-command-regexp "" ;; FIXME: empty? @@ -35,19 +41,20 @@ ;; proof-showproof-command "pr()" ;; proof-undo-n-times-cmd "pg_repeat undo %s;" + proof-auto-multiple-files t - proof-shell-cd-cmd "Twelf.OS.chDir \"%s\";" -;; proof-shell-prompt-pattern "[ML-=#>]+>? " -;; proof-shell-interrupt-regexp "Interrupt" + proof-shell-cd-cmd "OS.chDir %s" + proof-shell-prompt-pattern "%% OK %%\n" + proof-shell-interrupt-regexp "interrupt" ;; proof-shell-start-goals-regexp "Level [0-9]" ;; proof-shell-end-goals-regexp "val it" - - ;; FIXME! - ;; proof-shell-annotated-prompt-regexp "^\\(val it = () : unit\n\\)?ML>? " - proof-shell-error-regexp "%% ABORT %%" - proof-shell-quit-cmd "quit." - proof-shell-restart-cmd "reset." + proof-shell-annotated-prompt-regexp "%% [OA][KB]O?R?T? %%\n" + proof-shell-error-regexp "Server error:" + proof-shell-quit-cmd "quit" + proof-shell-restart-cmd "reset" + + ;; unset ;; 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!" |