aboutsummaryrefslogtreecommitdiffhomepage
path: root/pghaskell
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2015-01-05 11:39:30 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2015-01-05 11:39:30 +0000
commita7e139c5aa4b597f34d501efa283efe7732d893e (patch)
treeaa02aa70d6c68f11029b172559bf7118a6366215 /pghaskell
parent453c56a955f15623a29ae41a4e767b7745e80076 (diff)
Deleted file
Diffstat (limited to 'pghaskell')
-rw-r--r--pghaskell/pghashell.el58
1 files changed, 0 insertions, 58 deletions
diff --git a/pghaskell/pghashell.el b/pghaskell/pghashell.el
deleted file mode 100644
index ced3514f..00000000
--- a/pghaskell/pghashell.el
+++ /dev/null
@@ -1,58 +0,0 @@
-;; pgocaml.el - Proof General for Haskell scripts.
-;;
-;; David Aspinall. $Id$
-;;
-;; This instance of PG is handy just for using script management to
-;; cut-and-paste into a buffer running Haskell (ghci)
-;;
-;; I'm providing this so that tool demonstrators may use it instead of
-;; tediously doing cut-and-paste of commands from a file. No history
-;; management, and nothing to do with theorem proving really!
-;;
-;; To use this instance of PG, visit a file with the ".pghci" extension
-;; or type
-;;
-;; M-x pgocaml-mode
-;;
-;; in an ordinary .ml file. (Check that you have enabled the instance
-;; in proof-site.el).
-;;
-
-
-(require 'proof-easy-config)
-(require 'proof-syntax)
-
-(proof-easy-config 'pgocaml "PG-OCaml"
-
- proof-prog-name "ocaml"
- proof-terminal-string ";;"
- proof-script-comment-start "(*"
- proof-script-comment-end "*)"
- proof-shell-annotated-prompt-regexp "^# " ;; matches interpreter prompts
-
- ;; Syntax table suitable for OCaml; see Elisp documentation of `modify-syntax-entry'
- proof-script-syntax-table-entries
- '(?\` "\""
- ?\$ "."
- ?\/ "."
- ?\\ "."
- ?+ "."
- ?- "."
- ?= "."
- ?% "."
- ?< "."
- ?> "."
- ?\& "."
- ?. "w"
- ?_ "w"
- ?\' "w"
- ?\| "."
- ?\* ". 23n"
- ?\( "()1"
- ?\) ")(4")
-
- ;; next setting is just to prevent warning
- proof-save-command-regexp proof-no-regexp
- )
-
-(provide 'pgocaml)