# HG changeset patch # User wenzelm # Date 1670926707 -3600 # Node ID 2447d947d90000bebd21140e6c26a894fb25de29 # Parent 207932c3435346629ca00df920f030e0d0fc9253 clarified modules; diff -r 207932c34353 -r 2447d947d900 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Dec 13 11:11:29 2022 +0100 +++ b/src/Pure/Thy/sessions.scala Tue Dec 13 11:18:27 2022 +0100 @@ -158,7 +158,7 @@ (other_name, List( - make_info( + Info.make( Chapter_Defs.empty, info.options, dir_selected = false, @@ -476,6 +476,81 @@ sessions: List[String] ) + object Info { + def make( + chapter_defs: Chapter_Defs, + options: Options, + dir_selected: Boolean, + dir: Path, + chapter: String, + entry: Session_Entry + ): Info = { + try { + val name = entry.name + + if (illegal_session(name)) error("Illegal session name " + quote(name)) + if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") + if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") + + val session_path = dir + Path.explode(entry.path) + val directories = entry.directories.map(dir => session_path + Path.explode(dir)) + + val session_options = options ++ entry.options + + val theories = + entry.theories.map({ case (opts, thys) => + (session_options ++ opts, + thys.map({ case ((thy, pos), _) => + val thy_name = Thy_Header.import_name(thy) + if (illegal_theory(thy_name)) { + error("Illegal theory name " + quote(thy_name) + Position.here(pos)) + } + else (thy, pos) })) }) + + val global_theories = + for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } + yield { + val thy_name = Path.explode(thy).file_name + if (Long_Name.is_qualified(thy_name)) { + error("Bad qualified name for global theory " + + quote(thy_name) + Position.here(pos)) + } + else thy_name + } + + val conditions = + theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted. + map(x => (x, Isabelle_System.getenv(x) != "")) + + val document_files = + entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) + + val export_files = + entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) + + val meta_digest = + SHA1.digest( + (name, chapter, entry.parent, entry.directories, entry.options, entry.imports, + entry.theories_no_position, conditions, entry.document_theories_no_position, + entry.document_files) + .toString) + + val chapter_groups = chapter_defs(chapter).groups + val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains) + + Info(name, chapter, dir_selected, entry.pos, groups, session_path, + entry.parent, entry.description, directories, session_options, + entry.imports, theories, global_theories, entry.document_theories, document_files, + export_files, entry.export_classpath, meta_digest) + } + catch { + case ERROR(msg) => + error(msg + "\nThe error(s) above occurred in session entry " + + quote(entry.name) + Position.here(entry.pos)) + } + } + } + sealed case class Info( name: String, chapter: String, @@ -568,79 +643,6 @@ def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains) } - def make_info( - chapter_defs: Chapter_Defs, - options: Options, - dir_selected: Boolean, - dir: Path, - chapter: String, - entry: Session_Entry - ): Info = { - try { - val name = entry.name - - if (illegal_session(name)) error("Illegal session name " + quote(name)) - if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") - if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") - - val session_path = dir + Path.explode(entry.path) - val directories = entry.directories.map(dir => session_path + Path.explode(dir)) - - val session_options = options ++ entry.options - - val theories = - entry.theories.map({ case (opts, thys) => - (session_options ++ opts, - thys.map({ case ((thy, pos), _) => - val thy_name = Thy_Header.import_name(thy) - if (illegal_theory(thy_name)) { - error("Illegal theory name " + quote(thy_name) + Position.here(pos)) - } - else (thy, pos) })) }) - - val global_theories = - for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } - yield { - val thy_name = Path.explode(thy).file_name - if (Long_Name.is_qualified(thy_name)) { - error("Bad qualified name for global theory " + - quote(thy_name) + Position.here(pos)) - } - else thy_name - } - - val conditions = - theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted. - map(x => (x, Isabelle_System.getenv(x) != "")) - - val document_files = - entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) - - val export_files = - entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) - - val meta_digest = - SHA1.digest( - (name, chapter, entry.parent, entry.directories, entry.options, entry.imports, - entry.theories_no_position, conditions, entry.document_theories_no_position, - entry.document_files) - .toString) - - val chapter_groups = chapter_defs(chapter).groups - val groups = chapter_groups ::: entry.groups.filterNot(chapter_groups.contains) - - Info(name, chapter, dir_selected, entry.pos, groups, session_path, - entry.parent, entry.description, directories, session_options, - entry.imports, theories, global_theories, entry.document_theories, document_files, - export_files, entry.export_classpath, meta_digest) - } - catch { - case ERROR(msg) => - error(msg + "\nThe error(s) above occurred in session entry " + - quote(entry.name) + Position.here(entry.pos)) - } - } - object Selection { val empty: Selection = Selection() val all: Selection = Selection(all_sessions = true) @@ -691,7 +693,7 @@ 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) + info_roots += Info.make(chapter_defs, options, root.select, root.dir, chapter, entry) case _ => } chapter = UNSORTED