# HG changeset patch # User wenzelm # Date 1670926289 -3600 # Node ID 207932c3435346629ca00df920f030e0d0fc9253 # Parent 7db5744fcf4f381a96c95019338189e266ef3344 clarified modules; diff -r 7db5744fcf4f -r 207932c34353 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Dec 13 11:01:04 2022 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Dec 13 11:11:29 2022 +0100 @@ -668,9 +668,47 @@ } object Structure { - val empty: Structure = make(Chapter_Defs.empty, Nil) + val empty: Structure = make(Options.empty) + + def make( + options: Options, + roots: List[Root_File] = Nil, + infos: List[Info] = Nil + ): Structure = { + val chapter_defs: Chapter_Defs = + roots.foldLeft(Chapter_Defs.empty) { + case (defs1, root) => + root.entries.foldLeft(defs1) { + case (defs2, entry: Chapter_Def) => defs2 + entry + case (defs2, _) => defs2 + } + } - def make(chapter_defs: Chapter_Defs, all_infos: List[Info]): Structure = { + val root_infos = { + var chapter = UNSORTED + val info_roots = new mutable.ListBuffer[Info] + for (root <- roots) { + root.entries.foreach { + case entry: Chapter_Entry => chapter = entry.name + case entry: Session_Entry => + info_roots += make_info(chapter_defs, options, root.select, root.dir, chapter, entry) + case _ => + } + chapter = UNSORTED + } + info_roots.toList + } + + val info_graph = + (root_infos ::: infos).foldLeft(Graph.string[Info]) { + case (graph, info) => + if (graph.defined(info.name)) { + error("Duplicate session " + quote(info.name) + Position.here(info.pos) + + Position.here(graph.get_node(info.name).pos)) + } + else graph.new_node(info.name, info) + } + def augment_graph( graph: Graph[String, Info], kind: String, @@ -696,15 +734,6 @@ } } - val info_graph = - all_infos.foldLeft(Graph.string[Info]) { - case (graph, info) => - if (graph.defined(info.name)) { - error("Duplicate session " + quote(info.name) + Position.here(info.pos) + - Position.here(graph.get_node(info.name).pos)) - } - else graph.new_node(info.name, info) - } val build_graph = augment_graph(info_graph, "parent", _.parent) val imports_graph = augment_graph(build_graph, "imports", _.imports) @@ -1152,38 +1181,6 @@ seen_roots.valuesIterator.toList.sortBy(_._2).map(_._1) } - def make_structure( - options: Options, - roots: List[Root_File] = Nil, - infos: List[Info] = Nil - ): Structure = { - val chapter_defs: Chapter_Defs = - roots.foldLeft(Chapter_Defs.empty) { - case (defs1, root) => - root.entries.foldLeft(defs1) { - case (defs2, entry: Chapter_Def) => defs2 + entry - case (defs2, _) => defs2 - } - } - - val root_infos = { - var chapter = UNSORTED - val info_roots = new mutable.ListBuffer[Info] - for (root <- roots) { - root.entries.foreach { - case entry: Chapter_Entry => chapter = entry.name - case entry: Session_Entry => - info_roots += make_info(chapter_defs, options, root.select, root.dir, chapter, entry) - case _ => - } - chapter = UNSORTED - } - info_roots.toList - } - - Structure.make(chapter_defs, root_infos ::: infos) - } - def load_structure( options: Options, dirs: List[Path] = Nil, @@ -1191,7 +1188,7 @@ infos: List[Info] = Nil ): Structure = { val roots = load_root_files(dirs = dirs, select_dirs = select_dirs) - make_structure(options, roots = roots, infos = infos) + Structure.make(options, roots = roots, infos = infos) }