tuned signature;
authorwenzelm
Tue Nov 07 15:45:33 2017 +0100 (7 months ago)
changeset 67023e27e05d6f2a7
parent 67018 f6aa133f9b16
child 67024 72d37a2e9cca
tuned signature;
src/Pure/Admin/build_doc.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
src/Tools/jEdit/src/jedit_sessions.scala
     1.1 --- a/src/Pure/Admin/build_doc.scala	Tue Nov 07 11:11:37 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_doc.scala	Tue Nov 07 15:45:33 2017 +0100
     1.3 @@ -22,13 +22,15 @@
     1.4      system_mode: Boolean = false,
     1.5      docs: List[String] = Nil): Int =
     1.6    {
     1.7 +    val sessions_structure = Sessions.load(options)
     1.8      val selection =
     1.9        for {
    1.10 -        info <- Sessions.load(options).build_topological_order
    1.11 +        name <- sessions_structure.build_topological_order
    1.12 +        info = sessions_structure(name)
    1.13          if info.groups.contains("doc")
    1.14          doc = info.options.string("document_variants")
    1.15          if all_docs || docs.contains(doc)
    1.16 -      } yield (doc, info.name)
    1.17 +      } yield (doc, name)
    1.18  
    1.19      val selected_docs = selection.map(_._1)
    1.20      val sessions = selection.map(_._2)
     2.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 11:11:37 2017 +0100
     2.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 15:45:33 2017 +0100
     2.3 @@ -204,9 +204,10 @@
     2.4  
     2.5      val session_bases =
     2.6        (Map.empty[String, Base] /: sessions.imports_topological_order)({
     2.7 -        case (session_bases, info) =>
     2.8 +        case (session_bases, session_name) =>
     2.9            if (progress.stopped) throw Exn.Interrupt()
    2.10  
    2.11 +          val info = sessions(session_name)
    2.12            try {
    2.13              val parent_base: Sessions.Base =
    2.14                info.parent match {
    2.15 @@ -624,15 +625,15 @@
    2.16        build_graph.all_succs(names)
    2.17      def build_requirements(names: List[String]): List[String] =
    2.18        build_graph.all_preds(names).reverse
    2.19 -    def build_topological_order: List[Info] =
    2.20 -      build_graph.topological_order.map(apply(_))
    2.21 +    def build_topological_order: List[String] =
    2.22 +      build_graph.topological_order
    2.23  
    2.24      def imports_descendants(names: List[String]): List[String] =
    2.25        imports_graph.all_succs(names)
    2.26      def imports_requirements(names: List[String]): List[String] =
    2.27        imports_graph.all_preds(names).reverse
    2.28 -    def imports_topological_order: List[Info] =
    2.29 -      imports_graph.topological_order.map(apply(_))
    2.30 +    def imports_topological_order: List[String] =
    2.31 +      imports_graph.topological_order
    2.32  
    2.33      override def toString: String =
    2.34        imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
     3.1 --- a/src/Pure/Tools/imports.scala	Tue Nov 07 11:11:37 2017 +0100
     3.2 +++ b/src/Pure/Tools/imports.scala	Tue Nov 07 15:45:33 2017 +0100
     3.3 @@ -138,7 +138,7 @@
     3.4  
     3.5          def make_result(set: Set[String]): Option[List[String]] =
     3.6            if (set.isEmpty) None
     3.7 -          else Some(selected_sessions.imports_topological_order.map(_.name).filter(set))
     3.8 +          else Some(selected_sessions.imports_topological_order.filter(set))
     3.9  
    3.10          Report(info, declared_imports, make_result(extra_imports),
    3.11            if (loaded_imports == declared_imports - session_name) None
    3.12 @@ -313,11 +313,11 @@
    3.13        else if (operation_update && incremental_update) {
    3.14          val (selected, selected_sessions) =
    3.15            Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
    3.16 -        selected_sessions.imports_topological_order.foreach(info =>
    3.17 +        selected_sessions.imports_topological_order.foreach(name =>
    3.18          {
    3.19            imports(options, operation_update = operation_update, progress = progress,
    3.20 -            update_message = " for session " + quote(info.name),
    3.21 -            selection = Sessions.Selection(sessions = List(info.name)),
    3.22 +            update_message = " for session " + quote(name),
    3.23 +            selection = Sessions.Selection(sessions = List(name)),
    3.24              dirs = dirs ::: select_dirs, verbose = verbose)
    3.25          })
    3.26        }
     4.1 --- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 11:11:37 2017 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 15:45:33 2017 +0100
     4.3 @@ -68,10 +68,11 @@
     4.4  
     4.5      val session_list =
     4.6      {
     4.7 -      val sessions = Sessions.load(options.value, dirs = session_dirs())
     4.8 +      val sessions_structure = Sessions.load(options.value, dirs = session_dirs())
     4.9        val (main_sessions, other_sessions) =
    4.10 -        sessions.imports_topological_order.partition(info => info.groups.contains("main"))
    4.11 -      main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
    4.12 +        sessions_structure.imports_topological_order.
    4.13 +          partition(name => sessions_structure(name).groups.contains("main"))
    4.14 +      main_sessions.sorted ::: other_sessions.sorted
    4.15      }
    4.16  
    4.17      val entries =