From 5f7695ac97fe7e624f00954fa39b1b6149427654 Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Tue, 7 Feb 2012 11:20:14 +0000
Subject: New pseudo instances to help tool demonstrators in ocaml/ghci (in
 progress)

---
 pgocaml/pgocaml.el | 58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 58 insertions(+)
 create mode 100644 pgocaml/pgocaml.el

(limited to 'pgocaml/pgocaml.el')

diff --git a/pgocaml/pgocaml.el b/pgocaml/pgocaml.el
new file mode 100644
index 00000000..4b11c7df
--- /dev/null
+++ b/pgocaml/pgocaml.el
@@ -0,0 +1,58 @@
+;; pgocaml.el - Proof General for OCaml scripts.
+;;
+;; David Aspinall.  $Id$
+;;
+;; This instance of PG is handy just for using script management to
+;; cut-and-paste into a buffer running OCaml
+;;
+;; 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 ".pgml" 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)
-- 
cgit v1.2.3