1.1 --- a/lib/scripts/feeder	Fri Nov 09 00:00:53 2001 +0100
     1.2 +++ b/lib/scripts/feeder	Fri Nov 09 00:01:55 2001 +0100
     1.3 @@ -21,7 +21,6 @@
     1.4    echo "    -h TEXT      head text"
     1.5    echo "    -p           emit my pid"
     1.6    echo "    -q           do not pipe stdin"
     1.7 -  echo "    -s           filter symbols"
     1.8    echo "    -t TEXT      tail text"
     1.9    echo
    1.10    echo "  Output texts (pid, head, stdin, tail), then wait to be terminated."
    1.11 @@ -43,10 +42,9 @@
    1.12  HEAD=""
    1.13  EMITPID=""
    1.14  QUIT=""
    1.15 -SYMBOLS=""
    1.16  TAIL=""
    1.17  
    1.18 -while getopts "h:pqst:" OPT
    1.19 +while getopts "h:pqt:" OPT
    1.20  do
    1.21    case "$OPT" in
    1.22      h)
    1.23 @@ -58,9 +56,6 @@
    1.24      q)
    1.25        QUIT=true
    1.26        ;;
    1.27 -    s)
    1.28 -      SYMBOLS=true
    1.29 -      ;;
    1.30      t)
    1.31        TAIL="$OPTARG"
    1.32        ;;
    1.33 @@ -84,4 +79,4 @@
    1.34  #set by configure
    1.35  AUTO_PERL=perl
    1.36  
    1.37 -exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$SYMBOLS" "$TAIL"
    1.38 +exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"

     2.1 --- a/lib/scripts/feeder.pl	Fri Nov 09 00:00:53 2001 +0100
     2.2 +++ b/lib/scripts/feeder.pl	Fri Nov 09 00:01:55 2001 +0100
     2.3 @@ -8,111 +8,7 @@
     2.4  
     2.5  # args
     2.6  
     2.7 -($head, $emitpid, $quit, $symbols, $tail) = @ARGV;
     2.8 -
     2.9 -
    2.10 -# symbols translation table
    2.11 -
    2.12 -%tab = (
    2.13 -#GENERATED TEXT FOLLOWS - Do not edit!
    2.14 -  "\xa0", "\\<spacespace>",
    2.15 -  "\xa1", "\\<Gamma>",
    2.16 -  "\xa2", "\\<Delta>",
    2.17 -  "\xa3", "\\<Theta>",
    2.18 -  "\xa4", "\\<Lambda>",
    2.19 -  "\xa5", "\\<Pi>",
    2.20 -  "\xa6", "\\<Sigma>",
    2.21 -  "\xa7", "\\<Phi>",
    2.22 -  "\xa8", "\\<Psi>",
    2.23 -  "\xa9", "\\<Omega>",
    2.24 -  "\xaa", "\\<alpha>",
    2.25 -  "\xab", "\\<beta>",
    2.26 -  "\xac", "\\<gamma>",
    2.27 -  "\xad", "\\<delta>",
    2.28 -  "\xae", "\\<epsilon>",
    2.29 -  "\xaf", "\\<zeta>",
    2.30 -  "\xb0", "\\<eta>",
    2.31 -  "\xb1", "\\<theta>",
    2.32 -  "\xb2", "\\<kappa>",
    2.33 -  "\xb3", "\\<lambda>",
    2.34 -  "\xb4", "\\<mu>",
    2.35 -  "\xb5", "\\<nu>",
    2.36 -  "\xb6", "\\<xi>",
    2.37 -  "\xb7", "\\<pi>",
    2.38 -  "\xb8", "\\<rho>",
    2.39 -  "\xb9", "\\<sigma>",
    2.40 -  "\xba", "\\<tau>",
    2.41 -  "\xbb", "\\<phi>",
    2.42 -  "\xbc", "\\<chi>",
    2.43 -  "\xbd", "\\<psi>",
    2.44 -  "\xbe", "\\<omega>",
    2.45 -  "\xbf", "\\<not>",
    2.46 -  "\xc0", "\\<and>",
    2.47 -  "\xc1", "\\<or>",
    2.48 -  "\xc2", "\\<forall>",
    2.49 -  "\xc3", "\\<exists>",
    2.50 -  "\xc4", "\\<And>",
    2.51 -  "\xc5", "\\<lceil>",
    2.52 -  "\xc6", "\\<rceil>",
    2.53 -  "\xc7", "\\<lfloor>",
    2.54 -  "\xc8", "\\<rfloor>",
    2.55 -  "\xc9", "\\<turnstile>",
    2.56 -  "\xca", "\\<Turnstile>",
    2.57 -  "\xcb", "\\<lbrakk>",
    2.58 -  "\xcc", "\\<rbrakk>",
    2.59 -  "\xcd", "\\<cdot>",
    2.60 -  "\xce", "\\<in>",
    2.61 -  "\xcf", "\\<subseteq>",
    2.62 -  "\xd0", "\\<inter>",
    2.63 -  "\xd1", "\\<union>",
    2.64 -  "\xd2", "\\<Inter>",
    2.65 -  "\xd3", "\\<Union>",
    2.66 -  "\xd4", "\\<sqinter>",
    2.67 -  "\xd5", "\\<squnion>",
    2.68 -  "\xd6", "\\<Sqinter>",
    2.69 -  "\xd7", "\\<Squnion>",
    2.70 -  "\xd8", "\\<bottom>",
    2.71 -  "\xd9", "\\<doteq>",
    2.72 -  "\xda", "\\<equiv>",
    2.73 -  "\xdb", "\\<noteq>",
    2.74 -  "\xdc", "\\<sqsubset>",
    2.75 -  "\xdd", "\\<sqsubseteq>",
    2.76 -  "\xde", "\\<prec>",
    2.77 -  "\xdf", "\\<preceq>",
    2.78 -  "\xe0", "\\<succ>",
    2.79 -  "\xe1", "\\<approx>",
    2.80 -  "\xe2", "\\<sim>",
    2.81 -  "\xe3", "\\<simeq>",
    2.82 -  "\xe4", "\\<le>",
    2.83 -  "\xe5", "\\<Colon>",
    2.84 -  "\xe6", "\\<leftarrow>",
    2.85 -  "\xe7", "\\<midarrow>",
    2.86 -  "\xe8", "\\<rightarrow>",
    2.87 -  "\xe9", "\\<Leftarrow>",
    2.88 -  "\xea", "\\<Midarrow>",
    2.89 -  "\xeb", "\\<Rightarrow>",
    2.90 -  "\xec", "\\<frown>",
    2.91 -  "\xed", "\\<mapsto>",
    2.92 -  "\xee", "\\<leadsto>",
    2.93 -  "\xef", "\\<up>",
    2.94 -  "\xf0", "\\<down>",
    2.95 -  "\xf1", "\\<notin>",
    2.96 -  "\xf2", "\\<times>",
    2.97 -  "\xf3", "\\<oplus>",
    2.98 -  "\xf4", "\\<ominus>",
    2.99 -  "\xf5", "\\<otimes>",
   2.100 -  "\xf6", "\\<oslash>",
   2.101 -  "\xf7", "\\<subset>",
   2.102 -  "\xf8", "\\<infinity>",
   2.103 -  "\xf9", "\\<box>",
   2.104 -  "\xfa", "\\<diamond>",
   2.105 -  "\xfb", "\\<circ>",
   2.106 -  "\xfc", "\\<bullet>",
   2.107 -  "\xfd", "\\<parallel>",
   2.108 -  "\xfe", "\\<surd>",
   2.109 -  "\xff", "\\<copyright>"
   2.110 -#END OF GENERATED TEXT
   2.111 -);
   2.112 +($head, $emitpid, $quit, $tail) = @ARGV;
   2.113  
   2.114  
   2.115  # setup signal handlers
   2.116 @@ -134,7 +30,6 @@
   2.117  
   2.118  if (!$quit) {
   2.119      while (<STDIN>) {
   2.120 -	$symbols && (s/([\xa1-\xff])/\\$tab{$1}/g);
   2.121  	print;
   2.122      }
   2.123  }

     3.1 --- a/lib/scripts/run-mlworks	Fri Nov 09 00:00:53 2001 +0100
     3.2 +++ b/lib/scripts/run-mlworks	Fri Nov 09 00:01:55 2001 +0100
     3.3 @@ -42,7 +42,7 @@
     3.4  MLEXIT="commit();"
     3.5  
     3.6  if [ -z "$TERMINATE" ]; then
     3.7 -  FEEDER_OPTS="-s"
     3.8 +  FEEDER_OPTS=""
     3.9  else
    3.10    FEEDER_OPTS="-q"
    3.11  fi

     4.1 --- a/lib/scripts/run-polyml	Fri Nov 09 00:00:53 2001 +0100
     4.2 +++ b/lib/scripts/run-polyml	Fri Nov 09 00:01:55 2001 +0100
     4.3 @@ -99,7 +99,7 @@
     4.4  ## run it!
     4.5  
     4.6  if [ -z "$TERMINATE" ]; then
     4.7 -  FEEDER_OPTS="-s"
     4.8 +  FEEDER_OPTS=""
     4.9  else
    4.10    FEEDER_OPTS="-q"
    4.11  fi

     5.1 --- a/lib/scripts/symbolinput.pl	Fri Nov 09 00:00:53 2001 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,116 +0,0 @@
     5.4 -#
     5.5 -# $Id$
     5.6 -# Author: Markus Wenzel, TU Muenchen
     5.7 -# License: GPL (GNU GENERAL PUBLIC LICENSE)
     5.8 -#
     5.9 -# symbolinput.pl - expand isabelle-0 encoded chars to \<...> sequences.
    5.10 -#
    5.11 -
    5.12 -%tab = (
    5.13 -#GENERATED TEXT FOLLOWS - Do not edit!
    5.14 -  "\xa0", "\\<spacespace>",
    5.15 -  "\xa1", "\\<Gamma>",
    5.16 -  "\xa2", "\\<Delta>",
    5.17 -  "\xa3", "\\<Theta>",
    5.18 -  "\xa4", "\\<Lambda>",
    5.19 -  "\xa5", "\\<Pi>",
    5.20 -  "\xa6", "\\<Sigma>",
    5.21 -  "\xa7", "\\<Phi>",
    5.22 -  "\xa8", "\\<Psi>",
    5.23 -  "\xa9", "\\<Omega>",
    5.24 -  "\xaa", "\\<alpha>",
    5.25 -  "\xab", "\\<beta>",
    5.26 -  "\xac", "\\<gamma>",
    5.27 -  "\xad", "\\<delta>",
    5.28 -  "\xae", "\\<epsilon>",
    5.29 -  "\xaf", "\\<zeta>",
    5.30 -  "\xb0", "\\<eta>",
    5.31 -  "\xb1", "\\<theta>",
    5.32 -  "\xb2", "\\<kappa>",
    5.33 -  "\xb3", "\\<lambda>",
    5.34 -  "\xb4", "\\<mu>",
    5.35 -  "\xb5", "\\<nu>",
    5.36 -  "\xb6", "\\<xi>",
    5.37 -  "\xb7", "\\<pi>",
    5.38 -  "\xb8", "\\<rho>",
    5.39 -  "\xb9", "\\<sigma>",
    5.40 -  "\xba", "\\<tau>",
    5.41 -  "\xbb", "\\<phi>",
    5.42 -  "\xbc", "\\<chi>",
    5.43 -  "\xbd", "\\<psi>",
    5.44 -  "\xbe", "\\<omega>",
    5.45 -  "\xbf", "\\<not>",
    5.46 -  "\xc0", "\\<and>",
    5.47 -  "\xc1", "\\<or>",
    5.48 -  "\xc2", "\\<forall>",
    5.49 -  "\xc3", "\\<exists>",
    5.50 -  "\xc4", "\\<And>",
    5.51 -  "\xc5", "\\<lceil>",
    5.52 -  "\xc6", "\\<rceil>",
    5.53 -  "\xc7", "\\<lfloor>",
    5.54 -  "\xc8", "\\<rfloor>",
    5.55 -  "\xc9", "\\<turnstile>",
    5.56 -  "\xca", "\\<Turnstile>",
    5.57 -  "\xcb", "\\<lbrakk>",
    5.58 -  "\xcc", "\\<rbrakk>",
    5.59 -  "\xcd", "\\<cdot>",
    5.60 -  "\xce", "\\<in>",
    5.61 -  "\xcf", "\\<subseteq>",
    5.62 -  "\xd0", "\\<inter>",
    5.63 -  "\xd1", "\\<union>",
    5.64 -  "\xd2", "\\<Inter>",
    5.65 -  "\xd3", "\\<Union>",
    5.66 -  "\xd4", "\\<sqinter>",
    5.67 -  "\xd5", "\\<squnion>",
    5.68 -  "\xd6", "\\<Sqinter>",
    5.69 -  "\xd7", "\\<Squnion>",
    5.70 -  "\xd8", "\\<bottom>",
    5.71 -  "\xd9", "\\<doteq>",
    5.72 -  "\xda", "\\<equiv>",
    5.73 -  "\xdb", "\\<noteq>",
    5.74 -  "\xdc", "\\<sqsubset>",
    5.75 -  "\xdd", "\\<sqsubseteq>",
    5.76 -  "\xde", "\\<prec>",
    5.77 -  "\xdf", "\\<preceq>",
    5.78 -  "\xe0", "\\<succ>",
    5.79 -  "\xe1", "\\<approx>",
    5.80 -  "\xe2", "\\<sim>",
    5.81 -  "\xe3", "\\<simeq>",
    5.82 -  "\xe4", "\\<le>",
    5.83 -  "\xe5", "\\<Colon>",
    5.84 -  "\xe6", "\\<leftarrow>",
    5.85 -  "\xe7", "\\<midarrow>",
    5.86 -  "\xe8", "\\<rightarrow>",
    5.87 -  "\xe9", "\\<Leftarrow>",
    5.88 -  "\xea", "\\<Midarrow>",
    5.89 -  "\xeb", "\\<Rightarrow>",
    5.90 -  "\xec", "\\<frown>",
    5.91 -  "\xed", "\\<mapsto>",
    5.92 -  "\xee", "\\<leadsto>",
    5.93 -  "\xef", "\\<up>",
    5.94 -  "\xf0", "\\<down>",
    5.95 -  "\xf1", "\\<notin>",
    5.96 -  "\xf2", "\\<times>",
    5.97 -  "\xf3", "\\<oplus>",
    5.98 -  "\xf4", "\\<ominus>",
    5.99 -  "\xf5", "\\<otimes>",
   5.100 -  "\xf6", "\\<oslash>",
   5.101 -  "\xf7", "\\<subset>",
   5.102 -  "\xf8", "\\<infinity>",
   5.103 -  "\xf9", "\\<box>",
   5.104 -  "\xfa", "\\<diamond>",
   5.105 -  "\xfb", "\\<circ>",
   5.106 -  "\xfc", "\\<bullet>",
   5.107 -  "\xfd", "\\<parallel>",
   5.108 -  "\xfe", "\\<surd>",
   5.109 -  "\xff", "\\<copyright>"
   5.110 -#END OF GENERATED TEXT
   5.111 -);
   5.112 -
   5.113 -$SIG{INT} = "IGNORE";
   5.114 -$| = 1;
   5.115 -
   5.116 -while (<ARGV>) {
   5.117 -  s/([\xa1-\xff])/\\$tab{$1}/g;
   5.118 -  print;
   5.119 -}