# HG changeset patch
# User wenzelm
# Date 1491231044 -7200
# Node ID 3ff88fece1f680c07764130ea1088266594449e7
# Parent  9ca34f0407a9ece35c396b5f459133202a2e0fc5
tuned;

diff -r 9ca34f0407a9 -r 3ff88fece1f6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 03 16:36:45 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 03 16:50:44 2017 +0200
@@ -17,25 +17,14 @@
 
 object Sessions
 {
-  /* Pure */
-
-  def pure_name(name: String): Boolean = name == Thy_Header.PURE
+  /* base info and source dependencies */
 
-  def pure_files(resources: Resources, syntax: Outer_Syntax, dir: Path): List[Path] =
-  {
-    val roots = Thy_Header.ml_roots.map(_._1)
-    val loaded_files =
-      roots.flatMap(root => resources.loaded_files(syntax, File.read(dir + Path.explode(root))))
-    (roots ::: loaded_files).map(file => dir + Path.explode(file))
-  }
-
-  def pure_base(options: Options): Base = session_base(options, Thy_Header.PURE)
-
-
-  /* base info and source dependencies */
+  def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
   object Base
   {
+    def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
+
     lazy val bootstrap: Base =
       Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
   }
@@ -120,7 +109,13 @@
             val loaded_files =
               if (inlined_files) {
                 val pure_files =
-                  if (pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
+                  if (is_pure(name)) {
+                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
+                    val files =
+                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
+                        map(file => info.dir + Path.explode(file))
+                    roots ::: files
+                  }
                   else Nil
                 pure_files ::: thy_deps.loaded_files
               }
@@ -368,8 +363,8 @@
           val name = entry.name
 
           if (name == "") error("Bad session name")
-          if (pure_name(name) && entry.parent.isDefined) error("Illegal parent session")
-          if (!pure_name(name) && !entry.parent.isDefined) error("Missing parent session")
+          if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
+          if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
           val session_options = options ++ entry.options
 
diff -r 9ca34f0407a9 -r 3ff88fece1f6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Apr 03 16:36:45 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Apr 03 16:50:44 2017 +0200
@@ -219,7 +219,7 @@
           "ML_Heap.share_common_data (); ML_Heap.save_child " +
             ML_Syntax.print_string0(File.platform_path(output))
 
-        if (pide && !Sessions.pure_name(name)) {
+        if (pide && !Sessions.is_pure(name)) {
           val resources = new Resources(name, deps(parent))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
@@ -255,7 +255,7 @@
             (if (do_output) "; " + save_heap else "") + "));"
 
           val process =
-            if (Sessions.pure_name(name)) {
+            if (Sessions.is_pure(name)) {
               ML_Process(options, raw_ml_system = true, cwd = info.dir.file,
                 args =
                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
@@ -519,7 +519,7 @@
                 val ancestor_results = selected_tree.ancestors(name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
 
-                val do_output = build_heap || Sessions.pure_name(name) || queue.is_inner(name)
+                val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
 
                 val (current, heap_stamp) =
                 {
diff -r 9ca34f0407a9 -r 3ff88fece1f6 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 16:36:45 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Apr 03 16:50:44 2017 +0200
@@ -74,7 +74,7 @@
     val session_name = JEdit_Sessions.session_name(options)
     val session_base =
       try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) }
-      catch { case ERROR(_) => Sessions.pure_base(options) }
+      catch { case ERROR(_) => Sessions.Base.pure(options) }
 
     _resources =
       new JEdit_Resources(session_base.copy(known_theories =