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.
proper Session.save with shutdown, which is relevant to avoid persistent threads;
authorwenzelm
Sat, 10 Jan 2015 21:22:25 +0100
changeset 59344 e0ce214303c1
parent 59343 43281cd62cb0
child 59345 b02b1fbcf051
proper Session.save with shutdown, which is relevant to avoid persistent threads;
lib/scripts/run-polyml file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.5.1 file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.5.2 file | annotate | diff | comparison | revisions
lib/scripts/run-polyml-5.5.3 file | annotate | diff | comparison | revisions
lib/scripts/run-smlnj file | annotate | diff | comparison | revisions
src/Pure/PIDE/session.ML file | annotate | diff | comparison | revisions 
--- a/lib/scripts/run-polyml	Sat Jan 10 20:28:53 2015 +0100
+++ b/lib/scripts/run-polyml	Sat Jan 10 21:22:25 2015 +0100
@@ -49,22 +49,20 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = false;'
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
   else
-    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+    MLEXIT="Session.save \"$OUTFILE\";"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
-MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+MLTEXT="$INIT $EXIT $MLTEXT"
 
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""
--- a/lib/scripts/run-polyml-5.5.1	Sat Jan 10 20:28:53 2015 +0100
+++ b/lib/scripts/run-polyml-5.5.1	Sat Jan 10 21:22:25 2015 +0100
@@ -50,22 +50,20 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = false;'
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
   else
-    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+    MLEXIT="Session.save \"$OUTFILE\";"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
-MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+MLTEXT="$INIT $EXIT $MLTEXT"
 
 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
   "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
--- a/lib/scripts/run-polyml-5.5.2	Sat Jan 10 20:28:53 2015 +0100
+++ b/lib/scripts/run-polyml-5.5.2	Sat Jan 10 21:22:25 2015 +0100
@@ -50,22 +50,20 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = false;'
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
   else
-    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+    MLEXIT="Session.save \"$OUTFILE\";"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
-MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+MLTEXT="$INIT $EXIT $MLTEXT"
 
 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
   "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
--- a/lib/scripts/run-polyml-5.5.3	Sat Jan 10 20:28:53 2015 +0100
+++ b/lib/scripts/run-polyml-5.5.3	Sat Jan 10 21:22:25 2015 +0100
@@ -50,22 +50,20 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = false;'
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    COMMIT="fun commit () = (PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
+    MLEXIT="(PolyML.shareCommonData PolyML.rootFunction; TextIO.output (TextIO.stdOut, \"Exporting $OUTFILE\n\"); PolyML.SaveState.saveState \"$OUTFILE\"; true) handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $OUTFILE\\n\"); Posix.Process.exit 0w1);"
   else
-    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+    MLEXIT="Session.save \"$OUTFILE\";"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
-MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
+MLTEXT="$INIT $EXIT $MLTEXT"
 
 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
   "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
--- a/lib/scripts/run-smlnj	Sat Jan 10 20:28:53 2015 +0100
+++ b/lib/scripts/run-smlnj	Sat Jan 10 21:22:25 2015 +0100
@@ -62,22 +62,20 @@
 fi
 
 if [ -z "$OUTFILE" ]; then
-  COMMIT='fun commit () = false;'
   MLEXIT=""
 else
   if [ -z "$INFILE" ]; then
-    COMMIT="fun commit () = if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
+    MLEXIT="if SMLofNJ.exportML \"$OUTFILE\" then () else OS.FileSys.rename {old = \"$OUTFILE.$ARCH-$OPSYS\", new = \"$OUTFILE\"};"
   else
-    COMMIT="fun commit () = (ML_System.share_common_data (); ML_System.save_state \"$OUTFILE\");"
+    MLEXIT="Session.save \"$OUTFILE\";"
   fi
   [ -f "$OUTFILE" ] && { chmod +w "$OUTFILE" || fail_out; }
-  MLEXIT="commit();"
 fi
 
 
 ## run it!
 
-MLTEXT="$EXIT $COMMIT $MLTEXT"
+MLTEXT="$EXIT $MLTEXT"
 
 if [ -z "$TERMINATE" ]; then
   FEEDER_OPTS=""
--- a/src/Pure/PIDE/session.ML	Sat Jan 10 20:28:53 2015 +0100
+++ b/src/Pure/PIDE/session.ML	Sat Jan 10 21:22:25 2015 +0100
@@ -12,6 +12,7 @@
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
     (Path.T * Path.T) list -> string -> string * string -> bool -> unit
   val finish: unit -> unit
+  val save: string -> unit
   val protocol_handler: string -> unit
   val init_protocol_handlers: unit -> unit
 end;
@@ -69,6 +70,14 @@
       (Thy_Info.get_names ()) Keyword.empty_keywords;
   session_finished := true);
 
+fun save heap =
+ (Execution.shutdown ();
+  Future.shutdown ();
+  Event_Timer.shutdown ();
+  Future.shutdown ();
+  ML_System.share_common_data ();
+  ML_System.save_state heap);
+
 
 
 (** protocol handlers **)
isabelle