merged
authorwenzelm
Tue Nov 07 21:46:28 2017 +0100 (19 months ago)
changeset 6703122a47374a205
parent 67022 49309fe530fd
parent 67030 a9859e879f38
child 67032 ed499d1252fc
child 67033 2288cc39b038
merged
     1.1 --- a/src/Pure/Admin/afp.scala	Tue Nov 07 15:16:42 2017 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Tue Nov 07 21:46:28 2017 +0100
     1.3 @@ -36,8 +36,8 @@
     1.4    val sessions: List[String] = entries.flatMap(_.sessions)
     1.5  
     1.6    val sessions_structure: Sessions.T =
     1.7 -    Sessions.load(options, dirs = List(main_dir)).
     1.8 -      selection(Sessions.Selection(sessions = sessions.toList))._2
     1.9 +    Sessions.load_structure(options, dirs = List(main_dir)).
    1.10 +      selection(Sessions.Selection(sessions = sessions.toList))
    1.11  
    1.12  
    1.13    /* dependency graph */
     2.1 --- a/src/Pure/Admin/build_doc.scala	Tue Nov 07 15:16:42 2017 +0100
     2.2 +++ b/src/Pure/Admin/build_doc.scala	Tue Nov 07 21:46:28 2017 +0100
     2.3 @@ -22,13 +22,15 @@
     2.4      system_mode: Boolean = false,
     2.5      docs: List[String] = Nil): Int =
     2.6    {
     2.7 +    val sessions_structure = Sessions.load_structure(options)
     2.8      val selection =
     2.9        for {
    2.10 -        info <- Sessions.load(options).build_topological_order
    2.11 +        name <- sessions_structure.build_topological_order
    2.12 +        info = sessions_structure(name)
    2.13          if info.groups.contains("doc")
    2.14          doc = info.options.string("document_variants")
    2.15          if all_docs || docs.contains(doc)
    2.16 -      } yield (doc, info.name)
    2.17 +      } yield (doc, name)
    2.18  
    2.19      val selected_docs = selection.map(_._1)
    2.20      val sessions = selection.map(_._2)
     3.1 --- a/src/Pure/ML/ml_process.scala	Tue Nov 07 15:16:42 2017 +0100
     3.2 +++ b/src/Pure/ML/ml_process.scala	Tue Nov 07 21:46:28 2017 +0100
     3.3 @@ -32,8 +32,8 @@
     3.4        if (raw_ml_system) Nil
     3.5        else {
     3.6          val selection = Sessions.Selection(sessions = List(logic_name))
     3.7 -        val (_, selected_sessions) =
     3.8 -          sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
     3.9 +        val selected_sessions =
    3.10 +          sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
    3.11          selected_sessions.build_requirements(List(logic_name)).
    3.12            map(a => File.platform_path(store.heap(a)))
    3.13        }
     4.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 15:16:42 2017 +0100
     4.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 21:46:28 2017 +0100
     4.3 @@ -175,7 +175,7 @@
     4.4        }
     4.5    }
     4.6  
     4.7 -  def deps(sessions: T,
     4.8 +  def deps(sessions_structure: T,
     4.9        global_theories: Map[String, String],
    4.10        progress: Progress = No_Progress,
    4.11        inlined_files: Boolean = false,
    4.12 @@ -203,10 +203,11 @@
    4.13      }
    4.14  
    4.15      val session_bases =
    4.16 -      (Map.empty[String, Base] /: sessions.imports_topological_order)({
    4.17 -        case (session_bases, info) =>
    4.18 +      (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
    4.19 +        case (session_bases, session_name) =>
    4.20            if (progress.stopped) throw Exn.Interrupt()
    4.21  
    4.22 +          val info = sessions_structure(session_name)
    4.23            try {
    4.24              val parent_base: Sessions.Base =
    4.25                info.parent match {
    4.26 @@ -272,7 +273,8 @@
    4.27                }
    4.28  
    4.29                val imports_subgraph =
    4.30 -                sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
    4.31 +                sessions_structure.imports_graph.
    4.32 +                  restrict(sessions_structure.imports_graph.all_preds(info.deps).toSet)
    4.33  
    4.34                val graph0 =
    4.35                  (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
    4.36 @@ -328,7 +330,7 @@
    4.37  
    4.38    sealed case class Base_Info(
    4.39      session: String,
    4.40 -    sessions: T,
    4.41 +    sessions_structure: T,
    4.42      errors: List[String],
    4.43      base: Base,
    4.44      infos: List[Info])
    4.45 @@ -343,11 +345,11 @@
    4.46      focus_session: Boolean = false,
    4.47      required_session: Boolean = false): Base_Info =
    4.48    {
    4.49 -    val full_sessions = load(options, dirs = dirs)
    4.50 +    val full_sessions = load_structure(options, dirs = dirs)
    4.51      val global_theories = full_sessions.global_theories
    4.52  
    4.53      val selected_sessions =
    4.54 -      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))._2
    4.55 +      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))
    4.56      val info = selected_sessions(session)
    4.57      val ancestor = ancestor_session orElse info.parent
    4.58  
    4.59 @@ -398,13 +400,13 @@
    4.60  
    4.61      val full_sessions1 =
    4.62        if (infos1.isEmpty) full_sessions
    4.63 -      else load(options, dirs = dirs, infos = infos1)
    4.64 +      else load_structure(options, dirs = dirs, infos = infos1)
    4.65  
    4.66      val select_sessions1 =
    4.67        if (focus_session) full_sessions1.imports_descendants(List(session1))
    4.68        else List(session1)
    4.69      val selected_sessions1 =
    4.70 -      full_sessions1.selection(Selection(sessions = select_sessions1))._2
    4.71 +      full_sessions1.selection(Selection(sessions = select_sessions1))
    4.72  
    4.73      val sessions1 = if (all_known) full_sessions1 else selected_sessions1
    4.74      val deps1 = Sessions.deps(sessions1, global_theories)
    4.75 @@ -509,43 +511,34 @@
    4.76          session_groups = Library.merge(session_groups, other.session_groups),
    4.77          sessions = Library.merge(sessions, other.sessions))
    4.78  
    4.79 -    def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
    4.80 +    def selected(graph: Graph[String, Info]): List[String] =
    4.81      {
    4.82 -      val bad_sessions =
    4.83 -        SortedSet((base_sessions ::: exclude_sessions ::: sessions).
    4.84 -          filterNot(graph.defined(_)): _*).toList
    4.85 -      if (bad_sessions.nonEmpty)
    4.86 -        error("Undefined session(s): " + commas_quote(bad_sessions))
    4.87 +      val select_group = session_groups.toSet
    4.88 +      val select_session = sessions.toSet ++ graph.all_succs(base_sessions)
    4.89  
    4.90 -      val excluded =
    4.91 -      {
    4.92 -        val exclude_group = exclude_session_groups.toSet
    4.93 -        val exclude_group_sessions =
    4.94 +      val selected0 =
    4.95 +        if (all_sessions) graph.keys
    4.96 +        else {
    4.97            (for {
    4.98              (name, (info, _)) <- graph.iterator
    4.99 -            if graph.get_node(name).groups.exists(exclude_group)
   4.100 -          } yield name).toList
   4.101 -        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
   4.102 -      }
   4.103 -
   4.104 -      val pre_selected =
   4.105 -      {
   4.106 -        if (all_sessions) graph.keys
   4.107 -        else {
   4.108 -          val select_group = session_groups.toSet
   4.109 -          val select = sessions.toSet ++ graph.all_succs(base_sessions)
   4.110 -          (for {
   4.111 -            (name, (info, _)) <- graph.iterator
   4.112 -            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
   4.113 +            if info.dir_selected || select_session(name) ||
   4.114 +              graph.get_node(name).groups.exists(select_group)
   4.115            } yield name).toList
   4.116          }
   4.117 -      }.filterNot(excluded)
   4.118 +
   4.119 +      if (requirements) (graph.all_preds(selected0).toSet -- selected0).toList
   4.120 +      else selected0
   4.121 +    }
   4.122  
   4.123 -      val selected =
   4.124 -        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   4.125 -        else pre_selected
   4.126 -
   4.127 -      (selected, graph.restrict(graph.all_preds(selected).toSet))
   4.128 +    def excluded(graph: Graph[String, Info]): List[String] =
   4.129 +    {
   4.130 +      val exclude_group = exclude_session_groups.toSet
   4.131 +      val exclude_group_sessions =
   4.132 +        (for {
   4.133 +          (name, (info, _)) <- graph.iterator
   4.134 +          if graph.get_node(name).groups.exists(exclude_group)
   4.135 +        } yield name).toList
   4.136 +      graph.all_succs(exclude_group_sessions ::: exclude_sessions)
   4.137      }
   4.138    }
   4.139  
   4.140 @@ -594,9 +587,9 @@
   4.141      def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
   4.142      def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
   4.143  
   4.144 +    def defined(name: String): Boolean = imports_graph.defined(name)
   4.145      def apply(name: String): Info = imports_graph.get_node(name)
   4.146 -    def get(name: String): Option[Info] =
   4.147 -      if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
   4.148 +    def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
   4.149  
   4.150      def global_theories: Map[String, String] =
   4.151        (Thy_Header.bootstrap_global_theories.toMap /:
   4.152 @@ -613,26 +606,34 @@
   4.153                }
   4.154            })
   4.155  
   4.156 -    def selection(select: Selection): (List[String], T) =
   4.157 +    def selection(sel: Selection): T =
   4.158      {
   4.159 -      val (_, build_graph1) = select(build_graph)
   4.160 -      val (selected, imports_graph1) = select(imports_graph)
   4.161 -      (selected, new T(build_graph1, imports_graph1))
   4.162 +      val bad_sessions =
   4.163 +        SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
   4.164 +          filterNot(defined(_)): _*).toList
   4.165 +      if (bad_sessions.nonEmpty)
   4.166 +        error("Undefined session(s): " + commas_quote(bad_sessions))
   4.167 +
   4.168 +      val excluded = sel.excluded(build_graph).toSet
   4.169 +
   4.170 +      def restrict(graph: Graph[String, Info]): Graph[String, Info] =
   4.171 +      {
   4.172 +        val sessions = graph.all_preds(sel.selected(graph)).filterNot(excluded)
   4.173 +        graph.restrict(graph.all_preds(sessions).toSet)
   4.174 +      }
   4.175 +
   4.176 +      new T(restrict(build_graph), restrict(imports_graph))
   4.177      }
   4.178  
   4.179 -    def build_descendants(names: List[String]): List[String] =
   4.180 -      build_graph.all_succs(names)
   4.181 -    def build_requirements(names: List[String]): List[String] =
   4.182 -      build_graph.all_preds(names).reverse
   4.183 -    def build_topological_order: List[Info] =
   4.184 -      build_graph.topological_order.map(apply(_))
   4.185 +    def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
   4.186 +    def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
   4.187 +    def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
   4.188 +    def build_topological_order: List[String] = build_graph.topological_order
   4.189  
   4.190 -    def imports_descendants(names: List[String]): List[String] =
   4.191 -      imports_graph.all_succs(names)
   4.192 -    def imports_requirements(names: List[String]): List[String] =
   4.193 -      imports_graph.all_preds(names).reverse
   4.194 -    def imports_topological_order: List[Info] =
   4.195 -      imports_graph.topological_order.map(apply(_))
   4.196 +    def imports_selection(sel: Selection): List[String] = sel.selected(imports_graph)
   4.197 +    def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
   4.198 +    def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse
   4.199 +    def imports_topological_order: List[String] = imports_graph.topological_order
   4.200  
   4.201      override def toString: String =
   4.202        imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   4.203 @@ -784,7 +785,7 @@
   4.204      (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
   4.205    }
   4.206  
   4.207 -  def load(options: Options,
   4.208 +  def load_structure(options: Options,
   4.209      dirs: List[Path] = Nil,
   4.210      select_dirs: List[Path] = Nil,
   4.211      infos: List[Info] = Nil): T =
     5.1 --- a/src/Pure/Tools/build.scala	Tue Nov 07 15:16:42 2017 +0100
     5.2 +++ b/src/Pure/Tools/build.scala	Tue Nov 07 21:46:28 2017 +0100
     5.3 @@ -382,7 +382,7 @@
     5.4      /* session selection and dependencies */
     5.5  
     5.6      val full_sessions =
     5.7 -      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
     5.8 +      Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
     5.9  
    5.10      def sources_stamp(deps: Sessions.Deps, name: String): String =
    5.11      {
    5.12 @@ -391,13 +391,13 @@
    5.13        SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
    5.14      }
    5.15  
    5.16 -    val (selected, selected_sessions, deps) =
    5.17 +    val selection1 =
    5.18 +      Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    5.19 +        exclude_sessions, session_groups, sessions) ++ selection
    5.20 +
    5.21 +    val (selected_sessions, deps) =
    5.22      {
    5.23 -      val (selected0, selected_sessions0) =
    5.24 -        full_sessions.selection(
    5.25 -            Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    5.26 -              exclude_sessions, session_groups, sessions) ++ selection)
    5.27 -
    5.28 +      val selected_sessions0 = full_sessions.selection(selection1)
    5.29        val deps0 =
    5.30          Sessions.deps(selected_sessions0, full_sessions.global_theories,
    5.31            progress = progress, inlined_files = true, verbose = verbose,
    5.32 @@ -405,7 +405,7 @@
    5.33  
    5.34        if (soft_build && !fresh_build) {
    5.35          val outdated =
    5.36 -          selected0.flatMap(name =>
    5.37 +          selected_sessions0.build_topological_order.flatMap(name =>
    5.38              store.find_database(name) match {
    5.39                case Some(database) =>
    5.40                  using(SQLite.open_database(database))(store.read_build(_, name)) match {
    5.41 @@ -415,14 +415,14 @@
    5.42                  }
    5.43                case None => Some(name)
    5.44              })
    5.45 -        val (selected, selected_sessions) =
    5.46 +        val selected_sessions =
    5.47            full_sessions.selection(Sessions.Selection(sessions = outdated))
    5.48          val deps =
    5.49            Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
    5.50              .check_errors
    5.51 -        (selected, selected_sessions, deps)
    5.52 +        (selected_sessions, deps)
    5.53        }
    5.54 -      else (selected0, selected_sessions0, deps0)
    5.55 +      else (selected_sessions0, deps0)
    5.56      }
    5.57  
    5.58  
    5.59 @@ -450,7 +450,7 @@
    5.60  
    5.61      // optional cleanup
    5.62      if (clean_build) {
    5.63 -      for (name <- full_sessions.build_descendants(selected)) {
    5.64 +      for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
    5.65          val files =
    5.66            List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    5.67              map(store.output_dir + _).filter(_.is_file)
     6.1 --- a/src/Pure/Tools/imports.scala	Tue Nov 07 15:16:42 2017 +0100
     6.2 +++ b/src/Pure/Tools/imports.scala	Tue Nov 07 21:46:28 2017 +0100
     6.3 @@ -99,8 +99,8 @@
     6.4      select_dirs: List[Path] = Nil,
     6.5      verbose: Boolean = false) =
     6.6    {
     6.7 -    val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
     6.8 -    val (selected, selected_sessions) = full_sessions.selection(selection)
     6.9 +    val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
    6.10 +    val selected_sessions = full_sessions.selection(selection)
    6.11  
    6.12      val deps =
    6.13        Sessions.deps(selected_sessions, full_sessions.global_theories,
    6.14 @@ -109,41 +109,42 @@
    6.15      val root_keywords = Sessions.root_syntax.keywords
    6.16  
    6.17      if (operation_imports) {
    6.18 -      val report_imports: List[Report] = selected.map((session_name: String) =>
    6.19 -      {
    6.20 -        val info = selected_sessions(session_name)
    6.21 -        val session_base = deps(session_name)
    6.22 +      val report_imports: List[Report] =
    6.23 +        selected_sessions.build_topological_order.map((session_name: String) =>
    6.24 +          {
    6.25 +            val info = selected_sessions(session_name)
    6.26 +            val session_base = deps(session_name)
    6.27  
    6.28 -        val declared_imports =
    6.29 -          selected_sessions.imports_requirements(List(session_name)).toSet
    6.30 +            val declared_imports =
    6.31 +              selected_sessions.imports_requirements(List(session_name)).toSet
    6.32  
    6.33 -        val extra_imports =
    6.34 -          (for {
    6.35 -            (_, a) <- session_base.known.theories.iterator
    6.36 -            if session_base.theory_qualifier(a) == info.name
    6.37 -            b <- deps.all_known.get_file(a.path.file)
    6.38 -            qualifier = session_base.theory_qualifier(b)
    6.39 -            if !declared_imports.contains(qualifier)
    6.40 -          } yield qualifier).toSet
    6.41 +            val extra_imports =
    6.42 +              (for {
    6.43 +                (_, a) <- session_base.known.theories.iterator
    6.44 +                if session_base.theory_qualifier(a) == info.name
    6.45 +                b <- deps.all_known.get_file(a.path.file)
    6.46 +                qualifier = session_base.theory_qualifier(b)
    6.47 +                if !declared_imports.contains(qualifier)
    6.48 +              } yield qualifier).toSet
    6.49  
    6.50 -        val loaded_imports =
    6.51 -          selected_sessions.imports_requirements(
    6.52 -            session_base.loaded_theories.keys.map(a =>
    6.53 -              session_base.theory_qualifier(session_base.known.theories(a))))
    6.54 -          .toSet - session_name
    6.55 +            val loaded_imports =
    6.56 +              selected_sessions.imports_requirements(
    6.57 +                session_base.loaded_theories.keys.map(a =>
    6.58 +                  session_base.theory_qualifier(session_base.known.theories(a))))
    6.59 +              .toSet - session_name
    6.60  
    6.61 -        val minimal_imports =
    6.62 -          loaded_imports.filter(s1 =>
    6.63 -            !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    6.64 +            val minimal_imports =
    6.65 +              loaded_imports.filter(s1 =>
    6.66 +                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    6.67  
    6.68 -        def make_result(set: Set[String]): Option[List[String]] =
    6.69 -          if (set.isEmpty) None
    6.70 -          else Some(selected_sessions.imports_topological_order.map(_.name).filter(set))
    6.71 +            def make_result(set: Set[String]): Option[List[String]] =
    6.72 +              if (set.isEmpty) None
    6.73 +              else Some(selected_sessions.imports_topological_order.filter(set))
    6.74  
    6.75 -        Report(info, declared_imports, make_result(extra_imports),
    6.76 -          if (loaded_imports == declared_imports - session_name) None
    6.77 -          else make_result(minimal_imports))
    6.78 -      })
    6.79 +            Report(info, declared_imports, make_result(extra_imports),
    6.80 +              if (loaded_imports == declared_imports - session_name) None
    6.81 +              else make_result(minimal_imports))
    6.82 +          })
    6.83  
    6.84        progress.echo("\nPotential session imports:")
    6.85        for {
    6.86 @@ -172,34 +173,34 @@
    6.87      if (operation_update) {
    6.88        progress.echo("\nUpdate theory imports" + update_message + ":")
    6.89        val updates =
    6.90 -        selected.flatMap(session_name =>
    6.91 -        {
    6.92 -          val info = selected_sessions(session_name)
    6.93 -          val session_base = deps(session_name)
    6.94 -          val session_resources = new Resources(session_base)
    6.95 -          val imports_base = session_base.get_imports
    6.96 -          val imports_resources = new Resources(imports_base)
    6.97 +        selected_sessions.build_topological_order.flatMap(session_name =>
    6.98 +          {
    6.99 +            val info = selected_sessions(session_name)
   6.100 +            val session_base = deps(session_name)
   6.101 +            val session_resources = new Resources(session_base)
   6.102 +            val imports_base = session_base.get_imports
   6.103 +            val imports_resources = new Resources(imports_base)
   6.104  
   6.105 -          def standard_import(qualifier: String, dir: String, s: String): String =
   6.106 -            imports_resources.standard_import(session_base, qualifier, dir, s)
   6.107 +            def standard_import(qualifier: String, dir: String, s: String): String =
   6.108 +              imports_resources.standard_import(session_base, qualifier, dir, s)
   6.109  
   6.110 -          val updates_root =
   6.111 -            for {
   6.112 -              (_, pos) <- info.theories.flatMap(_._2)
   6.113 -              upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
   6.114 -            } yield upd
   6.115 +            val updates_root =
   6.116 +              for {
   6.117 +                (_, pos) <- info.theories.flatMap(_._2)
   6.118 +                upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
   6.119 +              } yield upd
   6.120  
   6.121 -          val updates_theories =
   6.122 -            for {
   6.123 -              (_, name) <- session_base.known.theories_local.toList
   6.124 -              if session_base.theory_qualifier(name) == info.name
   6.125 -              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   6.126 -              upd <- update_name(session_base.overall_syntax.keywords, pos,
   6.127 -                standard_import(session_base.theory_qualifier(name), name.master_dir, _))
   6.128 -            } yield upd
   6.129 +            val updates_theories =
   6.130 +              for {
   6.131 +                (_, name) <- session_base.known.theories_local.toList
   6.132 +                if session_base.theory_qualifier(name) == info.name
   6.133 +                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   6.134 +                upd <- update_name(session_base.overall_syntax.keywords, pos,
   6.135 +                  standard_import(session_base.theory_qualifier(name), name.master_dir, _))
   6.136 +              } yield upd
   6.137  
   6.138 -          updates_root ::: updates_theories
   6.139 -        })
   6.140 +            updates_root ::: updates_theories
   6.141 +          })
   6.142  
   6.143        val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   6.144        val conflicts =
   6.145 @@ -311,15 +312,14 @@
   6.146            verbose = verbose)
   6.147        }
   6.148        else if (operation_update && incremental_update) {
   6.149 -        val (selected, selected_sessions) =
   6.150 -          Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
   6.151 -        selected_sessions.imports_topological_order.foreach(info =>
   6.152 -        {
   6.153 -          imports(options, operation_update = operation_update, progress = progress,
   6.154 -            update_message = " for session " + quote(info.name),
   6.155 -            selection = Sessions.Selection(sessions = List(info.name)),
   6.156 -            dirs = dirs ::: select_dirs, verbose = verbose)
   6.157 -        })
   6.158 +        Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
   6.159 +          selection(selection).imports_topological_order.foreach(name =>
   6.160 +            {
   6.161 +              imports(options, operation_update = operation_update, progress = progress,
   6.162 +                update_message = " for session " + quote(name),
   6.163 +                selection = Sessions.Selection(sessions = List(name)),
   6.164 +                dirs = dirs ::: select_dirs, verbose = verbose)
   6.165 +            })
   6.166        }
   6.167      })
   6.168  }
     7.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 15:16:42 2017 +0100
     7.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 21:46:28 2017 +0100
     7.3 @@ -45,7 +45,10 @@
     7.4    def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
     7.5  
     7.6    def logic_info(options: Options): Option[Sessions.Info] =
     7.7 -    try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
     7.8 +    try {
     7.9 +      Sessions.load_structure(session_options(options), dirs = session_dirs()).
    7.10 +        get(logic_name(options))
    7.11 +    }
    7.12      catch { case ERROR(_) => None }
    7.13  
    7.14    def logic_root(options: Options): Position.T =
    7.15 @@ -68,10 +71,11 @@
    7.16  
    7.17      val session_list =
    7.18      {
    7.19 -      val sessions = Sessions.load(options.value, dirs = session_dirs())
    7.20 +      val sessions_structure = Sessions.load_structure(options.value, dirs = session_dirs())
    7.21        val (main_sessions, other_sessions) =
    7.22 -        sessions.imports_topological_order.partition(info => info.groups.contains("main"))
    7.23 -      main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
    7.24 +        sessions_structure.imports_topological_order.
    7.25 +          partition(name => sessions_structure(name).groups.contains("main"))
    7.26 +      main_sessions.sorted ::: other_sessions.sorted
    7.27      }
    7.28  
    7.29      val entries =
    7.30 @@ -129,7 +133,7 @@
    7.31    def session_start(options: Options)
    7.32    {
    7.33      Isabelle_Process.start(PIDE.session, session_options(options),
    7.34 -      sessions = Some(PIDE.resources.session_base_info.sessions),
    7.35 +      sessions = Some(PIDE.resources.session_base_info.sessions_structure),
    7.36        logic = PIDE.resources.session_name,
    7.37        store = Sessions.store(session_build_mode() == "system"),
    7.38        modes =