# HG changeset patch
# User wenzelm
# Date 1285186465 -7200
# Node ID 34952c2423c6efe895460335b1223e4087fc88a7
# Parent  1776b55f8d7a7b74cbe193162788c1b484dbbdf7
isabelle-process: less verbose no-commit mode;

diff -r 1776b55f8d7a -r 34952c2423c6 lib/scripts/run-polyml
--- 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=""
diff -r 1776b55f8d7a -r 34952c2423c6 lib/scripts/run-smlnj
--- 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=""