# HG changeset patch
# User wenzelm
# Date 1420921345 -3600
# Node ID e0ce214303c120aeea9265a013af6922a1741802
# Parent  43281cd62cb00280d65399bbc617449348aaae25
proper Session.save with shutdown, which is relevant to avoid persistent threads;

diff -r 43281cd62cb0 -r e0ce214303c1 lib/scripts/run-polyml
--- 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=""
diff -r 43281cd62cb0 -r e0ce214303c1 lib/scripts/run-polyml-5.5.1
--- 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")" \
diff -r 43281cd62cb0 -r e0ce214303c1 lib/scripts/run-polyml-5.5.2
--- 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")" \
diff -r 43281cd62cb0 -r e0ce214303c1 lib/scripts/run-polyml-5.5.3
--- 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")" \
diff -r 43281cd62cb0 -r e0ce214303c1 lib/scripts/run-smlnj
--- 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=""
diff -r 43281cd62cb0 -r e0ce214303c1 src/Pure/PIDE/session.ML
--- 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 **)