save heap more directly;
authorwenzelm
Mon Feb 29 16:12:47 2016 +0100 (2016-02-29)
changeset 624696d292ee30365
parent 62468 d97e13e5ea5b
child 62470 9037ed690e19
save heap more directly;
src/Pure/PIDE/session.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
src/Pure/build
     1.1 --- a/src/Pure/PIDE/session.ML	Mon Feb 29 15:39:17 2016 +0100
     1.2 +++ b/src/Pure/PIDE/session.ML	Mon Feb 29 16:12:47 2016 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4      (Path.T * Path.T) list -> Path.T -> string -> string * string -> bool -> unit
     1.5    val shutdown: unit -> unit
     1.6    val finish: unit -> unit
     1.7 -  val save: string -> unit
     1.8    val protocol_handler: string -> unit
     1.9    val init_protocol_handlers: unit -> unit
    1.10  end;
    1.11 @@ -75,11 +74,6 @@
    1.12        (Thy_Info.get_names ()) Keyword.empty_keywords;
    1.13    session_finished := true);
    1.14  
    1.15 -fun save heap =
    1.16 - (shutdown ();
    1.17 -  ML_Heap.share_common_data ();
    1.18 -  ML_Heap.save_state heap);
    1.19 -
    1.20  
    1.21  
    1.22  (** protocol handlers **)
     2.1 --- a/src/Pure/Tools/build.ML	Mon Feb 29 15:39:17 2016 +0100
     2.2 +++ b/src/Pure/Tools/build.ML	Mon Feb 29 16:12:47 2016 +0100
     2.3 @@ -124,15 +124,16 @@
     2.4      let
     2.5        val _ = SHA1_Samples.test ();
     2.6  
     2.7 -      val (symbol_codes, (command_timings, (do_output, (options, (verbose, (browser_info,
     2.8 +      val (symbol_codes, (command_timings, (output, (options, (verbose, (browser_info,
     2.9            (document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) =
    2.10          File.read (Path.explode args_file) |> YXML.parse_body |>
    2.11            let open XML.Decode in
    2.12 -            pair (list (pair string int)) (pair (list properties) (pair bool (pair Options.decode
    2.13 +            pair (list (pair string int)) (pair (list properties) (pair string (pair Options.decode
    2.14                (pair bool (pair string (pair (list (pair string string)) (pair string
    2.15                  (pair string (pair string (pair string
    2.16                  ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))))
    2.17            end;
    2.18 +      val do_output = output <> "";
    2.19  
    2.20        val symbols = HTML.make_symbols symbol_codes;
    2.21        val _ = Options.set_default options;
    2.22 @@ -165,7 +166,8 @@
    2.23        val _ = Par_Exn.release_all [res1, res2];
    2.24  
    2.25        val _ = Options.reset_default ();
    2.26 -      val _ = if do_output then () else exit 0;
    2.27 +      val _ = Session.shutdown ();
    2.28 +      val _ = if do_output then (ML_Heap.share_common_data (); ML_Heap.save_state output) else ();
    2.29      in () end);
    2.30  
    2.31  
     3.1 --- a/src/Pure/Tools/build.scala	Mon Feb 29 15:39:17 2016 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Mon Feb 29 16:12:47 2016 +0100
     3.3 @@ -541,6 +541,7 @@
     3.4      browser_info: Path, session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
     3.5    {
     3.6      def output_path: Option[Path] = if (do_output) Some(output) else None
     3.7 +    def output_standard_path: String = if (do_output) File.standard_path(output) else ""
     3.8  
     3.9      private val parent = info.parent.getOrElse("")
    3.10  
    3.11 @@ -555,25 +556,25 @@
    3.12          {
    3.13            val theories = info.theories.map(x => (x._2, x._3))
    3.14            import XML.Encode._
    3.15 -          pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(Options.encode,
    3.16 +          pair(list(pair(string, int)), pair(list(properties), pair(string, pair(Options.encode,
    3.17              pair(bool, pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
    3.18              pair(string, pair(string, pair(string,
    3.19              list(pair(Options.encode, list(Path.encode))))))))))))))(
    3.20 -          (Symbol.codes, (command_timings, (do_output, (info.options,
    3.21 +          (Symbol.codes, (command_timings, (output_standard_path, (info.options,
    3.22              (verbose, (browser_info, (info.document_files, (File.standard_path(graph_file),
    3.23              (parent, (info.chapter, (name,
    3.24              theories))))))))))))
    3.25          }))
    3.26  
    3.27      private val env =
    3.28 -      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> File.standard_path(output),
    3.29 +      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
    3.30          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
    3.31            File.standard_path(args_file))
    3.32  
    3.33      private val script =
    3.34        if (is_pure(name)) {
    3.35          if (do_output) "./build " + name + " \"$OUTPUT\""
    3.36 -        else """ rm -f "$OUTPUT"; ./build """ + name
    3.37 +        else "./build " + name
    3.38        }
    3.39        else {
    3.40          """
    3.41 @@ -581,7 +582,7 @@
    3.42          """ +
    3.43            (if (do_output)
    3.44              """
    3.45 -            "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
    3.46 +            "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" && chmod -w "$OUTPUT"
    3.47              """
    3.48            else
    3.49              """
     4.1 --- a/src/Pure/build	Mon Feb 29 15:39:17 2016 +0100
     4.2 +++ b/src/Pure/build	Mon Feb 29 16:12:47 2016 +0100
     4.3 @@ -64,11 +64,13 @@
     4.4        -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
     4.5        -q RAW_ML_SYSTEM
     4.6    else
     4.7 +    rm -f "$OUTPUT"
     4.8      "$ISABELLE_PROCESS" \
     4.9        -e "use \"$COMPAT\" handle _ => OS.Process.exit OS.Process.failure;" \
    4.10        -e "structure Isar = struct fun main () = () end;" \
    4.11        -e "ml_prompts \"ML> \" \"ML# \";" \
    4.12 -      -q -w RAW_ML_SYSTEM "$OUTPUT"
    4.13 +      -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
    4.14 +      -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
    4.15    fi
    4.16  else
    4.17    if [ -z "$OUTPUT" ]; then
    4.18 @@ -76,12 +78,15 @@
    4.19        -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
    4.20        -q RAW_ML_SYSTEM
    4.21    else
    4.22 +    rm -f "$OUTPUT"
    4.23      "$ISABELLE_PROCESS" \
    4.24        -e "(use \"$COMPAT\"; use \"ROOT.ML\") handle _ => OS.Process.exit OS.Process.failure;" \
    4.25        -e "ml_prompts \"ML> \" \"ML# \";" \
    4.26        -e "Command_Line.tool0 Session.finish;" \
    4.27        -e "Options.reset_default ();" \
    4.28 -      -q -w RAW_ML_SYSTEM "$OUTPUT"
    4.29 +      -e "Session.shutdown ();" \
    4.30 +      -e "ML_Heap.share_common_data (); ML_Heap.save_state \"$OUTPUT\";" \
    4.31 +      -q RAW_ML_SYSTEM && chmod -w "$OUTPUT"
    4.32    fi
    4.33  fi
    4.34