# HG changeset patch
# User wenzelm
# Date 883427962 -3600
# Node ID 5f629ee2502bab7cdcb98743635bcd5d3935365b
# Parent  db49bac6256a0c7d1dd1e7c1645c0c7d073cc25e
feed isabelle session;

diff -r db49bac6256a -r 5f629ee2502b lib/scripts/feeder
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/feeder	Mon Dec 29 21:39:22 1997 +0100
@@ -0,0 +1,87 @@
+#!/bin/bash
+#
+# $Id$
+#
+# feeder - feed isabelle session
+
+
+## diagnostics
+
+PRG=$(basename $0)
+DIR=$(dirname $0)
+
+function usage()
+{
+  echo
+  echo "Usage: $PRG [OPTIONS]"
+  echo
+  echo "  Options are:"
+  echo "    -h TEXT      head text"
+  echo "    -i           ignore INT signal"
+  echo "    -p           emit my pid"
+  echo "    -q           do not pipe stdin"
+  echo "    -s           filter symbols"
+  echo "    -t TEXT      tail text"
+  echo
+  echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
+  echo
+  exit 1
+}
+
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
+
+
+## process command line
+
+# options
+
+HEAD=""
+NOINT=""
+EMITPID=""
+QUIT=""
+SYMBOLS=""
+TAIL=""
+
+while getopts "h:ipqst:" OPT
+do
+  case "$OPT" in
+    h)
+      HEAD="$OPTARG"
+      ;;
+    i)
+      NOINT=true
+      ;;
+    p)
+      EMITPID=true
+      ;;
+    q)
+      QUIT=true
+      ;;
+    s)
+      SYMBOLS=true
+      ;;
+    t)
+      TAIL="$OPTARG"
+      ;;
+    \?)
+      usage
+      ;;
+  esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+[ $# -ne 0 ] && { echo "Bad args: $*"; usage; }
+
+
+
+## main
+
+exec perl -w $DIR/feeder.pl "$HEAD" "$NOINT" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
diff -r db49bac6256a -r 5f629ee2502b lib/scripts/feeder.pl
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/feeder.pl	Mon Dec 29 21:39:22 1997 +0100
@@ -0,0 +1,151 @@
+#
+# $Id$
+#
+# feeder.pl - feed isabelle session
+#
+
+# args
+
+($head, $noint, $emitpid, $quit, $symbols, $tail) = @ARGV;
+
+
+# symbols translation table
+
+%tab = (
+#GENERATED TEXT FOLLOWS - Do not edit!
+  "\xa0", "\\<space2>",
+  "\xa1", "\\<Gamma>",
+  "\xa2", "\\<Delta>",
+  "\xa3", "\\<Theta>",
+  "\xa4", "\\<Lambda>",
+  "\xa5", "\\<Pi>",
+  "\xa6", "\\<Sigma>",
+  "\xa7", "\\<Phi>",
+  "\xa8", "\\<Psi>",
+  "\xa9", "\\<Omega>",
+  "\xaa", "\\<alpha>",
+  "\xab", "\\<beta>",
+  "\xac", "\\<gamma>",
+  "\xad", "\\<delta>",
+  "\xae", "\\<epsilon>",
+  "\xaf", "\\<zeta>",
+  "\xb0", "\\<eta>",
+  "\xb1", "\\<theta>",
+  "\xb2", "\\<kappa>",
+  "\xb3", "\\<lambda>",
+  "\xb4", "\\<mu>",
+  "\xb5", "\\<nu>",
+  "\xb6", "\\<xi>",
+  "\xb7", "\\<pi>",
+  "\xb8", "\\<rho>",
+  "\xb9", "\\<sigma>",
+  "\xba", "\\<tau>",
+  "\xbb", "\\<phi>",
+  "\xbc", "\\<chi>",
+  "\xbd", "\\<psi>",
+  "\xbe", "\\<omega>",
+  "\xbf", "\\<not>",
+  "\xc0", "\\<and>",
+  "\xc1", "\\<or>",
+  "\xc2", "\\<forall>",
+  "\xc3", "\\<exists>",
+  "\xc4", "\\<And>",
+  "\xc5", "\\<lceil>",
+  "\xc6", "\\<rceil>",
+  "\xc7", "\\<lfloor>",
+  "\xc8", "\\<rfloor>",
+  "\xc9", "\\<turnstile>",
+  "\xca", "\\<Turnstile>",
+  "\xcb", "\\<lbrakk>",
+  "\xcc", "\\<rbrakk>",
+  "\xcd", "\\<cdot>",
+  "\xce", "\\<in>",
+  "\xcf", "\\<subseteq>",
+  "\xd0", "\\<inter>",
+  "\xd1", "\\<union>",
+  "\xd2", "\\<Inter>",
+  "\xd3", "\\<Union>",
+  "\xd4", "\\<sqinter>",
+  "\xd5", "\\<squnion>",
+  "\xd6", "\\<Sqinter>",
+  "\xd7", "\\<Squnion>",
+  "\xd8", "\\<bottom>",
+  "\xd9", "\\<doteq>",
+  "\xda", "\\<equiv>",
+  "\xdb", "\\<noteq>",
+  "\xdc", "\\<sqsubset>",
+  "\xdd", "\\<sqsubseteq>",
+  "\xde", "\\<prec>",
+  "\xdf", "\\<preceq>",
+  "\xe0", "\\<succ>",
+  "\xe1", "\\<approx>",
+  "\xe2", "\\<sim>",
+  "\xe3", "\\<simeq>",
+  "\xe4", "\\<le>",
+  "\xe5", "\\<Colon>",
+  "\xe6", "\\<leftarrow>",
+  "\xe7", "\\<midarrow>",
+  "\xe8", "\\<rightarrow>",
+  "\xe9", "\\<Leftarrow>",
+  "\xea", "\\<Midarrow>",
+  "\xeb", "\\<Rightarrow>",
+  "\xec", "\\<bow>",
+  "\xed", "\\<mapsto>",
+  "\xee", "\\<leadsto>",
+  "\xef", "\\<up>",
+  "\xf0", "\\<down>",
+  "\xf1", "\\<notin>",
+  "\xf2", "\\<times>",
+  "\xf3", "\\<oplus>",
+  "\xf4", "\\<ominus>",
+  "\xf5", "\\<otimes>",
+  "\xf6", "\\<oslash>",
+  "\xf7", "\\<subset>",
+  "\xf8", "\\<infinity>",
+  "\xf9", "\\<box>",
+  "\xfa", "\\<diamond>",
+  "\xfb", "\\<circ>",
+  "\xfc", "\\<bullet>",
+  "\xfd", "\\<parallel>",
+  "\xfe", "\\<surd>",
+  "\xff", "\\<copyright>"
+#END OF GENERATED TEXT
+);
+
+
+# setup hangup handler
+
+sub hangup {
+    exit(0);
+}
+
+$SIG{'HUP'} = "hangup";
+
+
+# main
+
+#bulletproof session
+$noint && ($SIG{INT} = "IGNORE");
+
+#buffer lines
+$| = 1;
+
+
+$emitpid && (print $$, "\n");
+
+$head && (print "$head", "\n");
+
+if (!$quit) {
+    while (<STDIN>) {
+	$symbols && (s/([\xa1-\xff])/\\$tab{$1}/g);
+	print;
+    }
+}
+
+$tail && (print "$tail", "\n");
+
+
+# wait forever, expecting to be terminated by HUP
+
+close STDOUT;
+sleep;