# HG changeset patch # User wenzelm # Date 1660742297 -7200 # Node ID 8342cba8eae86ee9915a9eab96934154fdfb42f0 # Parent 3d8b37b1d798b160447c83806601e02e5da097cf clarified signature: avoid constants from Sessions.Structure within Session.Base; diff -r 3d8b37b1d798 -r 8342cba8eae8 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Wed Aug 17 14:42:20 2022 +0200 +++ b/src/Pure/ML/ml_process.scala Wed Aug 17 15:18:17 2022 +0200 @@ -80,7 +80,7 @@ // session base val (init_session_base, eval_init_session) = session_base match { - case None => (sessions_structure.bootstrap, Nil) + case None => (Sessions.bootstrap_base, Nil) case Some(base) => (base, List("Resources.init_session_env ()")) } val init_session = Isabelle_System.tmp_file("init_session") diff -r 3d8b37b1d798 -r 8342cba8eae8 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Aug 17 14:42:20 2022 +0200 +++ b/src/Pure/PIDE/resources.scala Wed Aug 17 15:18:17 2022 +0200 @@ -57,7 +57,7 @@ (command_timings, (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)), (Scala.functions, - (session_base.global_theories.toList, + (sessions_structure.global_theories.toList, session_base.loaded_theories.keys))))))))) } @@ -150,9 +150,11 @@ } yield file } + def global_theory(theory: String): Boolean = + sessions_structure.global_theories.isDefinedAt(theory) + def theory_name(qualifier: String, theory: String): String = - if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory)) - theory + if (Long_Name.is_qualified(theory) || global_theory(theory)) theory else Long_Name.qualify(qualifier, theory) def find_theory_node(theory: String): Option[Document.Node.Name] = { @@ -189,7 +191,7 @@ def find_theory(file: JFile): Option[Document.Node.Name] = { for { - qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile) + qualifier <- sessions_structure.session_directories.get(File.canonical(file).getParentFile) theory_base <- proper_string(Thy_Header.theory_name(file.getName)) theory = theory_name(qualifier, theory_base) theory_node <- find_theory_node(theory) @@ -208,7 +210,7 @@ theory <- Thy_Header.try_read_dir(dir).iterator if Completion.completed(s)(theory) } yield { - if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory + if (session == context_session || global_theory(theory)) theory else Long_Name.qualify(session, theory) }).toList.sorted } diff -r 3d8b37b1d798 -r 8342cba8eae8 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Aug 17 14:42:20 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Aug 17 15:18:17 2022 +0200 @@ -61,8 +61,6 @@ sealed case class Base( session_name: String = "", session_pos: Position.T = Position.none, - session_directories: Map[JFile, String] = Map.empty, - global_theories: Map[String, String] = Map.empty, proper_session_theories: List[Document.Node.Name] = Nil, document_theories: List[Document.Node.Name] = Nil, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, // cumulative imports @@ -76,6 +74,8 @@ session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, errors: List[String] = Nil ) { + def session_entry: (String, Base) = session_name -> this + override def toString: String = "Sessions.Base(session_name = " + quote(session_name) + ", loaded_theories = " + loaded_theories.size + @@ -96,6 +96,8 @@ nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax } + val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax) + sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { override def toString: String = "Sessions.Deps(" + sessions_structure + ")" @@ -152,13 +154,9 @@ } } - val bootstrap_bases = { - val base = sessions_structure.bootstrap - Map(base.session_name -> base) - } - val session_bases = - sessions_structure.imports_topological_order.foldLeft(bootstrap_bases) { + sessions_structure.imports_topological_order.foldLeft( + Map(Sessions.bootstrap_base.session_entry)) { case (session_bases, session_name) => progress.expose_interrupt() @@ -333,8 +331,6 @@ Base( session_name = info.name, session_pos = info.pos, - session_directories = sessions_structure.session_directories, - global_theories = sessions_structure.global_theories, proper_session_theories = proper_session_theories, document_theories = document_theories, loaded_theories = dependencies.loaded_theories, @@ -350,7 +346,7 @@ document_errors ::: dir_errors ::: sources_errors ::: path_errors ::: bibtex_errors) - session_bases + (info.name -> base) + session_bases + base.session_entry } catch { case ERROR(msg) => @@ -736,11 +732,7 @@ ) { sessions_structure => - def bootstrap: Base = - Base( - session_directories = session_directories, - global_theories = global_theories, - overall_syntax = Thy_Header.bootstrap_syntax) + def bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax) def dest_session_directories: List[(String, String)] = for ((file, session) <- session_directories.toList)