From a85c79543c3203516226a414ccf3caff35c0c6e4 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Mon, 28 Aug 2000 14:57:11 +0000
Subject: Files for twelf, not working at all yet.

---
 twelf/twelf.el | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 twelf/twelf.el

(limited to 'twelf/twelf.el')

diff --git a/twelf/twelf.el b/twelf/twelf.el
new file mode 100644
index 00000000..56f9341b
--- /dev/null
+++ b/twelf/twelf.el
@@ -0,0 +1,58 @@
+;; twelf.el  Proof General instance for Twelf
+;;
+;; Copyright (C) 2000 LFCS Edinburgh. 
+;;
+;; Author: David Aspinall <da@dcs.ed.ac.uk>
+;;
+;; $Id$
+;;
+;;
+
+(require 'proof-easy-config)            ; easy configure mechanism
+
+(require 'twelf-font)			; font lock configuration
+;; (require 'twelf-old)			; port of parts of old code
+
+(proof-easy-config 
+ 'twelf "Twelf" 
+ proof-prog-name		 "twelf-server"
+ proof-assistant-home-page       "http://www.cs.cmu.edu/~twelf/"
+ proof-terminal-char             ?\.
+ ;; 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?
+ proof-goal-with-hole-regexp     "^%theorem\w-+\\(.*\\)\w-+:"
+ proof-save-with-hole-regexp     "" ;; FIXME
+ ;; proof-non-undoables-regexp      "undo\\|back"
+ proof-goal-command              "%theorem %s."
+ proof-save-command              "%prove "
+ ;; 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              "Twelf.OS.chDir \"%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"
+ 
+ ;; 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-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 'twelf)
\ No newline at end of file
-- 
cgit v1.2.3