# HG changeset patch # User wenzelm # Date 1660932461 -7200 # Node ID 091edca12219596b7588d872d277a524ef3f50d7 # Parent 2167b9e3157a826b82a277ddba8fe926a00b7d8d clarified modules; diff -r 2167b9e3157a -r 091edca12219 etc/build.props --- a/etc/build.props Fri Aug 19 16:46:00 2022 +0200 +++ b/etc/build.props Fri Aug 19 20:07:41 2022 +0200 @@ -116,6 +116,7 @@ src/Pure/PIDE/command_span.scala \ src/Pure/PIDE/document.scala \ src/Pure/PIDE/document_id.scala \ + src/Pure/PIDE/document_info.scala \ src/Pure/PIDE/document_status.scala \ src/Pure/PIDE/editor.scala \ src/Pure/PIDE/headless.scala \ diff -r 2167b9e3157a -r 091edca12219 src/Pure/PIDE/document_info.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/document_info.scala Fri Aug 19 20:07:41 2022 +0200 @@ -0,0 +1,172 @@ +/* Title: Pure/PIDE/document_info.scala + Author: Makarius + +Persistent document information --- for presentation purposes. +*/ + +package isabelle + + +object Document_Info { + sealed case class Session( + name: String, + used_theories: List[String], + loaded_theories: Map[String, Theory]) + + object Theory { + def apply( + name: String, + files: List[String], + static_session: String, + dynamic_session: String, + entities: List[Export_Theory.Entity0], + others: List[String] + ): Theory = { + val entities1 = + entities.filter(e => e.file.nonEmpty && Position.Range.unapply(e.pos).isDefined) + new Theory(name, files, static_session, dynamic_session, entities1, others) + } + } + + class Theory private( + val name: String, + val files: List[String], + val static_session: String, + val dynamic_session: String, + entities: List[Export_Theory.Entity0], + others: List[String] + ) { + override def toString: String = name + + val (thy_file, blobs_files) = + files match { + case Nil => error("Unknown theory file for " + quote(name)) + case a :: bs => + def for_theory: String = " for theory " + quote(name) + if (!File.is_thy(a)) error("Bad .thy file " + quote(a) + for_theory) + for (b <- bs if File.is_thy(b)) error("Bad auxiliary file " + quote(b) + for_theory) + (a, bs) + } + + def home_session: Boolean = static_session == dynamic_session + + def print_short: String = + if (home_session) Long_Name.base_name(name) else name + + def print_long: String = + "theory " + quote(name) + + (if (home_session) "" else " (session " + quote(dynamic_session) + ")") + + private lazy val by_file_range: Map[(String, Symbol.Range), List[Export_Theory.Entity0]] = + entities.groupBy(entity => (entity.file, entity.range)) + + private lazy val by_file_kname: Map[(String, String), Export_Theory.Entity0] = + (for { + entity <- entities + file <- Position.File.unapply(entity.pos) + } yield (file, entity.kname) -> entity).toMap + + def get_defs(file: String, range: Symbol.Range): List[Export_Theory.Entity0] = + by_file_range.getOrElse((file, range), Nil) + + def get_def(file: String, kind: String, name: String): Option[Export_Theory.Entity0] = + by_file_kname.get((file, Export_Theory.export_kind_name(kind, name))) + + def elements(elements: Presentation.Elements): Presentation.Elements = + elements.copy(entity = others.foldLeft(elements.entity)(_ + _)) + } + + val empty: Document_Info = new Document_Info(Map.empty) + + def read( + database_context: Export.Database_Context, + deps: Sessions.Deps, + sessions: List[String] + ): Document_Info = { + val sessions_domain = sessions.toSet + val sessions_structure = deps.sessions_structure + val sessions_requirements = sessions_structure.build_requirements(sessions) + + def read_theory(theory_context: Export.Theory_Context): Document_Info.Theory = + { + val session_name = theory_context.session_context.session_name + val theory_name = theory_context.theory + + val files = theory_context.files0(permissive = true) + + val (entities, others) = + if (sessions_domain(session_name)) { + val theory = Export_Theory.read_theory(theory_context, permissive = true) + (theory.entity_iterator.toList, + theory.others.keySet.toList) + } + else (Nil, Nil) + + Theory(theory_name, + static_session = sessions_structure.theory_qualifier(theory_name), + dynamic_session = session_name, + files = files, + entities = entities, + others = others) + } + + def read_session(session_name: String): Document_Info.Session = { + val used_theories = deps(session_name).used_theories.map(_._1.theory) + val loaded_theories0 = + using(database_context.open_session(deps.base_info(session_name))) { session_context => + for (theory_name <- used_theories) + yield theory_name -> read_theory(session_context.theory(theory_name)) + } + Session(session_name, used_theories, loaded_theories0.toMap) + } + + val result0 = + (for (session <- Par_List.map(read_session, sessions_requirements).iterator) + yield session.name -> session).toMap + + val result1 = + sessions_requirements.foldLeft(Map.empty[String, Session]) { + case (seen, session_name) => + val session0 = result0(session_name) + val loaded_theories1 = + sessions_structure(session_name).parent.map(seen) match { + case None => session0.loaded_theories + case Some(parent_session) => + parent_session.loaded_theories ++ session0.loaded_theories + } + val session1 = session0.copy(loaded_theories = loaded_theories1) + seen + (session_name -> session1) + } + + new Document_Info(result1) + } +} + +class Document_Info private(sessions: Map[String, Document_Info.Session]) { + override def toString: String = + sessions.keysIterator.toList.sorted.mkString("Document_Info(", ", ", ")") + + def the_session(session: String): Document_Info.Session = + sessions.getOrElse(session, + error("Unknown document information for session: " + quote(session))) + + def theory_by_name(session: String, theory: String): Option[Document_Info.Theory] = + by_session_and_theory_name.get((session, theory)) + + def theory_by_file(session: String, file: String): Option[Document_Info.Theory] = + by_session_and_theory_file.get((session, file)) + + private lazy val by_session_and_theory_name: Map[(String, String), Document_Info.Theory] = + (for { + session <- sessions.valuesIterator + theory <- session.loaded_theories.valuesIterator + } yield (session.name, theory.name) -> theory).toMap + + private lazy val by_session_and_theory_file: Map[(String, String), Document_Info.Theory] = { + (for { + session <- sessions.valuesIterator + theory <- session.loaded_theories.valuesIterator + file <- theory.files.iterator + } yield (session.name, file) -> theory).toMap + } +} diff -r 2167b9e3157a -r 091edca12219 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Fri Aug 19 16:46:00 2022 +0200 +++ b/src/Pure/Thy/presentation.scala Fri Aug 19 20:07:41 2022 +0200 @@ -21,33 +21,33 @@ sessions_structure: Sessions.Structure, elements: Elements, root_dir: Path = Path.current, - nodes: Nodes = Nodes.empty - ): HTML_Context = new HTML_Context(sessions_structure, elements, root_dir, nodes) + document_info: Document_Info = Document_Info.empty + ): HTML_Context = new HTML_Context(sessions_structure, elements, root_dir, document_info) class HTML_Context private[Presentation]( sessions_structure: Sessions.Structure, val elements: Elements, val root_dir: Path, - val nodes: Nodes + val document_info: Document_Info ) { /* directory structure and resources */ - def theory_by_name(session: String, theory: String): Option[Nodes.Theory] = - nodes.theory_by_name(session, theory) + def theory_by_name(session: String, theory: String): Option[Document_Info.Theory] = + document_info.theory_by_name(session, theory) - def theory_by_file(session: String, file: String): Option[Nodes.Theory] = - nodes.theory_by_file(session, file) + def theory_by_file(session: String, file: String): Option[Document_Info.Theory] = + document_info.theory_by_file(session, file) def session_dir(session: String): Path = root_dir + Path.explode(sessions_structure(session).chapter_session) - def theory_html(theory: Nodes.Theory): Path = + def theory_html(theory: Document_Info.Theory): Path = Path.explode(theory.print_short).html def file_html(file: String): Path = Path.explode("files") + Path.explode(file).squash.html - def smart_html(theory: Nodes.Theory, file: String): Path = + def smart_html(theory: Document_Info.Theory, file: String): Path = if (File.is_thy(file)) theory_html(theory) else file_html(file) def files_path(session: String, path: Path): Path = @@ -113,172 +113,6 @@ language = Markup.Elements(Markup.Language.DOCUMENT)) - /* per-session node info */ - - object Nodes { - sealed case class Session( - name: String, - used_theories: List[String], - loaded_theories: Map[String, Theory]) - - object Theory { - def apply( - name: String, - files: List[String], - static_session: String, - dynamic_session: String, - entities: List[Export_Theory.Entity0], - others: List[String] - ): Theory = { - val entities1 = - entities.filter(e => e.file.nonEmpty && Position.Range.unapply(e.pos).isDefined) - new Theory(name, files, static_session, dynamic_session, entities1, others) - } - } - - class Theory private( - val name: String, - val files: List[String], - val static_session: String, - val dynamic_session: String, - entities: List[Export_Theory.Entity0], - others: List[String] - ) { - override def toString: String = name - - val (thy_file, blobs_files) = - files match { - case Nil => error("Unknown theory file for " + quote(name)) - case a :: bs => - def for_theory: String = " for theory " + quote(name) - if (!File.is_thy(a)) error("Bad .thy file " + quote(a) + for_theory) - for (b <- bs if File.is_thy(b)) error("Bad auxiliary file " + quote(b) + for_theory) - (a, bs) - } - - def home_session: Boolean = static_session == dynamic_session - - def print_short: String = - if (home_session) Long_Name.base_name(name) else name - - def print_long: String = - "theory " + quote(name) + - (if (home_session) "" else " (session " + quote(dynamic_session) + ")") - - private lazy val by_file_range: Map[(String, Symbol.Range), List[Export_Theory.Entity0]] = - entities.groupBy(entity => (entity.file, entity.range)) - - private lazy val by_file_kname: Map[(String, String), Export_Theory.Entity0] = - (for { - entity <- entities - file <- Position.File.unapply(entity.pos) - } yield (file, entity.kname) -> entity).toMap - - def get_defs(file: String, range: Symbol.Range): List[Export_Theory.Entity0] = - by_file_range.getOrElse((file, range), Nil) - - def get_def(file: String, kind: String, name: String): Option[Export_Theory.Entity0] = - by_file_kname.get((file, Export_Theory.export_kind_name(kind, name))) - - def elements(elements: Elements): Elements = - elements.copy(entity = others.foldLeft(elements.entity)(_ + _)) - } - - val empty: Nodes = new Nodes(Map.empty) - - def read( - database_context: Export.Database_Context, - deps: Sessions.Deps, - sessions: List[String] - ): Nodes = { - val sessions_domain = sessions.toSet - val sessions_structure = deps.sessions_structure - val sessions_requirements = sessions_structure.build_requirements(sessions) - - def read_theory(theory_context: Export.Theory_Context): Nodes.Theory = - { - val session_name = theory_context.session_context.session_name - val theory_name = theory_context.theory - - val files = theory_context.files0(permissive = true) - - val (entities, others) = - if (sessions_domain(session_name)) { - val theory = Export_Theory.read_theory(theory_context, permissive = true) - (theory.entity_iterator.toList, - theory.others.keySet.toList) - } - else (Nil, Nil) - - Theory(theory_name, - static_session = sessions_structure.theory_qualifier(theory_name), - dynamic_session = session_name, - files = files, - entities = entities, - others = others) - } - - def read_session(session_name: String): Nodes.Session = { - val used_theories = deps(session_name).used_theories.map(_._1.theory) - val loaded_theories0 = - using(database_context.open_session(deps.base_info(session_name))) { session_context => - for (theory_name <- used_theories) - yield theory_name -> read_theory(session_context.theory(theory_name)) - } - Session(session_name, used_theories, loaded_theories0.toMap) - } - - val result0 = - (for (session <- Par_List.map(read_session, sessions_requirements).iterator) - yield session.name -> session).toMap - - val result1 = - sessions_requirements.foldLeft(Map.empty[String, Session]) { - case (seen, session_name) => - val session0 = result0(session_name) - val loaded_theories1 = - sessions_structure(session_name).parent.map(seen) match { - case None => session0.loaded_theories - case Some(parent_session) => - parent_session.loaded_theories ++ session0.loaded_theories - } - val session1 = session0.copy(loaded_theories = loaded_theories1) - seen + (session_name -> session1) - } - - new Nodes(result1) - } - } - - class Nodes private(sessions: Map[String, Nodes.Session]) { - override def toString: String = - sessions.keysIterator.toList.sorted.mkString("Nodes(", ", ", ")") - - def the_session(session: String): Nodes.Session = - sessions.getOrElse(session, error("Unknown session node information: " + quote(session))) - - def theory_by_name(session: String, theory: String): Option[Nodes.Theory] = - by_session_and_theory_name.get((session, theory)) - - def theory_by_file(session: String, file: String): Option[Nodes.Theory] = - by_session_and_theory_file.get((session, file)) - - private lazy val by_session_and_theory_name: Map[(String, String), Nodes.Theory] = - (for { - session <- sessions.valuesIterator - theory <- session.loaded_theories.valuesIterator - } yield (session.name, theory.name) -> theory).toMap - - private lazy val by_session_and_theory_file: Map[(String, String), Nodes.Theory] = { - (for { - session <- sessions.valuesIterator - theory <- session.loaded_theories.valuesIterator - file <- theory.files.iterator - } yield (session.name, file) -> theory).toMap - } - } - - /* formal entities */ object Theory_Ref { @@ -344,10 +178,10 @@ HTML.link(html_link, body) } case Entity_Ref(def_file, kind, name) => - def logical_ref(theory: Nodes.Theory): Option[String] = + def logical_ref(theory: Document_Info.Theory): Option[String] = theory.get_def(def_file, kind, name).map(_.kname) - def physical_ref(theory: Nodes.Theory): Option[String] = + def physical_ref(theory: Document_Info.Theory): Option[String] = props match { case Position.Def_Range(range) if theory.name == theory_name => seen_ranges += range @@ -618,7 +452,7 @@ progress.echo("Presenting " + session_name + " in " + session_dir + " ...") - val session = html_context.nodes.the_session(session_name) + val session = html_context.document_info.the_session(session_name) Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(session_info.options, diff -r 2167b9e3157a -r 091edca12219 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Aug 19 16:46:00 2022 +0200 +++ b/src/Pure/Tools/build.scala Fri Aug 19 20:07:41 2022 +0200 @@ -495,15 +495,15 @@ } using(Export.open_database_context(store)) { database_context => - val presentation_nodes = - Presentation.Nodes.read(database_context, deps, presentation_sessions.map(_.name)) + val document_info = + Document_Info.read(database_context, deps, presentation_sessions.map(_.name)) Par_List.map({ (session: String) => progress.expose_interrupt() val html_context = Presentation.html_context(deps.sessions_structure, Presentation.elements1, - root_dir = presentation_dir, nodes = presentation_nodes) + root_dir = presentation_dir, document_info = document_info) using(database_context.open_session(deps.base_info(session))) { session_context => Presentation.session_html(html_context, session_context,