# HG changeset patch
# User wenzelm
# Date 1165612640 -3600
# Node ID dfac729d306650781273b5d25ce44fb957f440f4
# Parent  4e4b7c801142911e6e7a27a939a4d11de1b45679
root function: restore default interrupt handler;
output file: avoid .exe (e.g. for Cygwin);

diff -r 4e4b7c801142 -r dfac729d3066 Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0
--- a/Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0	Fri Dec 08 18:22:28 2006 +0100
+++ b/Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0	Fri Dec 08 22:17:20 2006 +0100
@@ -51,13 +51,15 @@
   EXIT=""
 fi
 
+ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
+
 if [ -z "$OUTFILE" ]; then
   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
 else
   if [ -z "$COMPRESS" ]; then
-    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
+    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
   else
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   rm -f "${OUTFILE}.o" || fail_out
@@ -83,6 +85,7 @@
   if [ -e "${OUTFILE}.o" ]; then
     cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
     rm -f "${OUTFILE}.o"
+    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
   fi
   [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 fi
diff -r 4e4b7c801142 -r dfac729d3066 lib/scripts/run-polyml-5.0
--- a/lib/scripts/run-polyml-5.0	Fri Dec 08 18:22:28 2006 +0100
+++ b/lib/scripts/run-polyml-5.0	Fri Dec 08 22:17:20 2006 +0100
@@ -51,13 +51,15 @@
   EXIT=""
 fi
 
+ROOT_FUNCTION="fn () => (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.rootFunction ())"
+
 if [ -z "$OUTFILE" ]; then
   COMMIT='fun commit () = (TextIO.output (TextIO.stdErr, "Error - Database is not opened for writing.\n"); false);'
 else
   if [ -z "$COMPRESS" ]; then
-    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
+    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
   else
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   rm -f "${OUTFILE}.o" || fail_out
@@ -83,6 +85,7 @@
   if [ -e "${OUTFILE}.o" ]; then
     cc -o "$OUTFILE" "${OUTFILE}.o" -L"$POLYLIB" -lpolymain -lpolyml -lstdc++ || fail_out
     rm -f "${OUTFILE}.o"
+    [ -e "${OUTFILE}.exe" ] && mv "${OUTFILE}.exe" "$OUTFILE"
   fi
   [ -f "$OUTFILE" -a -n "$NOWRITE" ] && chmod -w "$OUTFILE"
 fi