bin/isabelle-process
changeset 16101 37471d84d353
parent 15967 f9163c6f69d6
child 16817 63a5782c764e
equal deleted inserted replaced
16100:f80fc4bff933 16101:37471d84d353
    28   echo
    28   echo
    29   echo "  Options are:"
    29   echo "  Options are:"
    30   echo "    -C           tell ML system to copy output image"
    30   echo "    -C           tell ML system to copy output image"
    31   echo "    -I           startup Isar interaction mode"
    31   echo "    -I           startup Isar interaction mode"
    32   echo "    -P           startup Proof General interaction mode"
    32   echo "    -P           startup Proof General interaction mode"
       
    33   echo "    -X           startup PGIP interaction mode"
    33   echo "    -c           tell ML system to compress output image"
    34   echo "    -c           tell ML system to compress output image"
    34   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    35   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    35   echo "    -f           pass 'Session.finish();' to the ML session"
    36   echo "    -f           pass 'Session.finish();' to the ML session"
    36   echo "    -m MODE      add print mode for output"
    37   echo "    -m MODE      add print mode for output"
    37   echo "    -q           non-interactive session"
    38   echo "    -q           non-interactive session"
    66 MODES=""
    67 MODES=""
    67 TERMINATE=""
    68 TERMINATE=""
    68 READONLY=""
    69 READONLY=""
    69 NOWRITE=""
    70 NOWRITE=""
    70 
    71 
    71 while getopts "CIPce:fm:qruw" OPT
    72 while getopts "XCIPce:fm:qruw" OPT
    72 do
    73 do
    73   case "$OPT" in
    74   case "$OPT" in
    74     C)
    75     C)
    75       COPYDB=true
    76       COPYDB=true
    76       ;;
    77       ;;
    77     I)
    78     I)
    78       ISAR=true
    79       ISAR=true
    79       ;;
    80       ;;
    80     P)
    81     P)
    81       PROOFGENERAL=true
    82       PROOFGENERAL=true
       
    83       ;;
       
    84     X)
       
    85       PGIP=true
    82       ;;
    86       ;;
    83     c)
    87     c)
    84       COMPRESS=true
    88       COMPRESS=true
    85       ;;
    89       ;;
    86     e)
    90     e)
   203 
   207 
   204 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   208 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   205 
   209 
   206 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   210 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   207 
   211 
   208 if [ -n "$PROOFGENERAL" ]; then
   212 if [ -n "$PGIP" ]; then
       
   213   MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;"
       
   214 elif [ -n "$PROOFGENERAL" ]; then
   209   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   215   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   210 elif [ "$ISAR" = true ]; then
   216 elif [ "$ISAR" = true ]; then
   211   MLTEXT="$MLTEXT; Isar.main();"
   217   MLTEXT="$MLTEXT; Isar.main();"
   212 fi
   218 fi
   213 
   219