isabelle-process: less verbose no-commit mode;
authorwenzelm
Wed, 22 Sep 2010 22:14:25 +0200
changeset 39619 34952c2423c6
parent 39618 1776b55f8d7a
child 39620 ff694044a55b
isabelle-process: less verbose no-commit mode;
lib/scripts/run-polyml
lib/scripts/run-smlnj
--- a/lib/scripts/run-polyml	Wed Sep 22 21:21:04 2010 +0200
+++ b/lib/scripts/run-polyml	Wed Sep 22 22:14:25 2010 +0200
@@ -52,17 +52,18 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
+  COMMIT='fun commit () = false;'
+  MLEXIT=""
 else
   COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true);"
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
 MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
 
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""
--- a/lib/scripts/run-smlnj	Wed Sep 22 21:21:04 2010 +0200
+++ b/lib/scripts/run-smlnj	Wed Sep 22 22:14:25 2010 +0200
@@ -57,17 +57,18 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
+  COMMIT='fun commit () = false;'
+  MLEXIT=""
 else
   COMMIT="fun commit () = not (SMLofNJ.exportML\"$OUTFILE\");"
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
+  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
 MLTEXT="$EXIT $COMMIT $MLTEXT"
-MLEXIT="commit();"
 
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""