bin/isabelle
changeset 3183 537f7281d42c
parent 3118 24dae6222579
child 3184 4e0bbfb113d5
equal deleted inserted replaced
3182:3270d7bca923 3183:537f7281d42c
    24   echo "  Options are:"
    24   echo "  Options are:"
    25   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    25   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    26   echo "    -m MODE      add print mode for output"
    26   echo "    -m MODE      add print mode for output"
    27   echo "    -q           non-interactive session"
    27   echo "    -q           non-interactive session"
    28   echo "    -r           open heap file read-only"
    28   echo "    -r           open heap file read-only"
    29   echo "    -u           pass 'exit_use_dir\".\";' to the ML session"
       
    30   echo
    29   echo
    31   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    30   echo "  INPUT (default \"$DEFAULT_LOGIC\") and OUTPUT specify in/out heaps."
    32   echo "  These are either names to be searched in the Isabelle path, or actual"
    31   echo "  These are either names to be searched in the Isabelle path, or actual"
    33   echo "  file names (then containing at least one /)."
    32   echo "  file names (then containing at least one /)."
    34   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    33   echo "  If INPUT is \"RAW_ML_SYSTEM\", just start the bare bones ML system."
    50 MLTEXT=""
    49 MLTEXT=""
    51 MODES=""
    50 MODES=""
    52 TERMINATE=""
    51 TERMINATE=""
    53 READONLY=""
    52 READONLY=""
    54 
    53 
    55 while getopts "e:m:qru" OPT
    54 while getopts "e:m:qr" OPT
    56 do
    55 do
    57   case "$OPT" in
    56   case "$OPT" in
    58     e)
    57     e)
    59       MLTEXT="$MLTEXT $OPTARG"
    58       MLTEXT="$MLTEXT $OPTARG"
    60       ;;
    59       ;;
    68     q)
    67     q)
    69       TERMINATE=true
    68       TERMINATE=true
    70       ;;
    69       ;;
    71     r)
    70     r)
    72       READONLY=true
    71       READONLY=true
    73       ;;
       
    74     u)
       
    75       MLTEXT="$MLTEXT exit_use_dir\".\";"
       
    76       ;;
    72       ;;
    77     \?)
    73     \?)
    78       usage
    74       usage
    79       ;;
    75       ;;
    80   esac
    76   esac