# HG changeset patch # User wenzelm # Date 1636666523 -3600 # Node ID 2e3b649111f168306de8783c05bb1c5c4d2a914f # Parent bae4731cba8f06a363d02733200bbb325d4cf58b# Parent a6c7a257b7138df18f2a6ff16eeb04898c08c1ec merged diff -r bae4731cba8f -r 2e3b649111f1 src/Pure/PIDE/document_status.scala --- a/src/Pure/PIDE/document_status.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Pure/PIDE/document_status.scala Thu Nov 11 22:35:23 2021 +0100 @@ -268,7 +268,7 @@ val update_iterator = for { name <- domain.getOrElse(nodes1.domain).iterator - if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name) + if !Resources.hidden_node(name) && !resources.session_base.loaded_theory(name) st = Document_Status.Node_Status.make(state, version, name) if !rep.isDefinedAt(name) || rep(name) != st } yield (name -> st) diff -r bae4731cba8f -r 2e3b649111f1 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Pure/PIDE/resources.scala Thu Nov 11 22:35:23 2021 +0100 @@ -16,6 +16,15 @@ { def empty: Resources = new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap) + + def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name = + empty.file_node(file, dir = dir, theory = theory) + + def hidden_node(name: Document.Node.Name): Boolean = + !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) + + def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = + File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot)) } class Resources( @@ -60,12 +69,6 @@ def make_theory_content(thy_name: Document.Node.Name): Option[String] = File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name)) - def is_hidden(name: Document.Node.Name): Boolean = - !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name) - - def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] = - File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot)) - /* file-system operations */ diff -r bae4731cba8f -r 2e3b649111f1 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Pure/Thy/html.scala Thu Nov 11 22:35:23 2021 +0100 @@ -420,7 +420,8 @@ base match { case None => "" case Some(base_dir) => - File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile).implode + val path = File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile) + if (path.is_current) "" else path.implode + "/" } def isabelle_css: Path = Path.explode("~~/etc/isabelle.css") diff -r bae4731cba8f -r 2e3b649111f1 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Pure/Thy/presentation.scala Thu Nov 11 22:35:23 2021 +0100 @@ -50,9 +50,6 @@ def source(body: XML.Body): XML.Tree = HTML.pre("source", body) - def physical_ref(range: Text.Range): String = - "offset_" + range.start + ".." + range.stop - def contents(heading: String, items: List[XML.Body], css_class: String = "contents") : List[XML.Elem] = { @@ -97,9 +94,92 @@ type Entity = Export_Theory.Entity[Export_Theory.No_Content] - case class Entity_Context(node: Document.Node.Name) + object Entity_Context { - val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty + val empty: Entity_Context = new Entity_Context + + def make( + session: String, + deps: Sessions.Deps, + node: Document.Node.Name, + theory_exports: Map[String, Export_Theory.Theory]): Entity_Context = + new Entity_Context { + private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty + + 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 { + val entities = + theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range)) + .getOrElse(Nil) + val body1 = + if (seen_ranges.contains(range)) { + HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body)) + } + else HTML.span(body) + entities.map(_.kname).foldLeft(body1) { + case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), 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 { + thy <- theory_exports.get(thy_name) + entity <- thy.entity_by_kind_name.get((kind, name)) + } yield entity.kname + + override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = + { + (props, props, props, props, props) match { + case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) => + val node_name = Resources.file_node(Path.explode(thy_file), theory = theory) + node_relative(deps, session, node_name).map(html_dir => + HTML.link(html_dir + html_name(node_name), body)) + case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory), + Markup.Kind(kind), Markup.Name(name)) => + val file_path = Path.explode(def_file) + val proper_thy_name = + proper_string(def_theory) orElse + (if (File.eq(node.path, file_path)) Some(node.theory) else None) + for { + thy_name <- proper_thy_name + node_name = Resources.file_node(file_path, theory = thy_name) + html_dir <- node_relative(deps, session, node_name) + html_file = node_file(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)) + } + case _ => None + } + } + } + } + + class Entity_Context + { + def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None + def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = None } @@ -110,14 +190,10 @@ HTML.descr.name) def make_html( - name: Document.Node.Name, + entity_context: Entity_Context, elements: Elements, - entity_anchor: (Entity_Context, Symbol.Range, XML.Body) => Option[XML.Tree], - entity_link: (Entity_Context, Properties.T, XML.Body) => Option[XML.Tree], xml: XML.Body): XML.Body = { - val context = Entity_Context(name) - def html_div(html: XML.Body): Boolean = html exists { case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body) @@ -142,7 +218,7 @@ case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) => val (body1, offset) = html_body(body, end_offset) if (elements.entity(kind)) { - entity_link(context, props, body1) match { + entity_context.make_ref(props, body1) match { case Some(link) => (List(link), offset) case None => (body1, offset) } @@ -180,7 +256,7 @@ case XML.Text(text) => val offset = end_offset - Symbol.length(text) val body = HTML.text(Symbol.decode(text)) - entity_anchor(context, Text.Range(offset, end_offset), body) match { + entity_context.make_def(Text.Range(offset, end_offset), body) match { case Some(body1) => (List(body1), offset) case None => (body, offset) } @@ -193,7 +269,6 @@ /* PIDE HTML document */ def html_document( - resources: Resources, snapshot: Document.Snapshot, html_context: HTML_Context, elements: Elements, @@ -209,12 +284,12 @@ html_context.html_document(title, body, fonts_css) } else { - resources.html_document(snapshot) getOrElse { + Resources.html_document(snapshot) getOrElse { val title = if (name.is_theory) "Theory " + quote(name.theory_base_name) else "File " + Symbol.cartouche_decoded(name.path.file_name) val xml = snapshot.xml_markup(elements = elements.html) - val body = make_html(name, elements, (_, _, _) => None, (_, _, _) => None, xml) + val body = make_html(Entity_Context.empty, elements, xml) html_context.html_document(title, body, fonts_css) } } @@ -345,7 +420,10 @@ def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode def html_path(path: Path): String = (files_path + path.squash.html).implode - def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] = + private def node_file(node: Document.Node.Name): String = + if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node)) + + private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] = { for { info0 <- deps.sessions_structure.get(session0) @@ -376,7 +454,6 @@ } def session_html( - resources: Resources, session: String, deps: Sessions.Deps, db_context: Sessions.Database_Context, @@ -455,6 +532,9 @@ thy_name -> theory }).toMap + def entity_context(name: Document.Node.Name): Entity_Context = + Entity_Context.make(session, deps, name, theory_exports) + val theories: List[XML.Body] = { sealed case class Seen_File( @@ -465,73 +545,6 @@ } var seen_files = List.empty[Seen_File] - def node_file(node: Document.Node.Name): String = - if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node)) - - def entity_anchor( - context: Entity_Context, range: Symbol.Range, body: XML.Body): Option[XML.Elem] = - { - body match { - case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None - case _ => - Some { - val entities = - theory_exports.get(context.node.theory).flatMap(_.entity_by_range.get(range)) - .getOrElse(Nil) - val body1 = - if (context.seen_ranges.contains(range)) { - HTML.entity_def(HTML.span(HTML.id(html_context.physical_ref(range)), body)) - } - else HTML.span(body) - entities.map(_.kname).foldLeft(body1) { - case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem))) - } - } - } - } - - def logical_ref(thy_name: String, kind: String, name: String): Option[String] = - for { - thy <- theory_exports.get(thy_name) - entity <- thy.entity_by_kind_name.get((kind, name)) - } yield entity.kname - - def physical_ref( - context: Entity_Context, thy_name: String, props: Properties.T): Option[String] = - { - for { - range <- Position.Def_Range.unapply(props) - if thy_name == context.node.theory - } yield { - context.seen_ranges += range - html_context.physical_ref(range) - } - } - - def entity_link( - context: Entity_Context, props: Properties.T, body: XML.Body): Option[XML.Elem] = - { - (props, props, props, props, props) match { - case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) => - val node_name = resources.file_node(Path.explode(thy_file), theory = theory) - node_relative(deps, session, node_name).map(html_dir => - HTML.link(html_dir + html_name(node_name), body)) - case (Markup.Ref(_), Position.Def_File(thy_file), Position.Def_Theory(def_theory), - Markup.Kind(kind), Markup.Name(name)) => - val thy_name = if (def_theory.nonEmpty) def_theory else context.node.theory - val node_name = resources.file_node(Path.explode(thy_file), theory = thy_name) - for { - html_dir <- node_relative(deps, session, node_name) - html_file = node_file(node_name) - html_ref <- - logical_ref(thy_name, kind, name) orElse physical_ref(context, thy_name, props) - } yield { - HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body)) - } - case _ => None - } - } - sealed case class Theory( name: Document.Node.Name, command: Command, @@ -542,7 +555,7 @@ { progress.expose_interrupt() - for (command <- Build_Job.read_theory(db_context, resources, hierarchy, name.theory)) + for (command <- Build_Job.read_theory(db_context, hierarchy, name.theory)) yield { if (verbose) progress.echo("Presenting theory " + name) val snapshot = Document.State.init.snippet(command) @@ -561,12 +574,12 @@ if (verbose) progress.echo("Presenting file " + src_path) (src_path, html_context.source( - make_html(name, thy_elements, entity_anchor, entity_link, xml))) + make_html(entity_context(name), thy_elements, xml))) } val html = html_context.source( - make_html(name, thy_elements, entity_anchor, entity_link, + make_html(entity_context(name), thy_elements, snapshot.xml_markup(elements = thy_elements.html))) Theory(name, command, files_html, html) diff -r bae4731cba8f -r 2e3b649111f1 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Pure/Tools/build.scala Thu Nov 11 22:35:23 2021 +0100 @@ -506,7 +506,6 @@ Presentation.update_chapter(presentation_dir, chapter, entries) } - val resources = Resources.empty val html_context = Presentation.html_context(cache = store.cache) using(store.open_database_context())(db_context => @@ -514,7 +513,7 @@ progress.expose_interrupt() progress.echo("Presenting " + info.name + " ...") Presentation.session_html( - resources, info.name, deps, db_context, progress = progress, + info.name, deps, db_context, progress = progress, verbose = verbose, html_context = html_context, Presentation.elements1, presentation = presentation) }) diff -r bae4731cba8f -r 2e3b649111f1 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Pure/Tools/build_job.scala Thu Nov 11 22:35:23 2021 +0100 @@ -18,7 +18,6 @@ def read_theory( db_context: Sessions.Database_Context, - resources: Resources, session_hierarchy: List[String], theory: String, unicode_symbols: Boolean = false): Option[Command] = @@ -33,7 +32,7 @@ (read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match { case (Value.Long(id), thy_file :: blobs_files) => - val node_name = resources.file_node(Path.explode(thy_file), theory = theory) + val node_name = Resources.file_node(Path.explode(thy_file), theory = theory) val results = Command.Results.make( @@ -44,7 +43,7 @@ blobs_files.map(file => { val path = Path.explode(file) - val name = resources.file_node(path) + val name = Resources.file_node(path) val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) Command.Blob(name, src_path, None) }) @@ -95,8 +94,7 @@ unicode_symbols: Boolean = false): Unit = { val store = Sessions.store(options) - val resources = Resources.empty - val session = new Session(options, resources) + val session = new Session(options, Resources.empty) using(store.open_database_context())(db_context => { @@ -118,8 +116,7 @@ if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet) for (thy <- print_theories) { val thy_heading = "\nTheory " + quote(thy) + ":" - read_theory(db_context, resources, List(session_name), thy, - unicode_symbols = unicode_symbols) + read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols) match { case None => progress.echo(thy_heading + " MISSING") case Some(command) => diff -r bae4731cba8f -r 2e3b649111f1 src/Pure/Tools/profiling_report.scala --- a/src/Pure/Tools/profiling_report.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Pure/Tools/profiling_report.scala Thu Nov 11 22:35:23 2021 +0100 @@ -17,7 +17,6 @@ progress: Progress = new Progress): Unit = { val store = Sessions.store(options) - val resources = Resources.empty using(store.open_database_context())(db_context => { @@ -34,7 +33,7 @@ (for { thy <- used_theories.iterator if theories.isEmpty || theories.contains(thy) - command <- Build_Job.read_theory(db_context, resources, List(session), thy).iterator + command <- Build_Job.read_theory(db_context, List(session), thy).iterator snapshot = Document.State.init.snippet(command) (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator } yield if (clean_name) report.clean_name else report).toList diff -r bae4731cba8f -r 2e3b649111f1 src/Tools/VSCode/src/preview_panel.scala --- a/src/Tools/VSCode/src/preview_panel.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Tools/VSCode/src/preview_panel.scala Thu Nov 11 22:35:23 2021 +0100 @@ -33,8 +33,7 @@ else { val html_context = Presentation.html_context() val document = - Presentation.html_document( - resources, snapshot, html_context, Presentation.elements2) + Presentation.html_document(snapshot, html_context, Presentation.elements2) channel.write(LSP.Preview_Response(file, column, document.title, document.content)) m - file } diff -r bae4731cba8f -r 2e3b649111f1 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Thu Nov 11 11:51:25 2021 +0000 +++ b/src/Tools/jEdit/src/document_model.scala Thu Nov 11 22:35:23 2021 +0100 @@ -327,7 +327,7 @@ val html_context = Presentation.html_context() val document = Presentation.html_document( - PIDE.resources, snapshot, html_context, Presentation.elements2, + snapshot, html_context, Presentation.elements2, plain_text = query.startsWith(plain_text_prefix), fonts_css = HTML.fonts_css_dir(http_root)) HTTP.Response.html(document.content)