bin/isabelle-process
changeset 25523 08b0feb07239
parent 25504 dc960d760052
child 25645 b2ed983a5e80
equal deleted inserted replaced
25522:26851f8bdf14 25523:08b0feb07239
    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 "    -S           secure mode -- disallow critical operations"
    33   echo "    -S           secure mode -- disallow critical operations"
    34   echo "    -X           startup PGIP interaction mode"
    34   echo "    -X           startup PGIP interaction mode"
       
    35   echo "    -W           startup process wrapper (interaction via external program)"
    35   echo "    -c           tell ML system to compress output image"
    36   echo "    -c           tell ML system to compress output image"
    36   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    37   echo "    -e MLTEXT    pass MLTEXT to the ML session"
    37   echo "    -f           pass 'Session.finish();' to the ML session"
    38   echo "    -f           pass 'Session.finish();' to the ML session"
    38   echo "    -m MODE      add print mode for output"
    39   echo "    -m MODE      add print mode for output"
    39   echo "    -p           echo ISABELLE_PID on startup"
       
    40   echo "    -q           non-interactive session"
    40   echo "    -q           non-interactive session"
    41   echo "    -r           open heap file read-only"
    41   echo "    -r           open heap file read-only"
    42   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    42   echo "    -u           pass 'use\"ROOT.ML\";' to the ML session"
    43   echo "    -w           reset write permissions on OUTPUT"
    43   echo "    -w           reset write permissions on OUTPUT"
    44   echo
    44   echo
    63 
    63 
    64 COPYDB=""
    64 COPYDB=""
    65 ISAR=false
    65 ISAR=false
    66 PROOFGENERAL=""
    66 PROOFGENERAL=""
    67 SECURE=""
    67 SECURE=""
       
    68 WRAPPER=""
       
    69 PGIP=""
    68 COMPRESS=""
    70 COMPRESS=""
    69 MLTEXT=""
    71 MLTEXT=""
    70 MODES=""
    72 MODES=""
    71 ECHOPID=""
       
    72 TERMINATE=""
    73 TERMINATE=""
    73 READONLY=""
    74 READONLY=""
    74 NOWRITE=""
    75 NOWRITE=""
    75 
    76 
    76 while getopts "XCIPSce:fm:pqruw" OPT
    77 while getopts "CIPSWXce:fm:qruw" OPT
    77 do
    78 do
    78   case "$OPT" in
    79   case "$OPT" in
    79     C)
    80     C)
    80       COPYDB=true
    81       COPYDB=true
    81       ;;
    82       ;;
    85     P)
    86     P)
    86       PROOFGENERAL=true
    87       PROOFGENERAL=true
    87       ;;
    88       ;;
    88     S)
    89     S)
    89       SECURE=true
    90       SECURE=true
       
    91       ;;
       
    92     W)
       
    93       WRAPPER=true
    90       ;;
    94       ;;
    91     X)
    95     X)
    92       PGIP=true
    96       PGIP=true
    93       ;;
    97       ;;
    94     c)
    98     c)
   104       if [ -z "$MODES" ]; then
   108       if [ -z "$MODES" ]; then
   105         MODES="\"$OPTARG\""
   109         MODES="\"$OPTARG\""
   106       else
   110       else
   107         MODES="\"$OPTARG\", $MODES"
   111         MODES="\"$OPTARG\", $MODES"
   108       fi
   112       fi
   109       ;;
       
   110     p)
       
   111       ECHOPID=true
       
   112       ;;
   113       ;;
   113     q)
   114     q)
   114       TERMINATE=true
   115       TERMINATE=true
   115       ;;
   116       ;;
   116     r)
   117     r)
   219 
   220 
   220 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   221 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT"
   221 
   222 
   222 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   223 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();"
   223 
   224 
   224 if [ -n "$PGIP" ]; then
   225 if [ -n "$WRAPPER" ]; then
       
   226   MLTEXT="$MLTEXT; IsabelleProcess.init();"
       
   227 elif [ -n "$PGIP" ]; then
   225   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   228   MLTEXT="$MLTEXT; ProofGeneralPgip.init_pgip $ISAR;"
   226 elif [ -n "$PROOFGENERAL" ]; then
   229 elif [ -n "$PROOFGENERAL" ]; then
   227   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   230   MLTEXT="$MLTEXT; ProofGeneral.init $ISAR;"
   228 elif [ "$ISAR" = true ]; then
   231 elif [ "$ISAR" = true ]; then
   229   MLTEXT="$MLTEXT; Isar.main();"
   232   MLTEXT="$MLTEXT; Isar.main();"
   230 fi
   233 fi
   231 
   234 
   232 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
   235 export INFILE OUTFILE COPYDB COMPRESS MLTEXT TERMINATE NOWRITE \
   233   ISABELLE_PID ISABELLE_TMP
   236   ISABELLE_PID ISABELLE_TMP
   234 
   237 
   235 [ -n "$ECHOPID" ] && echo "ISABELLE_PID=$ISABELLE_PID"
       
   236 
       
   237 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   238 if [ -f "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM" ]; then
   238   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   239   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM"
   239 else
   240 else
   240   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   241   "$ISABELLE_HOME/lib/scripts/run-$ML_SYSTEM_BASE"
   241 fi
   242 fi