merged
authorwenzelm
Thu, 11 Nov 2021 22:35:23 +0100
changeset 75150 2e3b649111f1
parent 75143 bae4731cba8f (current diff)
parent 75149 a6c7a257b713 (diff)
child 75151 6cb700c77786
merged
--- 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)
--- 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 */
 
--- 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")
--- 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)
--- 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)
           })
--- 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) =>
--- 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
--- 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
                 }
--- 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)