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.
removed signal setup from root function to on-entry hook;
authorwenzelm
Thu, 16 Aug 2007 18:53:21 +0200
changeset 24296 3479a9fe73e0
parent 24295 af8dbc7a2305
child 24297 a50cdc42798d
removed signal setup from root function to on-entry hook;
lib/scripts/run-polyml-5.0 file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.1 file | annotate | diff | comparison | revisions
src/Pure/ML-Systems/polyml.ML file | annotate | diff | comparison | revisions 
--- a/lib/scripts/run-polyml-5.0	Thu Aug 16 18:53:21 2007 +0200
+++ b/lib/scripts/run-polyml-5.0	Thu Aug 16 18:53:21 2007 +0200
@@ -52,15 +52,13 @@
   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\", $ROOT_FUNCTION); true);"
+    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
   else
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   rm -f "${OUTFILE}.o" || fail_out
--- a/lib/scripts/run-polyml-5.1	Thu Aug 16 18:53:21 2007 +0200
+++ b/lib/scripts/run-polyml-5.1	Thu Aug 16 18:53:21 2007 +0200
@@ -52,15 +52,13 @@
   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\", $ROOT_FUNCTION); true);"
+    COMMIT="fun commit () = (TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
   else
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", $ROOT_FUNCTION); true);"
+    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.export (\"$OUTFILE\", PolyML.rootFunction); true);"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
   rm -f "${OUTFILE}.o" || fail_out
--- a/src/Pure/ML-Systems/polyml.ML	Thu Aug 16 18:53:21 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Aug 16 18:53:21 2007 +0200
@@ -111,7 +111,9 @@
   fun eval "-q" = ()
     | eval txt = use_text "" (println, println) false txt;
 in
-  val _ = PolyML.onEntry (fn () => app eval (CommandLine.arguments ()));
+  val _ = PolyML.onEntry (fn () =>
+   (Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ()));
+    app eval (CommandLine.arguments ())));
 end;
isabelle