lib/Tools/symbolinput
author paulson
Thu, 05 Jun 1997 13:22:25 +0200
changeset 3403 6cc663f6d62e
parent 3007 e5efa177ee0c
child 4508 f102cb0140fe
permissions -rwxr-xr-x
A slight simplification of optstring The new "simpset" keyword in the "recdef" declaration
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3007
e5efa177ee0c removed -norc;
wenzelm
parents: 2589
diff changeset
     1
#!/bin/bash
2399
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     2
#
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     3
# $Id$
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     4
#
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     5
# DESCRIPTION: translate symbols into \<...> sequences
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     6
#
2589
9d910f3681d0 now falls back on ucat instead of cat;
wenzelm
parents: 2399
diff changeset
     7
# NOTE: If perl is unavailable we simply fall back on ucat!
2399
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     8
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
     9
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    10
PERL=$(type -path perl)
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    11
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    12
if [ -z "$PERL" ]
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    13
then
2589
9d910f3681d0 now falls back on ucat instead of cat;
wenzelm
parents: 2399
diff changeset
    14
  exec $ISABELLE_HOME/lib/scripts/ucat "$@"
2399
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    15
else
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    16
  exec $PERL $ISABELLE_HOME/lib/scripts/symbolinput.pl "$@"
6719b465198b symbolinput - translate symbols into \<...> sequences;
wenzelm
parents:
diff changeset
    17
fi