--- 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 \
--- /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
+ }
+}
--- 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,
--- 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,