From 7ec2a7d39e2bdd3bfc9186fb44e7c7782bd39171 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 10 Mar 2000 09:17:08 +0000 Subject: Added decoration and syntax table entries. --- hol98/hol98.el | 112 ++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 95 insertions(+), 17 deletions(-) (limited to 'hol98') diff --git a/hol98/hol98.el b/hol98/hol98.el index a6c5ca71..31fb1b3a 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -11,14 +11,8 @@ ;; See the README file in this directory for information. -;; keywords: -;; val prove store_thm prove by -;; tacticals: THEN THENL -;; by seems to be "e"; - - (require 'proof-easy-config) ; easy configure mechanism -(require 'proof-syntax) +(require 'proof-syntax) ; functions for making regexps (proof-easy-config 'hol98 "HOL" proof-prog-name "hol.unquote" @@ -26,9 +20,12 @@ proof-comment-start "(*" proof-comment-end "*)" proof-goal-command-regexp "^g[ `]" - proof-save-command-regexp "^qed" - proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" - proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" + proof-save-command-regexp "^val .*top_thm()" + ;; FIXME: next two just to suppress warnings, not set yet. + proof-goal-with-hole-regexp "^\0\1$" + proof-save-with-hol-regexp "^\0\1$" + ;; proof-goal-with-hole-regexp "qed_goal \"\\(\\(.*\\)\\)\"" + ;; proof-save-with-hole-regexp "qed \"\\(\\(.*\\)\\)\"" proof-non-undoables-regexp "b()" proof-goal-command "g `%s`;" proof-save-command "val %s = top_thm(); drop();" @@ -36,17 +33,18 @@ proof-showproof-command "p()" proof-undo-n-times-cmd "(pg_repeat backup %s; p());" proof-auto-multiple-files t -; proof-shell-cd-cmd "cd \"%s\"" + proof-shell-cd-cmd "FileSys.chDir \"%s\"" proof-shell-prompt-pattern "^[->] " proof-shell-interrupt-regexp "Interrupted" -; proof-shell-start-goals-regexp "Proof manager status\\|OK.." proof-shell-start-goals-regexp - (proof-regexp-alt "Proof manager status" "OK.." "val it =\n") + (proof-regexp-alt "Proof manager status" + "OK.." + "val it =\n") proof-shell-end-goals-regexp (proof-regexp-alt "^[ \t]*: GoalstackPure.goalstack" "^[ \t]*: GoalstackPure.proofs") proof-shell-quit-cmd "quit();" - proof-assistant-home-page + proof-assistant-home-page "http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html" proof-shell-annotated-prompt-regexp "^\\(> val it = () : unit\n\\)?- " @@ -59,11 +57,91 @@ proof-info-command "help \"hol\"" proof-shell-proof-completed-regexp "\\(\\(.\\|\n\\)*No subgoals!\n\\)" -; proof-shell-eager-annotation-start + ;; FIXME: next one needs setting. + ;; proof-shell-eager-annotation-start proof-find-theorems-command "DB.match [] (%s);" + ;; We must set this to use ptys since mosml doesn't flush its output - ;; (on Linux, presumably on Solaris to). + ;; (on Linux, presumably on Solaris too). proof-shell-process-connection-type t + + ;; + ;; Syntax table entries for proof scripts + ;; + proof-script-syntax-table-entries + '(?\` "\"" + ?\$ "." + ?\/ "." + ?\\ "." + ?+ "." + ?- "." + ?= "." + ?% "." + ?< "." + ?> "." + ?\& "." + ?. "w" + ?_ "w" + ?\' "w" + ?\| "." + ?\* ". 23" + ?\( "()1" + ?\) ")(4") + + ;; + ;; A few of the vast variety of keywords, tactics, tacticals, + ;; for decorating proof scripts. + ;; + ;; In the future, PG will use a mechanism for passing identifier + ;; lists like this from the proof assistant, we don't really + ;; want to duplicate the information here! + ;; + hol98-keywords '("g" "expand" "e" "val" "store_thm" "top_thm" "by" + "Define" "xDefine" "Hol_defn" + "Induct" "Cases" "Cases_on" "Induct_on" + "std_ss" "arith_ss" "list_ss" + "define_type") + hol98-rules '("ASSUME" "REFL" "BETA_CONV" "SUBST" + "ABS" "INST_TYPE" "DISCH" "MP" + "T_DEF" "FORALL_DEF" "AND_DEF" "OR_DEF" "F_DEF" + "NOT_DEF" "EXISTS_UNIQUE_DEF" "BOOL_CASES_AX" + "IMP_ANTISYM_AX" "ETA_AX" "SELECT_AX" "ONE_ONE_DEF" + "ONTO_DEF" "INFINITY_AX" "LET_DEF" "COND_DEF" "ARB_DEF") + hol98-tactics '("ACCEPT_TAC" "ASSUME_TAC" "GEN_TAC" + "CONJ_TAC" "DISCH_TAC" "STRIP_TAC" + "SUBST_TAC" "ASM_CASES_TAC" "DISJ_CASES_TAC" + "REWRITE_TAC" "IMP_RES_TAC" "ALL_TAC" "NO_TAC" + "EQ_TAC" "EXISTS_TAC" "INDUCT_TAC" + "POP_ASM" "SUBST1_TAC" "ASSUM_LIST" + "PROVE" "PROVE_TAC" "DECIDE" "DECIDE_TAC" "RW_TAC" + "STP_TAC" "ZAP_TAC" + "EXISTS_TAC") + hol98-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN" + "THENL" "EVERY" "REPEAT" + "MAP_EVERY") + proof-script-font-lock-keywords + (list + (cons (proof-ids-to-regexp hol98-keywords) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp hol98-tactics) 'font-lock-keyword-face) + ; (cons (proof-ids-to-regexp hol98-rules) 'font-lock-keyword-face) + (cons (proof-ids-to-regexp hol98-tacticals) 'proof-tacticals-name-face)) + + ;; + ;; Some decoration of the goals output + ;; + proof-goals-font-lock-keywords + (list + (cons (proof-ids-to-regexp '("Proof manager status" + "proof" "Incomplete" + "Initial goal")) + 'font-lock-keyword-face)) + + + ;; End of easy config. ) -(provide 'demoisa) \ No newline at end of file + +(warn "Hol Proof General is incomplete! Please help improve it! +Read the manual, make improvements and send them to proofgen@dcs.ed.ac.uk") + +(provide 'hol98) \ No newline at end of file -- cgit v1.2.3