# HG changeset patch # User wenzelm # Date 1670494595 -3600 # Node ID faea52979f547eda92f50cc8e19b018436a70cc5 # Parent ec505888434740d4d48d5830f89867c144c32ef0 tuned; diff -r ec5058884347 -r faea52979f54 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Dec 08 10:44:03 2022 +0100 +++ b/src/Pure/Thy/sessions.scala Thu Dec 08 11:16:35 2022 +0100 @@ -54,7 +54,7 @@ } - /* base info and source dependencies */ + /* base info */ sealed case class Base( session_name: String = "", @@ -96,8 +96,109 @@ val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax) + sealed case class Base_Info( + base: Base, + sessions_structure: Structure = Structure.empty, + errors: List[String] = Nil, + infos: List[Info] = Nil + ) { + def session_name: String = base.session_name + + def check_errors: Base_Info = + if (errors.isEmpty) this + else error(cat_lines(errors)) + } + + def base_info0(session: String): Base_Info = + Base_Info(Base(session_name = session)) + + def base_info(options: Options, + session: String, + progress: Progress = new Progress, + dirs: List[Path] = Nil, + include_sessions: List[String] = Nil, + session_ancestor: Option[String] = None, + session_requirements: Boolean = false + ): Base_Info = { + val full_sessions = load_structure(options, dirs = dirs) + + val selected_sessions = + full_sessions.selection(Selection(sessions = session :: session_ancestor.toList)) + val info = selected_sessions(session) + val ancestor = session_ancestor orElse info.parent + + val (session1, infos1) = + if (session_requirements && ancestor.isDefined) { + val deps = Sessions.deps(selected_sessions, progress = progress) + val base = deps(session) + + val ancestor_loaded = + deps.get(ancestor.get) match { + case Some(ancestor_base) + if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) => + ancestor_base.loaded_theories.defined _ + case _ => + error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session)) + } + + val required_theories = + for { + thy <- base.loaded_theories.keys + if !ancestor_loaded(thy) && selected_sessions.theory_qualifier(thy) != session + } + yield thy + + if (required_theories.isEmpty) (ancestor.get, Nil) + else { + val other_name = info.name + "_requirements(" + ancestor.get + ")" + Isabelle_System.isabelle_tmp_prefix() + + (other_name, + List( + make_info( + Chapter_Defs.empty, + info.options, + dir_selected = false, + dir = Path.explode("$ISABELLE_TMP_PREFIX"), + chapter = info.chapter, + Session_Entry( + pos = info.pos, + name = other_name, + groups = info.groups, + path = ".", + parent = ancestor, + description = "Required theory imports from other sessions", + options = Nil, + imports = info.deps, + directories = Nil, + theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))), + document_theories = Nil, + document_files = Nil, + export_files = Nil, + export_classpath = Nil)))) + } + } + else (session, Nil) + + val full_sessions1 = + if (infos1.isEmpty) full_sessions + else load_structure(options, dirs = dirs, infos = infos1) + + val selected_sessions1 = + full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions)) + + val deps1 = Sessions.deps(selected_sessions1, progress = progress) + + Base_Info(deps1(session1), sessions_structure = full_sessions1, + errors = deps1.errors, infos = infos1) + } + + + /* source dependencies */ + sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { - override def toString: String = "Sessions.Deps(" + sessions_structure + ")" + def base_info(session: String): Base_Info = + Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors) def is_empty: Boolean = session_bases.keysIterator.forall(_.isEmpty) def apply(name: String): Base = session_bases(name) @@ -123,8 +224,7 @@ case errs => error(cat_lines(errs)) } - def base_info(session: String): Base_Info = - Base_Info(base = apply(session), sessions_structure = sessions_structure, errors = errors) + override def toString: String = "Sessions.Deps(" + sessions_structure + ")" } def deps(sessions_structure: Structure, @@ -359,106 +459,6 @@ } - /* base info */ - - sealed case class Base_Info( - base: Base, - sessions_structure: Structure = Structure.empty, - errors: List[String] = Nil, - infos: List[Info] = Nil - ) { - def session_name: String = base.session_name - - def check_errors: Base_Info = - if (errors.isEmpty) this - else error(cat_lines(errors)) - } - - def base_info0(session: String): Base_Info = - Base_Info(Base(session_name = session)) - - def base_info(options: Options, - session: String, - progress: Progress = new Progress, - dirs: List[Path] = Nil, - include_sessions: List[String] = Nil, - session_ancestor: Option[String] = None, - session_requirements: Boolean = false - ): Base_Info = { - val full_sessions = load_structure(options, dirs = dirs) - - val selected_sessions = - full_sessions.selection(Selection(sessions = session :: session_ancestor.toList)) - val info = selected_sessions(session) - val ancestor = session_ancestor orElse info.parent - - val (session1, infos1) = - if (session_requirements && ancestor.isDefined) { - val deps = Sessions.deps(selected_sessions, progress = progress) - val base = deps(session) - - val ancestor_loaded = - deps.get(ancestor.get) match { - case Some(ancestor_base) - if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) => - ancestor_base.loaded_theories.defined _ - case _ => - error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session)) - } - - val required_theories = - for { - thy <- base.loaded_theories.keys - if !ancestor_loaded(thy) && selected_sessions.theory_qualifier(thy) != session - } - yield thy - - if (required_theories.isEmpty) (ancestor.get, Nil) - else { - val other_name = info.name + "_requirements(" + ancestor.get + ")" - Isabelle_System.isabelle_tmp_prefix() - - (other_name, - List( - make_info( - Chapter_Defs.empty, - info.options, - dir_selected = false, - dir = Path.explode("$ISABELLE_TMP_PREFIX"), - chapter = info.chapter, - Session_Entry( - pos = info.pos, - name = other_name, - groups = info.groups, - path = ".", - parent = ancestor, - description = "Required theory imports from other sessions", - options = Nil, - imports = info.deps, - directories = Nil, - theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))), - document_theories = Nil, - document_files = Nil, - export_files = Nil, - export_classpath = Nil)))) - } - } - else (session, Nil) - - val full_sessions1 = - if (infos1.isEmpty) full_sessions - else load_structure(options, dirs = dirs, infos = infos1) - - val selected_sessions1 = - full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions)) - - val deps1 = Sessions.deps(selected_sessions1, progress = progress) - - Base_Info(deps1(session1), sessions_structure = full_sessions1, - errors = deps1.errors, infos = infos1) - } - - /* cumulative session info */ sealed case class Chapter_Info(