bin/isabelle-process
changeset 14712 81362115cedd
parent 11550 915c5de6480f
child 14981 e73f8140af78
equal deleted inserted replaced
14711:521aa281808a 14712:81362115cedd
    25   echo
    25   echo
    26   echo "  Options are:"
    26   echo "  Options are:"
    27   echo "    -C           tell ML system to copy output image"
    27   echo "    -C           tell ML system to copy output image"
    28   echo "    -I           startup Isar interaction mode"
    28   echo "    -I           startup Isar interaction mode"
    29   echo "    -P           startup Proof General interaction mode"
    29   echo "    -P           startup Proof General interaction mode"
       
    30   echo "    -X           startup PGIP interaction mode"
    30   echo "    -c           tell ML system to compress output image"
    31   echo "    -c           tell ML system to compress output image"
    31   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    32   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    32   echo "    -f           pass 'Session.finish();' to the ML session"
    33   echo "    -f           pass 'Session.finish();' to the ML session"
    33   echo "    -m MODE      add print mode for output"
    34   echo "    -m MODE      add print mode for output"
    34   echo "    -q           non-interactive session"
    35   echo "    -q           non-interactive session"
    63 MODES=""
    64 MODES=""
    64 TERMINATE=""
    65 TERMINATE=""
    65 READONLY=""
    66 READONLY=""
    66 NOWRITE=""
    67 NOWRITE=""
    67 
    68 
    68 while getopts "CIPce:fm:qruw" OPT
    69 while getopts "XCIPce:fm:qruw" OPT
    69 do
    70 do
    70   case "$OPT" in
    71   case "$OPT" in
    71     C)
    72     C)
    72       COPYDB=true
    73       COPYDB=true
    73       ;;
    74       ;;
    74     I)
    75     I)
    75       ISAR=true
    76       ISAR=true
    76       ;;
    77       ;;
    77     P)
    78     P)
    78       PROOFGENERAL=true
    79       PROOFGENERAL=true
       
    80       ;;
       
    81     X)
       
    82       PGIP=true
    79       ;;
    83       ;;
    80     c)
    84     c)
    81       COMPRESS=true
    85       COMPRESS=true
    82       ;;
    86       ;;
    83     e)
    87     e)
   200 
   204 
   201 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   205 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-)
   202 
   206 
   203 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   207 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   204 
   208 
   205 if [ -n "$PROOFGENERAL" ]; then
   209 if [ -n "$PGIP" ]; then
       
   210   MLTEXT="$MLTEXT; ProofGeneral.init_pgip $ISAR;"
       
   211 elif [ -n "$PROOFGENERAL" ]; then
   206   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   212   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   207 elif [ "$ISAR" = true ]; then
   213 elif [ "$ISAR" = true ]; then
   208   MLTEXT="$MLTEXT; Isar.main();"
   214   MLTEXT="$MLTEXT; Isar.main();"
   209 fi
   215 fi
   210 
   216