# HG changeset patch # User wenzelm # Date 1456758767 -3600 # Node ID 6d292ee3036550176343eb86d32f5717ebb272d4 # Parent d97e13e5ea5b644351ac42ef43a56efad1d62693 save heap more directly; diff -r d97e13e5ea5b -r 6d292ee30365 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Mon Feb 29 15:39:17 2016 +0100 +++ b/src/Pure/PIDE/session.ML Mon Feb 29 16:12:47 2016 +0100 @@ -13,7 +13,6 @@ (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit val shutdown: unit -> unit val finish: unit -> unit - val save: string -> unit val protocol_handler: string -> unit val init_protocol_handlers: unit -> unit end; @@ -75,11 +74,6 @@ (Thy_Info.get_names ()) Keyword.empty_keywords; session_finished := true); -fun save heap = - (shutdown (); - ML_Heap.share_common_data (); - ML_Heap.save_state heap); - (** protocol handlers **) diff -r d97e13e5ea5b -r 6d292ee30365 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Mon Feb 29 15:39:17 2016 +0100 +++ b/src/Pure/Tools/build.ML Mon Feb 29 16:12:47 2016 +0100 @@ -124,15 +124,16 @@ let val _ = SHA1_Samples.test (); - val (symbol_codes, (command_timings, (do_output, (options, (verbose, (browser_info, + val (symbol_codes, (command_timings, (output, (options, (verbose, (browser_info, (document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in - pair (list (pair string int)) (pair (list properties) (pair bool (pair Options.decode + pair (list (pair string int)) (pair (list properties) (pair string (pair Options.decode (pair bool (pair string (pair (list (pair string string)) (pair string (pair string (pair string (pair string ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))) end; + val do_output = output <> ""; val symbols = HTML.make_symbols symbol_codes; val _ = Options.set_default options; @@ -165,7 +166,8 @@ val _ = Par_Exn.release_all [res1, res2]; val _ = Options.reset_default (); - val _ = if do_output then () else exit 0; + val _ = Session.shutdown (); + val _ = if do_output then (ML_Heap.share_common_data (); ML_Heap.save_state output) else (); in () end); diff -r d97e13e5ea5b -r 6d292ee30365 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Feb 29 15:39:17 2016 +0100 +++ b/src/Pure/Tools/build.scala Mon Feb 29 16:12:47 2016 +0100 @@ -541,6 +541,7 @@ browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T]) { def output_path: Option[Path] = if (do_output) Some(output) else None + def output_standard_path: String = if (do_output) File.standard_path(output) else "" private val parent = info.parent.getOrElse("") @@ -555,25 +556,25 @@ { val theories = info.theories.map(x => (x._2, x._3)) import XML.Encode._ - pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Options.encode, + pair(list(pair(string, int)), pair(list(properties), pair(string, pair(Options.encode, pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string, pair(string, pair(string, pair(string, list(pair(Options.encode, list(Path.encode))))))))))))))( - (Symbol.codes, (command_timings, (do_output, (info.options, + (Symbol.codes, (command_timings, (output_standard_path, (info.options, (verbose, (browser_info, (info.document_files, (File.standard_path(graph_file), (parent, (info.chapter, (name, theories)))))))))))) })) private val env = - Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output), + Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path, (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> File.standard_path(args_file)) private val script = if (is_pure(name)) { if (do_output) "./build " + name + " \"$OUTPUT\"" - else """ rm -f "$OUTPUT"; ./build """ + name + else "./build " + name } else { """ @@ -581,7 +582,7 @@ """ + (if (do_output) """ - "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" + "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" && chmod -w "$OUTPUT" """ else """ diff -r d97e13e5ea5b -r 6d292ee30365 src/Pure/build --- a/src/Pure/build Mon Feb 29 15:39:17 2016 +0100 +++ b/src/Pure/build Mon Feb 29 16:12:47 2016 +0100 @@ -64,11 +64,13 @@ -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ -q RAW_ML_SYSTEM else + rm -f "$OUTPUT" "$ISABELLE_PROCESS" \ -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \ -e "structure Isar = struct fun main () = () end;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ - -q -w RAW_ML_SYSTEM "$OUTPUT" + -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ + -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" fi else if [ -z "$OUTPUT" ]; then @@ -76,12 +78,15 @@ -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ -q RAW_ML_SYSTEM else + rm -f "$OUTPUT" "$ISABELLE_PROCESS" \ -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \ -e "ml_prompts \"ML> \" \"ML# \";" \ -e "Command_Line.tool0 Session.finish;" \ -e "Options.reset_default ();" \ - -q -w RAW_ML_SYSTEM "$OUTPUT" + -e "Session.shutdown ();" \ + -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \ + -q RAW_ML_SYSTEM && chmod -w "$OUTPUT" fi fi