bin/isatool
changeset 9786 270ca580b880
parent 7971 023778c8a029
child 10511 efb3428c9879
equal deleted inserted replaced
9785:1634fdb11b00 9786:270ca580b880
     1 #!/bin/bash
     1 #!/bin/bash
     2 #
     2 #
     3 # $Id$
     3 # $Id$
       
     4 # Author: Markus Wenzel, TU Muenchen
       
     5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
     4 #
     6 #
     5 # Isabelle tool starter -- provides settings environment,
     7 # Isabelle tool starter -- provides settings environment
     6 #   and keeps your PATH name space clean.
     8 # and keeps your PATH name space clean.
     7 
     9 
     8 
    10 
     9 ## settings
    11 ## settings
    10 
    12 
    11 PRG=$(basename $0)
    13 PRG=$(basename "$0")
    12 
    14 
    13 ISABELLE_HOME=$(dirname $0)/..
    15 ISABELLE_HOME=$(dirname "$0")/..
    14 . $ISABELLE_HOME/lib/scripts/getsettings || \
    16 . "$ISABELLE_HOME/lib/scripts/getsettings" || \
    15   { echo "$PRG probably not called from its original place!"; exit 2; }
    17   { echo "$PRG probably not called from its original place!"; exit 2; }
    16 
    18 
    17 
    19 
    18 ## diagnostics
    20 ## diagnostics
    19 
       
    20 TOOLDIRS=$(echo $ISABELLE_TOOLS | tr : " ")
       
    21 
    21 
    22 function usage()
    22 function usage()
    23 {
    23 {
    24   echo
    24   echo
    25   echo "Usage: $PRG TOOL [ARGS ...]"
    25   echo "Usage: $PRG TOOL [ARGS ...]"
    27   echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
    27   echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
    28   echo "  for more specific help."
    28   echo "  for more specific help."
    29   echo
    29   echo
    30   echo "  Available tools are:"
    30   echo "  Available tools are:"
    31   (
    31   (
    32     for DIR in $TOOLDIRS
    32     ORIG_IFS="$IFS"
       
    33     IFS=":"
       
    34     for DIR in $ISABELLE_TOOLS
    33     do
    35     do
    34       cd $DIR
    36       cd "$DIR"
    35       echo
    37       echo
    36       for T in *
    38       for T in *
    37       do
    39       do
    38         if [ -f "$T" -a -x "$T" ]; then
    40         if [ -f "$T" -a -x "$T" ]; then
    39           DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
    41           DESCRLINE=$(grep DESCRIPTION: "$T" | sed -e 's/^.*DESCRIPTION: *//')
    40           echo "    $T - $DESCRLINE"
    42           echo "    $T - $DESCRLINE"
    41         fi
    43         fi
    42       done
    44       done
    43     done
    45     done
       
    46     IFS="$ORIG_IFS"
    44   )
    47   )
    45   echo
    48   echo
    46   exit 1
    49   exit 1
    47 }
    50 }
    48 
    51 
    53 }
    56 }
    54 
    57 
    55 
    58 
    56 ## args
    59 ## args
    57 
    60 
    58 [ $# -lt 1 -o "$1" = "-?" ] && usage
    61 [ "$#" -lt 1 -o "$1" = "-?" ] && usage
    59 
    62 
    60 TOOLNAME="$1"
    63 TOOLNAME="$1"
    61 shift
    64 shift
    62 
    65 
    63 
    66 
    64 ## main
    67 ## main
    65 
    68 
    66 for DIR in $TOOLDIRS
    69 ORIG_IFS="$IFS"
       
    70 IFS=":"
       
    71 for DIR in $ISABELLE_TOOLS
    67 do
    72 do
    68   TOOL=$DIR/$TOOLNAME
    73   TOOL="$DIR/$TOOLNAME"
    69   [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
    74   [ -f "$TOOL" -a -x "$TOOL" ] && exec "$TOOL" "$@"
    70 done
    75 done
       
    76 IFS="$ORIG_IFS"
    71 
    77 
    72 fail "Unknown Isabelle tool: $TOOLNAME"
    78 fail "Unknown Isabelle tool: $TOOLNAME"