From b35ce5388cfbd86b2be92e7acb56ff4aa215f58a Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 5 Sep 2009 10:42:23 +0000 Subject: Clean whitespace --- hol98/hol98.el | 62 +++++++++++++++++++++++++++++----------------------------- 1 file changed, 31 insertions(+), 31 deletions(-) (limited to 'hol98') diff --git a/hol98/hol98.el b/hol98/hol98.el index 653bbcb8..57172649 100644 --- a/hol98/hol98.el +++ b/hol98/hol98.el @@ -1,6 +1,6 @@ ;; hol98.el Basic Proof General instance for HOL 98 ;; -;; Copyright (C) 2000 LFCS Edinburgh. +;; Copyright (C) 2000 LFCS Edinburgh. ;; ;; Author: David Aspinall ;; @@ -14,7 +14,7 @@ (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps -(proof-easy-config 'hol98 "HOL" +(proof-easy-config 'hol98 "HOL" proof-prog-name "hol.unquote" proof-terminal-char ?\; proof-script-comment-start "(*" @@ -34,26 +34,26 @@ proof-shell-cd-cmd "FileSys.chDir \"%s\"" proof-shell-filename-escapes '(("\\\\" . "\\\\") ("\"" . "\\\"")) proof-shell-interrupt-regexp "Interrupted" - proof-shell-start-goals-regexp - (proof-regexp-alt "Proof manager status" - "OK.." + proof-shell-start-goals-regexp + (proof-regexp-alt "Proof manager status" + "OK.." "val it =\n") - proof-shell-end-goals-regexp + 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 + proof-shell-annotated-prompt-regexp "^- " ;; This one is nice but less reliable, I think. ;; "\\(> val it = () : unit\n\\)?- " proof-shell-error-regexp "^! " - proof-shell-init-cmd + proof-shell-init-cmd "Help.displayLines:=3000; fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1)); fun pg_top_thm_and_drop () = let val t = top_thm(); in (drop(); t) end;" - ;; FIXME: add optional help topic parameter to help command. + ;; FIXME: add optional help topic parameter to help command. proof-info-command "help \"hol\"" proof-shell-proof-completed-regexp "Initial goal proved" ;; FIXME: next one needs setting so that "urgent" messages are displayed @@ -67,27 +67,27 @@ ;; (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" - ?\| "." + ?\$ "." + ?\/ "." + ?\\ "." + ?+ "." + ?- "." + ?= "." + ?% "." + ?< "." + ?> "." + ?\& "." + ?. "w" + ?_ "w" + ?\' "w" + ?\| "." ?\* ". 23" - ?\( "()1" + ?\( "()1" ?\) ")(4") ;; @@ -104,11 +104,11 @@ "Induct" "Cases" "Cases_on" "Induct_on" "std_ss" "arith_ss" "list_ss" "define_type") - hol98-rules '("ASSUME" "REFL" "BETA_CONV" "SUBST" + 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" + "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" @@ -122,7 +122,7 @@ hol98-tacticals '("ORELSE" "FIRST" "CHANGED_TAC" "THEN" "THENL" "EVERY" "REPEAT" "MAP_EVERY") - proof-script-font-lock-keywords + 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) @@ -134,7 +134,7 @@ ;; proof-goals-font-lock-keywords (list - (cons (proof-ids-to-regexp '("Proof manager status" + (cons (proof-ids-to-regexp '("Proof manager status" "proof" "Incomplete" "Initial goal proved" "Initial goal" @@ -147,7 +147,7 @@ (cons ": GoalstackPure.proofs" 'proof-boring-face) (cons ": Thm.thm" 'proof-boring-face) (cons "val it =" 'proof-boring-face)) - + ;; End of easy config. ) -- cgit v1.2.3