--- a/lib/scripts/feeder Fri Nov 09 00:00:53 2001 +0100
+++ b/lib/scripts/feeder Fri Nov 09 00:01:55 2001 +0100
@@ -21,7 +21,6 @@
echo " -h TEXT head text"
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."
@@ -43,10 +42,9 @@
HEAD=""
EMITPID=""
QUIT=""
-SYMBOLS=""
TAIL=""
-while getopts "h:pqst:" OPT
+while getopts "h:pqt:" OPT
do
case "$OPT" in
h)
@@ -58,9 +56,6 @@
q)
QUIT=true
;;
- s)
- SYMBOLS=true
- ;;
t)
TAIL="$OPTARG"
;;
@@ -84,4 +79,4 @@
#set by configure
AUTO_PERL=perl
-exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
+exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"
--- a/lib/scripts/feeder.pl Fri Nov 09 00:00:53 2001 +0100
+++ b/lib/scripts/feeder.pl Fri Nov 09 00:01:55 2001 +0100
@@ -8,111 +8,7 @@
# args
-($head, $emitpid, $quit, $symbols, $tail) = @ARGV;
-
-
-# symbols translation table
-
-%tab = (
-#GENERATED TEXT FOLLOWS - Do not edit!
- "\xa0", "\\<spacespace>",
- "\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", "\\<frown>",
- "\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
-);
+($head, $emitpid, $quit, $tail) = @ARGV;
# setup signal handlers
@@ -134,7 +30,6 @@
if (!$quit) {
while (<STDIN>) {
- $symbols && (s/([\xa1-\xff])/\\$tab{$1}/g);
print;
}
}
--- a/lib/scripts/run-mlworks Fri Nov 09 00:00:53 2001 +0100
+++ b/lib/scripts/run-mlworks Fri Nov 09 00:01:55 2001 +0100
@@ -42,7 +42,7 @@
MLEXIT="commit();"
if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS="-s"
+ FEEDER_OPTS=""
else
FEEDER_OPTS="-q"
fi
--- a/lib/scripts/run-polyml Fri Nov 09 00:00:53 2001 +0100
+++ b/lib/scripts/run-polyml Fri Nov 09 00:01:55 2001 +0100
@@ -99,7 +99,7 @@
## run it!
if [ -z "$TERMINATE" ]; then
- FEEDER_OPTS="-s"
+ FEEDER_OPTS=""
else
FEEDER_OPTS="-q"
fi
--- a/lib/scripts/symbolinput.pl Fri Nov 09 00:00:53 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-#
-# $Id$
-# Author: Markus Wenzel, TU Muenchen
-# License: GPL (GNU GENERAL PUBLIC LICENSE)
-#
-# symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences.
-#
-
-%tab = (
-#GENERATED TEXT FOLLOWS - Do not edit!
- "\xa0", "\\<spacespace>",
- "\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", "\\<frown>",
- "\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
-);
-
-$SIG{INT} = "IGNORE";
-$| = 1;
-
-while (<ARGV>) {
- s/([\xa1-\xff])/\\$tab{$1}/g;
- print;
-}