no heap sharing for empty session (e.g. HOL-ODE);
authorwenzelm
Wed Nov 01 13:06:01 2017 +0100 (18 months ago)
changeset 66972f65fc869e835
parent 66971 43b2aac6053c
child 66973 829c3133c4ca
no heap sharing for empty session (e.g. HOL-ODE);
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Wed Nov 01 12:31:53 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Nov 01 13:06:01 2017 +0100
     1.3 @@ -227,8 +227,8 @@
     1.4              ("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)
     1.5  
     1.6          def save_heap: String =
     1.7 -          "ML_Heap.share_common_data (); ML_Heap.save_child " +
     1.8 -            ML_Syntax.print_string_bytes(File.platform_path(output))
     1.9 +          (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
    1.10 +            "ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(output))
    1.11  
    1.12          if (pide && !Sessions.is_pure(name)) {
    1.13            val resources = new Resources(deps(parent))