Trivial instance of PG for shell scripts.

2 files changed, 63 insertions, 0 deletions

diff --git a/pgshell/example.pgsh b/pgshell/example.pgsh
new file mode 100644
index 00000000..d7f860e5
--- /dev/null
+++ b/pgshell/example.pgsh
@@ -0,0 +1,34 @@
+# This is an example shell script for processing 
+# with the script management of Proof General.
+#
+# It demonstrates the usefulness of PG simply for
+# sending a pre-defined sequence of commands to
+# some command-line interpreter, here /bin/sh.
+#
+# To adjust this for your needs, edit pgshell.el
+# (or copy and rename it).
+#
+# $Id$
+#
+
+# What time is it?
+date;
+
+# What machine am I on?
+uname -a;
+
+# What files are here?
+ls 
+   -lt;
+
+# Notes:
+#
+# * Commands have to be terminated by ';'.  Alternative is to write 
+#   your own scanner to recognize the start of the next command.
+#
+
+
+
+
+
+
diff --git a/pgshell/pgshell.el b/pgshell/pgshell.el
new file mode 100644
index 00000000..fe356432
--- /dev/null
+++ b/pgshell/pgshell.el
@@ -0,0 +1,29 @@
+;; pgshell.el - Proof General for shell scripts.
+;;
+;; David Aspinall.  $Id$
+;;
+;; This instance of PG is handy just for using script management to
+;; cut-and-paste into a buffer running an ordinary shell of some kind.
+;;
+;; I'm providing this so that tool demonstrators may use it instead of
+;; tediously doing cut-and-paste of commands from a file.  Nothing
+;; to do with theorem proving really!
+;;
+;; To use this instance of PG, visit a file with the ".pgsh" extension.
+;; 
+;; Feedback welcome.
+
+
+(require 'proof-easy-config)           
+(require 'proof-syntax)
+
+(proof-easy-config  'pgshell	"PG-Shell"
+ proof-prog-name		 "/bin/sh" ;; or choose your shell
+ proof-terminal-char             ?\;	   ;; better: parse the syntax
+ proof-script-comment-start      "\#"
+ proof-shell-annotated-prompt-regexp  "^.*[$] $" ;; matches shell prompts
+ ;; next settings are just to prevent warnings
+ proof-save-command-regexp	proof-no-regexp
+ )
+
+(provide 'pgshell)