# HG changeset patch
# User wenzelm
# Date 1491509070 -7200
# Node ID 8cd54b18b68b0f59efa94b0f32d34c6aec83aaf0
# Parent  d7ebd2b25b825df0bea884a3edbc8785819019ee
clarified signature: tree structure is not essential;

diff -r d7ebd2b25b82 -r 8cd54b18b68b Admin/jenkins/build/ci_build_benchmark.scala
--- a/Admin/jenkins/build/ci_build_benchmark.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -12,7 +12,7 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
-  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
-    tree.selection(session_groups = List("timing"))
+  def select_sessions(sessions: Sessions.T) =
+    sessions.selection(session_groups = List("timing"))
 
 }
diff -r d7ebd2b25b82 -r 8cd54b18b68b Admin/jenkins/build/ci_build_makeall.scala
--- a/Admin/jenkins/build/ci_build_makeall.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -11,7 +11,7 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
-  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
-    tree.selection(all_sessions = true)
+  def select_sessions(sessions: Sessions.T) =
+    sessions.selection(all_sessions = true)
 
 }
diff -r d7ebd2b25b82 -r 8cd54b18b68b Admin/jenkins/build/ci_build_makeall_seq.scala
--- a/Admin/jenkins/build/ci_build_makeall_seq.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall_seq.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -11,7 +11,7 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
-  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) =
-    tree.selection(all_sessions = true)
+  def select_sessions(sessions: Sessions.T) =
+    sessions.selection(all_sessions = true)
 
 }
diff -r d7ebd2b25b82 -r 8cd54b18b68b src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -146,5 +146,5 @@
   def pre_hook(args: List[String]): Unit
   def post_hook(results: Build.Results): Unit
 
-  def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
+  def select_sessions(sessions: Sessions.T): (List[String], Sessions.T)
 }
diff -r d7ebd2b25b82 -r 8cd54b18b68b src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/System/isabelle_process.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -20,7 +20,7 @@
     modes: List[String] = Nil,
     cwd: JFile = null,
     env: Map[String, String] = Isabelle_System.settings(),
-    tree: Option[Sessions.Tree] = None,
+    sessions: Option[Sessions.T] = None,
     store: Sessions.Store = Sessions.store(),
     phase_changed: Session.Phase => Unit = null)
   {
@@ -30,7 +30,7 @@
     session.start(receiver =>
       Isabelle_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
         cwd = cwd, env = env, receiver = receiver, xml_cache = session.xml_cache,
-        tree = tree, store = store))
+        sessions = sessions, store = store))
   }
 
   def apply(
@@ -43,14 +43,14 @@
     env: Map[String, String] = Isabelle_System.settings(),
     receiver: Prover.Receiver = Console.println(_),
     xml_cache: XML.Cache = new XML.Cache(),
-    tree: Option[Sessions.Tree] = None,
+    sessions: Option[Sessions.T] = None,
     store: Sessions.Store = Sessions.store()): Prover =
   {
     val channel = System_Channel()
     val process =
       try {
         ML_Process(options, logic = logic, args = args, dirs = dirs, modes = modes,
-          cwd = cwd, env = env, tree = tree, store = store, channel = Some(channel))
+          cwd = cwd, env = env, sessions = sessions, store = store, channel = Some(channel))
       }
       catch { case exn @ ERROR(_) => channel.accepted(); throw exn }
     process.stdin.close
diff -r d7ebd2b25b82 -r 8cd54b18b68b src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -49,7 +49,7 @@
     def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
   }
 
-  def deps(tree: Tree,
+  def deps(sessions: T,
       progress: Progress = No_Progress,
       inlined_files: Boolean = false,
       verbose: Boolean = false,
@@ -57,7 +57,8 @@
       check_keywords: Set[String] = Set.empty,
       global_theories: Set[String] = Set.empty): Deps =
   {
-    Deps((Map.empty[String, Base] /: tree.topological_order)({ case (sessions, (name, info)) =>
+    Deps((Map.empty[String, Base] /: sessions.topological_order)({
+      case (sessions, (name, info)) =>
         if (progress.stopped) throw Exn.Interrupt()
 
         try {
@@ -153,14 +154,14 @@
 
   def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
   {
-    val full_tree = load(options, dirs = dirs)
-    val (_, tree) = full_tree.selection(sessions = List(session))
+    val full_sessions = load(options, dirs = dirs)
+    val (_, selected_sessions) = full_sessions.selection(sessions = List(session))
 
-    deps(tree, global_theories = full_tree.global_theories)(session)
+    deps(selected_sessions, global_theories = full_sessions.global_theories)(session)
   }
 
 
-  /* session tree */
+  /* cumulative session info */
 
   sealed case class Info(
     chapter: String,
@@ -180,44 +181,41 @@
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   }
 
-  object Tree
+  def make(infos: Traversable[(String, Info)]): T =
   {
-    def apply(infos: Traversable[(String, Info)]): Tree =
-    {
-      val graph1 =
-        (Graph.string[Info] /: infos) {
-          case (graph, (name, info)) =>
-            if (graph.defined(name))
-              error("Duplicate session " + quote(name) + Position.here(info.pos) +
-                Position.here(graph.get_node(name).pos))
-            else graph.new_node(name, info)
-        }
-      val graph2 =
-        (graph1 /: graph1.iterator) {
-          case (graph, (name, (info, _))) =>
-            info.parent match {
-              case None => graph
-              case Some(parent) =>
-                if (!graph.defined(parent))
-                  error("Bad parent session " + quote(parent) + " for " +
-                    quote(name) + Position.here(info.pos))
+    val graph1 =
+      (Graph.string[Info] /: infos) {
+        case (graph, (name, info)) =>
+          if (graph.defined(name))
+            error("Duplicate session " + quote(name) + Position.here(info.pos) +
+              Position.here(graph.get_node(name).pos))
+          else graph.new_node(name, info)
+      }
+    val graph2 =
+      (graph1 /: graph1.iterator) {
+        case (graph, (name, (info, _))) =>
+          info.parent match {
+            case None => graph
+            case Some(parent) =>
+              if (!graph.defined(parent))
+                error("Bad parent session " + quote(parent) + " for " +
+                  quote(name) + Position.here(info.pos))
 
-                try { graph.add_edge_acyclic(parent, name) }
-                catch {
-                  case exn: Graph.Cycles[_] =>
-                    error(cat_lines(exn.cycles.map(cycle =>
-                      "Cyclic session dependency of " +
-                        cycle.map(c => quote(c.toString)).mkString(" via "))) +
-                          Position.here(info.pos))
-                }
-            }
-        }
+              try { graph.add_edge_acyclic(parent, name) }
+              catch {
+                case exn: Graph.Cycles[_] =>
+                  error(cat_lines(exn.cycles.map(cycle =>
+                    "Cyclic session dependency of " +
+                      cycle.map(c => quote(c.toString)).mkString(" via "))) +
+                        Position.here(info.pos))
+              }
+          }
+      }
 
-      new Tree(graph2)
-    }
+    new T(graph2)
   }
 
-  final class Tree private(val graph: Graph[String, Info])
+  final class T private[Sessions](val graph: Graph[String, Info])
     extends PartialFunction[String, Info]
   {
     def apply(name: String): Info = graph.get_node(name)
@@ -235,7 +233,7 @@
       exclude_session_groups: List[String] = Nil,
       exclude_sessions: List[String] = Nil,
       session_groups: List[String] = Nil,
-      sessions: List[String] = Nil): (List[String], Tree) =
+      sessions: List[String] = Nil): (List[String], T) =
     {
       val bad_sessions =
         SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
@@ -270,7 +268,7 @@
         else pre_selected
 
       val graph1 = graph.restrict(graph.all_preds(selected).toSet)
-      (selected, new Tree(graph1))
+      (selected, new T(graph1))
     }
 
     def ancestors(name: String): List[String] =
@@ -279,7 +277,7 @@
     def topological_order: List[(String, Info)] =
       graph.topological_order.map(name => (name, apply(name)))
 
-    override def toString: String = graph.keys_iterator.mkString("Sessions.Tree(", ", ", ")")
+    override def toString: String = graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   }
 
 
@@ -450,7 +448,7 @@
     if (is_session_dir(dir)) dir
     else error("Bad session root directory: " + dir.toString)
 
-  def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
+  def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
   {
     def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
       load_root(select, dir) ::: load_roots(select, dir)
@@ -481,7 +479,7 @@
     dirs.foreach(check_session_dir(_))
     select_dirs.foreach(check_session_dir(_))
 
-    Tree(
+    make(
       for {
         (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
         info <- load_dir(select, dir)
diff -r d7ebd2b25b82 -r 8cd54b18b68b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -63,12 +63,12 @@
       }
     }
 
-    def apply(tree: Sessions.Tree, store: Sessions.Store): Queue =
+    def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
     {
-      val graph = tree.graph
-      val sessions = graph.keys
+      val graph = sessions.graph
+      val names = graph.keys
 
-      val timings = sessions.map(name => (name, load_timings(store, name)))
+      val timings = names.map(name => (name, load_timings(store, name)))
       val command_timings =
         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
       val session_timing =
@@ -91,7 +91,7 @@
             case 0 =>
               compare_timing(name2, name1) match {
                 case 0 =>
-                  tree(name2).timeout compare tree(name1).timeout match {
+                  sessions(name2).timeout compare sessions(name1).timeout match {
                     case 0 => name1 compare name2
                     case ord => ord
                   }
@@ -101,7 +101,7 @@
           }
       }
 
-      new Queue(graph, SortedSet(sessions: _*)(Ordering), command_timings)
+      new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
     }
   }
 
@@ -170,7 +170,7 @@
   private class Job(progress: Progress,
     name: String,
     val info: Sessions.Info,
-    tree: Sessions.Tree,
+    sessions: Sessions.T,
     deps: Sessions.Deps,
     store: Sessions.Store,
     do_output: Boolean,
@@ -228,7 +228,7 @@
           val session_result = Future.promise[Process_Result]
 
           Isabelle_Process.start(session, options, logic = parent,
-            cwd = info.dir.file, env = env, tree = Some(tree), store = store,
+            cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
             phase_changed =
             {
               case Session.Ready => session.protocol_command("build_session", args_yxml)
@@ -260,11 +260,13 @@
                 args =
                   (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
                   List("--eval", eval),
-                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
+                env = env, sessions = Some(sessions), store = store,
+                cleanup = () => args_file.delete)
             }
             else {
               ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
-                env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
+                env = env, sessions = Some(sessions), store = store,
+                cleanup = () => args_file.delete)
             }
 
           process.result(
@@ -366,53 +368,53 @@
       system_mode = system_mode,
       verbose = verbose,
       pide = pide,
-      selection = { full_tree =>
-        full_tree.selection(requirements, all_sessions,
+      selection = { full_sessions =>
+        full_sessions.selection(requirements, all_sessions,
           exclude_session_groups, exclude_sessions, session_groups, sessions) })
   }
 
   def build_selection(
-    options: Options,
-    progress: Progress = No_Progress,
-    build_heap: Boolean = false,
-    clean_build: Boolean = false,
-    dirs: List[Path] = Nil,
-    select_dirs: List[Path] = Nil,
-    numa_shuffling: Boolean = false,
-    max_jobs: Int = 1,
-    list_files: Boolean = false,
-    check_keywords: Set[String] = Set.empty,
-    no_build: Boolean = false,
-    system_mode: Boolean = false,
-    verbose: Boolean = false,
-    pide: Boolean = false,
-    selection: Sessions.Tree => (List[String], Sessions.Tree) =
-      (_.selection(all_sessions = true))): Results =
+      options: Options,
+      progress: Progress = No_Progress,
+      build_heap: Boolean = false,
+      clean_build: Boolean = false,
+      dirs: List[Path] = Nil,
+      select_dirs: List[Path] = Nil,
+      numa_shuffling: Boolean = false,
+      max_jobs: Int = 1,
+      list_files: Boolean = false,
+      check_keywords: Set[String] = Set.empty,
+      no_build: Boolean = false,
+      system_mode: Boolean = false,
+      verbose: Boolean = false,
+      pide: Boolean = false,
+      selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
+    ): Results =
   {
     /* session selection and dependencies */
 
     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
-    val full_tree = Sessions.load(build_options, dirs, select_dirs)
-    val (selected, selected_tree) = selection(full_tree)
+    val full_sessions = Sessions.load(build_options, dirs, select_dirs)
+    val (selected, selected_sessions) = selection(full_sessions)
     val deps =
-      Sessions.deps(selected_tree, progress = progress, inlined_files = true,
+      Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
         verbose = verbose, list_files = list_files, check_keywords = check_keywords,
-        global_theories = full_tree.global_theories)
+        global_theories = full_sessions.global_theories)
 
     def sources_stamp(name: String): List[String] =
-      (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
+      (selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
 
 
     /* main build process */
 
     val store = Sessions.store(system_mode)
-    val queue = Queue(selected_tree, store)
+    val queue = Queue(selected_sessions, store)
 
     store.prepare_output()
 
     // optional cleanup
     if (clean_build) {
-      for (name <- full_tree.graph.all_succs(selected)) {
+      for (name <- full_sessions.graph.all_succs(selected)) {
         val files =
           List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
             map(store.output_dir + _).filter(_.is_file)
@@ -518,7 +520,7 @@
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt(_)) match {
               case Some((name, info)) =>
-                val ancestor_results = selected_tree.ancestors(name).map(results(_))
+                val ancestor_results = selected_sessions.ancestors(name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
 
                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
@@ -555,8 +557,8 @@
                   val numa_node = numa_nodes.next(used_node(_))
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
                   val job =
-                    new Job(progress, name, info, selected_tree, deps, store, do_output, verbose,
-                      pide, numa_node, queue.command_timings(name))
+                    new Job(progress, name, info, selected_sessions, deps, store, do_output,
+                      verbose, pide, numa_node, queue.command_timings(name))
                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
                 }
                 else {
@@ -604,7 +606,7 @@
         (for {
           (name, result) <- results0.iterator
           if result.ok
-          info = full_tree(name)
+          info = full_sessions(name)
           if info.options.bool("browser_info")
         } yield (info.chapter, (name, info.description))).toList.groupBy(_._1).
             map({ case (chapter, es) => (chapter, es.map(_._2)) }).filterNot(_._2.isEmpty)
diff -r d7ebd2b25b82 -r 8cd54b18b68b src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Thu Apr 06 21:10:35 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Thu Apr 06 22:04:30 2017 +0200
@@ -23,16 +23,16 @@
     redirect: Boolean = false,
     cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None,
-    tree: Option[Sessions.Tree] = None,
+    sessions: Option[Sessions.T] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
     val logic_name = Isabelle_System.default_logic(logic)
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
-        val (_, session_tree) =
-          tree.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
-        (session_tree.ancestors(logic_name) ::: List(logic_name)).
+        val (_, selected_sessions) =
+          sessions.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
+        (selected_sessions.ancestors(logic_name) ::: List(logic_name)).
           map(a => File.platform_path(store.heap(a)))
       }