aboutsummaryrefslogtreecommitdiffhomepage
path: root/ccc
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-05 10:42:23 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-05 10:42:23 +0000
commitb35ce5388cfbd86b2be92e7acb56ff4aa215f58a (patch)
treeaa6f57349bb07993bf80136e6dd18a8fe0e6ea84 /ccc
parent41a4f20e3250cbe225fb8363738a6c6ac35d0368 (diff)
Clean whitespace
Diffstat (limited to 'ccc')
-rw-r--r--ccc/ccc.el51
1 files changed, 24 insertions, 27 deletions
diff --git a/ccc/ccc.el b/ccc/ccc.el
index 0fdf77de..9b5c35e4 100644
--- a/ccc/ccc.el
+++ b/ccc/ccc.el
@@ -1,27 +1,27 @@
;; ccc.el - Proof General for the Casl Consistency Checker
-;;
+;;
;; Author: Christoph Lüth <cxl@informatik.uni-bremen.de>
-;;
+;;
;; This is a fairly straightforward instantiation of Proof General for
-;; the Casl Consistency Checker, CCC.
+;; the Casl Consistency Checker, CCC.
;;
;; CASL is the standard algebraic specification language, and CCC is a
;; tool to check consistency of CASL specifications.
-;;
+;;
;; For more information, hasten thee browser yonder:
;; http://www.informatik.uni-bremen.de/cofi/ccc
(require 'proof-easy-config) ; nice and easy does it
(require 'proof-syntax) ; functions for making regexps
-(proof-easy-config 'ccc "CASL Consistency Checker"
+(proof-easy-config 'ccc "CASL Consistency Checker"
proof-prog-name "ccc" ;; must be in your path.
proof-terminal-char ?\;
proof-script-comment-start "(*"
proof-script-comment-end "*)"
proof-goal-command-regexp "\\(ccc\\|holcasl\\) \".*\";"
proof-save-command-regexp "^qeccc"
- proof-goal-with-hole-regexp "\\(ccc\\|holcasl\\) \"\\(\\(.*\\)\\)\""
+ proof-goal-with-hole-regexp "\\(ccc\\|holcasl\\) \"\\(\\(.*\\)\\)\""
proof-save-with-hole-regexp "qeccc \"\\(\\(.*\\)\\)\""
proof-non-undoables-regexp "undo\\|back"
proof-goal-command "ccc \"%s\";"
@@ -29,7 +29,7 @@
proof-kill-goal-command "abort ();"
proof-showproof-command "prt()"
proof-undo-n-times-cmd "undo_steps %s;"
- proof-auto-multiple-files nil
+ proof-auto-multiple-files nil
proof-shell-cd-cmd "cd \"%s\""
proof-shell-interrupt-regexp "Interrupt"
proof-shell-start-goals-regexp "^No subgoals\\|^[0-9]* subgoals\\|^Wts:"
@@ -43,35 +43,35 @@
proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" ;;; ???
;;
- ;; Some basic fontlocking and syntax table entries, as taken from the
+ ;; Some basic fontlocking and syntax table entries, as taken from the
;; hol98 instance (it's all SML anyway :-)
;;
proof-script-syntax-table-entries
'(?\` "\""
- ?\$ "."
- ?\/ "."
- ?\\ "."
- ?+ "."
- ?- "."
- ?= "."
- ?% "."
- ?< "."
- ?> "."
- ?\& "."
- ?. "w"
- ?_ "w"
- ?\' "w"
+ ?\$ "."
+ ?\/ "."
+ ?\\ "."
+ ?+ "."
+ ?- "."
+ ?= "."
+ ?% "."
+ ?< "."
+ ?> "."
+ ?\& "."
+ ?. "w"
+ ?_ "w"
+ ?\' "w"
?\| "."
?\[ "(]"
- ?\] ")["
+ ?\] ")["
?\* ". 23"
- ?\( "()1"
+ ?\( "()1"
?\) ")(4")
ccc-keywords '("use" "ap" "holcasl" "ccc" "load_lib" "qeccc")
ccc-tactics '("compose" "compose'" "prove" "prove_free_type")
ccc-tacticals '("Repeat" "Orelse" "Then" "ThenList" "OrelseList")
- proof-script-font-lock-keywords
+ proof-script-font-lock-keywords
(list
(cons (proof-ids-to-regexp ccc-keywords) 'font-lock-keyword-face)
(cons (proof-ids-to-regexp ccc-tactics) 'font-lock-keyword-face)
@@ -80,6 +80,3 @@
)
-
-
-