New pseudo instances to help tool demonstrators in ocaml/ghci (in progress)

2 files changed, 117 insertions, 0 deletions

diff --git a/pghaskell/pghashell.el b/pghaskell/pghashell.el
new file mode 100644
index 00000000..ced3514f
--- /dev/null
+++ b/pghaskell/pghashell.el
@@ -0,0 +1,58 @@
+;; 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)
diff --git a/pghaskell/pghaskell.el b/pghaskell/pghaskell.el
new file mode 100644
index 00000000..5a92256b
--- /dev/null
+++ b/pghaskell/pghaskell.el
@@ -0,0 +1,59 @@
+;; 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 pghaskell-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		     "ghci"
+;; BELOW HERE TODO TODO
+ 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 'pghaskell)