src/Pure/Tools/build.scala
changeset 65360 3ff88fece1f6
parent 65359 9ca34f0407a9
child 65365 d32e702d7ab8
     1.1 --- a/src/Pure/Tools/build.scala	Mon Apr 03 16:36:45 2017 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Apr 03 16:50:44 2017 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4            "ML_Heap.share_common_data (); ML_Heap.save_child " +
     1.5              ML_Syntax.print_string0(File.platform_path(output))
     1.6  
     1.7 -        if (pide && !Sessions.pure_name(name)) {
     1.8 +        if (pide && !Sessions.is_pure(name)) {
     1.9            val resources = new Resources(name, deps(parent))
    1.10            val session = new Session(options, resources)
    1.11            val handler = new Handler(progress, session, name)
    1.12 @@ -255,7 +255,7 @@
    1.13              (if (do_output) "; " + save_heap else "") + "));"
    1.14  
    1.15            val process =
    1.16 -            if (Sessions.pure_name(name)) {
    1.17 +            if (Sessions.is_pure(name)) {
    1.18                ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
    1.19                  args =
    1.20                    (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
    1.21 @@ -519,7 +519,7 @@
    1.22                  val ancestor_results = selected_tree.ancestors(name).map(results(_))
    1.23                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    1.24  
    1.25 -                val do_output = build_heap || Sessions.pure_name(name) || queue.is_inner(name)
    1.26 +                val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
    1.27  
    1.28                  val (current, heap_stamp) =
    1.29                  {