Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
root function: restore default interrupt handler;
authorwenzelm
Fri, 08 Dec 2006 22:17:20 +0100
changeset 21711 dfac729d3066
parent 21710 4e4b7c801142
child 21712 8b2fd895a7fc
root function: restore default interrupt handler; output file: avoid .exe (e.g. for Cygwin);
Admin/Isabelle2005-polyml-5.0/lib/scripts/run-polyml-5.0 file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.0 file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle