# HG changeset patch # User wenzelm # Date 1660918799 -7200 # Node ID 2ee3ea69e8f113cd6ea4484d44b89ee35be9d773 # Parent 6d9d9a395533ef1132ca27c518760d30d67f8d52 clarified Presentation.Nodes, with explicit Nodes.Session and Nodes.Theory; distinguish Nodes.Theory.static_session vs. dynamic_session: refer to exports from dynamic_session, corresponding to strictly to build_graph; more robust treatment of source files and links to generated files; retrieve entities by their file position, within its corresponding session/theory hierarchy; diff -r 6d9d9a395533 -r 2ee3ea69e8f1 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Fri Aug 19 15:24:39 2022 +0200 +++ b/src/Pure/Thy/export_theory.scala Fri Aug 19 16:19:59 2022 +0200 @@ -190,6 +190,7 @@ ) { val kname: String = export_kind_name(kind, name) val range: Symbol.Range = Position.Range.unapply(pos).getOrElse(Text.Range.offside) + val file: String = Position.File.unapply(pos).getOrElse("") def export_kind: String = Export_Theory.export_kind(kind) override def toString: String = export_kind + " " + quote(name) diff -r 6d9d9a395533 -r 2ee3ea69e8f1 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Fri Aug 19 15:24:39 2022 +0200 +++ b/src/Pure/Thy/presentation.scala Fri Aug 19 16:19:59 2022 +0200 @@ -32,41 +32,33 @@ ) { /* directory structure and resources */ - def theory_session(name: Document.Node.Name): String = - sessions_structure.theory_qualifier(name) + def theory_by_name(session: String, theory: String): Option[Nodes.Theory] = + nodes.theory_by_name(session, theory) - def theory_elements(name: Document.Node.Name): Elements = - elements.copy(entity = nodes(name.theory).others.foldLeft(elements.entity)(_ + _)) + def theory_by_file(session: String, file: String): Option[Nodes.Theory] = + nodes.theory_by_file(session, file) def session_dir(session: String): Path = root_dir + Path.explode(sessions_structure(session).chapter_session) - def html_name_theory(name: Document.Node.Name): String = - Path.explode(name.theory_base_name).html.implode + def theory_html(theory: Nodes.Theory): Path = + Path.explode(theory.print_short).html - def html_name_file(src_path: Path): String = - (Path.explode("files") + src_path.squash.html).implode + def file_html(file: String): Path = + Path.explode("files") + Path.explode(file).squash.html - def html_name(name: Document.Node.Name): String = - if (name.node.endsWith(".thy")) html_name_theory(name) - else html_name_file(name.path) + def smart_html(theory: Nodes.Theory, file: String): Path = + if (file.endsWith(".thy")) theory_html(theory) else file_html(file) def files_path(session: String, path: Path): Path = session_dir(session) + Path.explode("files") + path.squash.html - private def session_relative(session0: String, session1: String): Option[String] = { - for { - info0 <- sessions_structure.get(session0) - info1 <- sessions_structure.get(session1) - } yield { - if (info0.name == info1.name) "" - else if (info0.chapter == info1.chapter) "../" + info1.name + "/" - else "../../" + info1.chapter_session + "/" + def relative_link(dir: Path, file: Path): String = + try { File.path(dir.java_path.relativize(file.java_path).toFile).implode } + catch { + case _: IllegalArgumentException => + error("Cannot relativize " + file + " wrt. " + dir) } - } - - def node_relative(session0: String, node_name: Document.Node.Name): Option[String] = - session_relative(session0, sessions_structure.theory_qualifier(node_name)) /* HTML content */ @@ -123,106 +115,185 @@ /* per-session node info */ - sealed case class File_Info(theory: String, is_theory: Boolean = false) + object Nodes { + sealed case class Session( + name: String, + used_theories: List[String], + loaded_theories: Map[String, Theory]) - object Node_Info { - val empty: Node_Info = new Node_Info(Map.empty, Map.empty, Nil) - def make(theory: Export_Theory.Theory): Node_Info = { - val by_range = theory.entity_iterator.toList.groupBy(_.range) - val by_kname = theory.entity_iterator.map(entity => entity.kname -> entity).toMap - val others = theory.others.keySet.toList - new Node_Info(by_range, by_kname, others) + 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 - class Node_Info private( - by_range: Map[Symbol.Range, List[Export_Theory.Entity0]], - by_kname: Map[String, Export_Theory.Entity0], - val others: List[String] - ) { - def get_defs(range: Symbol.Range): List[Export_Theory.Entity0] = - by_range.getOrElse(range, Nil) - def get_def(kind: String, name: String): Option[Export_Theory.Entity0] = { - by_kname.get(Export_Theory.export_kind_name(kind, 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 (!a.endsWith(".thy")) error("Bad .thy file " + quote(a) + for_theory) + for (b <- bs if b.endsWith(".thy")) 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)(_ + _)) } - } - object Nodes { - val empty: Nodes = new Nodes(Map.empty, Map.empty) + val empty: Nodes = new Nodes(Map.empty) def read( database_context: Export.Database_Context, deps: Sessions.Deps, - presentation_sessions: List[String] + sessions: List[String] ): Nodes = { + val sessions_domain = sessions.toSet + val sessions_structure = deps.sessions_structure + val sessions_requirements = sessions_structure.build_requirements(sessions) - def open_session(session: String): Export.Session_Context = - database_context.open_session(deps.base_info(session)) + 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) - type Batch = (String, List[String]) - val batches = - presentation_sessions.foldLeft((Set.empty[String], List.empty[Batch]))( - { case ((seen, batches), session) => - val thys = deps(session).loaded_theories.keys_iterator.filterNot(seen).toList - (seen ++ thys, (session, thys) :: batches) - })._2 + 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) + } - val theory_node_info = - Par_List.map[Batch, List[(String, Node_Info)]]( - { case (session, thys) => - using(open_session(session)) { session_context => - for (thy_name <- thys) yield { - val theory_context = session_context.theory(thy_name) - val theory = Export_Theory.read_theory(theory_context, permissive = true) - thy_name -> Node_Info.make(theory) - } - } - }, batches).flatten.toMap + 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 files_info = - deps.sessions_structure.build_requirements(presentation_sessions).flatMap(session => - using(open_session(session)) { session_context => - session_context.theory_names().flatMap { theory => - session_context.theory(theory).files0(permissive = true) match { - case Nil => Nil - case thy :: blobs => - val thy_file_info = File_Info(theory, is_theory = true) - (thy -> thy_file_info) :: blobs.map(_ -> File_Info(theory)) + 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 } - } - }).toMap + val session1 = session0.copy(loaded_theories = loaded_theories1) + seen + (session_name -> session1) + } - new Nodes(theory_node_info, files_info) + new Nodes(result1) } } - class Nodes private( - theory_node_info: Map[String, Node_Info], - val files_info: Map[String, File_Info] - ) { - def apply(name: String): Node_Info = theory_node_info.getOrElse(name, Node_Info.empty) - def get(name: String): Option[Node_Info] = theory_node_info.get(name) + 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 { - def unapply(props: Properties.T): Option[Document.Node.Name] = - (props, props, props) match { - case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) => - Some(Resources.file_node(Path.explode(thy_file), theory = theory)) + def unapply(props: Properties.T): Option[String] = + (props, props) match { + case (Markup.Kind(Markup.THEORY), Markup.Name(theory)) => Some(theory) case _ => None } } object Entity_Ref { - def unapply(props: Properties.T): Option[(Path, Option[String], String, String)] = + def unapply(props: Properties.T): Option[(String, String, String)] = (props, props, props, props) match { - case (Markup.Entity.Ref.Prop(_), Position.Def_File(def_file), - Markup.Kind(kind), Markup.Name(name)) => - val def_theory = Position.Def_Theory.unapply(props) - Some((Path.explode(def_file), def_theory, kind, name)) + case (Markup.Entity.Ref.Prop(_), Position.Def_File(file), Markup.Kind(kind), Markup.Name(name)) => + Some((file, kind, name)) case _ => None } } @@ -231,65 +302,67 @@ val empty: Entity_Context = new Entity_Context def make( - session: String, - node: Document.Node.Name, - html_context: HTML_Context): Entity_Context = + html_context: HTML_Context, + session_name: String, + theory_name: String, + file_name: String + ): Entity_Context = new Entity_Context { + private val session_dir = html_context.session_dir(session_name) + private val file_dir = Path.explode(file_name).dir + private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty - override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = { + override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = body match { case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None case _ => - Some { + for (theory <- html_context.theory_by_name(session_name, theory_name)) + yield { val body1 = if (seen_ranges.contains(range)) { HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body)) } else HTML.span(body) - html_context.nodes(node.theory).get_defs(range).foldLeft(body1) { + theory.get_defs(file_name, range).foldLeft(body1) { case (elem, entity) => HTML.entity_def(HTML.span(HTML.id(entity.kname), List(elem))) } } } - } private def offset_id(range: Text.Range): String = "offset_" + range.start + ".." + range.stop - private def physical_ref(thy_name: String, props: Properties.T): Option[String] = { - for { - range <- Position.Def_Range.unapply(props) - if thy_name == node.theory - } yield { - seen_ranges += range - offset_id(range) - } - } - - private def logical_ref(thy_name: String, kind: String, name: String): Option[String] = - for { - node_info <- html_context.nodes.get(thy_name) - entity <- node_info.get_def(kind, name) - } yield entity.kname - override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = { props match { - case Theory_Ref(node_name) => - html_context.node_relative(session, node_name).map(html_dir => - HTML.link(html_dir + html_context.html_name_theory(node_name), body)) - case Entity_Ref(file_path, def_theory, kind, name) if file_path.get_ext == "thy" => + case Theory_Ref(thy_name) => + for (theory <- html_context.theory_by_name(session_name, thy_name)) + yield { + val html_path = session_dir + html_context.theory_html(theory) + val html_link = html_context.relative_link(file_dir, html_path) + HTML.link(html_link, body) + } + case Entity_Ref(def_file, kind, name) => + def logical_ref(theory: Nodes.Theory): Option[String] = + theory.get_def(def_file, kind, name).map(_.kname) + + def physical_ref(theory: Nodes.Theory): Option[String] = + props match { + case Position.Def_Range(range) if theory.name == theory_name => + seen_ranges += range + Some(offset_id(range)) + case _ => None + } + for { - thy_name <- - def_theory orElse (if (File.eq(node.path, file_path)) Some(node.theory) else None) - node_name = Resources.file_node(file_path, theory = thy_name) - html_dir <- html_context.node_relative(session, node_name) - html_file = html_context.html_name(node_name) - html_ref <- - logical_ref(thy_name, kind, name) orElse physical_ref(thy_name, props) - } yield { - HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body)) + theory <- html_context.theory_by_file(session_name, def_file) + html_ref <- logical_ref(theory) orElse physical_ref(theory) + } + yield { + val html_path = session_dir + html_context.smart_html(theory, def_file) + val html_link = html_context.relative_link(file_dir, html_path) + HTML.entity_ref(HTML.link(html_link + "#" + html_ref, body)) } case _ => None } @@ -539,13 +612,14 @@ ): Unit = { val session_name = session_context.session_name val session_info = session_context.sessions_structure(session_name) - val base = session_context.session_base val session_dir = Isabelle_System.make_directory(html_context.session_dir(session_name)).expand progress.echo("Presenting " + session_name + " in " + session_dir + " ...") + val session = html_context.nodes.the_session(session_name) + Bytes.write(session_dir + session_graph_path, graphview.Graph_File.make_pdf(session_info.options, session_context.session_base.session_graph_display)) @@ -583,18 +657,22 @@ map(link => HTML.text("View ") ::: List(link))).flatten } - def present_theory(name: Document.Node.Name): Option[XML.Body] = { + def present_theory(theory_name: String): Option[XML.Body] = { progress.expose_interrupt() - Build_Job.read_theory(session_context.theory(name.theory)).map { command => - if (verbose) progress.echo("Presenting theory " + name) + for { + command <- Build_Job.read_theory(session_context.theory(theory_name)) + theory <- html_context.theory_by_name(session_name, theory_name) + } + yield { + if (verbose) progress.echo("Presenting theory " + quote(theory_name)) val snapshot = Document.State.init.snippet(command) - val thy_elements = html_context.theory_elements(name) + val thy_elements = theory.elements(html_context.elements) val thy_html = html_context.source( - make_html(Entity_Context.make(session_name, name, html_context), + make_html(Entity_Context.make(html_context, session_name, theory_name, theory.thy_file), thy_elements, snapshot.xml_markup(elements = thy_elements.html))) val files_html = @@ -622,19 +700,18 @@ List(HTML.link(rel_path.implode, HTML.text(file_title))) } - val thy_title = "Theory " + name.theory_base_name + val thy_title = "Theory " + theory.print_short - HTML.write_document(session_dir, html_context.html_name_theory(name), + HTML.write_document(session_dir, html_context.theory_html(theory).implode, List(HTML.title(thy_title)), List(html_context.head(thy_title), thy_html), base = Some(html_context.root_dir)) - List(HTML.link(html_context.html_name_theory(name), - HTML.text(name.theory_base_name) ::: - (if (files.isEmpty) Nil else List(HTML.itemize(files))))) + List(HTML.link(html_context.theory_html(theory), + HTML.text(theory.print_short) ::: (if (files.isEmpty) Nil else List(HTML.itemize(files))))) } } - val theories = base.proper_session_theories.flatMap(present_theory) + val theories = session.used_theories.flatMap(present_theory) val title = "Session " + session_name HTML.write_document(session_dir, "index.html",