merged draft
authorFabian Huch <huch@in.tum.de>
Tue, 28 Sep 2021 11:30:14 +0200
changeset 74744 a6b85db273e1
parent 74738 d8dc8fdc46fc (current diff)
parent 74743 194e9d443840 (diff)
child 74745 fea3966fa72a
child 74746 7d71fb119ffa
merged
--- a/etc/isabelle.css	Tue Sep 28 10:47:18 2021 +0200
+++ b/etc/isabelle.css	Tue Sep 28 11:30:14 2021 +0200
@@ -12,6 +12,11 @@
   background-color: #FFFFFF;
 }
 
+a {
+    color: inherit;
+    text-decoration: inherit;
+}
+
 .head     { background-color: #FFFFFF; }
 .source   {
   direction: ltr; unicode-bidi: bidi-override;
--- a/src/Pure/General/position.scala	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/General/position.scala	Tue Sep 28 11:30:14 2021 +0200
@@ -29,7 +29,7 @@
   val Def_File = new Properties.String(Markup.DEF_FILE)
   val Def_Id = new Properties.Long(Markup.DEF_ID)
 
-  val Def_Theory = new Properties.Long(Markup.DEF_THEORY)
+  val Def_Theory = new Properties.String(Markup.DEF_THEORY)
 
   object Line_File
   {
--- a/src/Pure/Thy/presentation.scala	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Thy/presentation.scala	Tue Sep 28 11:30:14 2021 +0200
@@ -7,7 +7,9 @@
 package isabelle
 
 
+import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
+import scala.collection.mutable
 
 
 object Presentation
@@ -37,6 +39,12 @@
 
     def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
 
+    def offset_ref(offset: Text.Range): String =
+      "offset/" + offset.start + ".." + offset.stop
+
+    def export_ref(entity: Export_Theory.Entity[Export_Theory.No_Content]): String =
+      Export_Theory.export_kind(entity.kind) + "/" + entity.name
+
     def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
       : List[XML.Elem] =
     {
@@ -65,10 +73,10 @@
 
   val elements1: Elements =
     Elements(
-      html =
-        Rendering.foreground_elements ++ Rendering.text_color_elements +
+      html = Rendering.foreground_elements ++ Rendering.text_color_elements +
         Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
-      entity = Markup.Elements(Markup.THEORY))
+      entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
+        Markup.CLASS, Markup.LOCALE, Markup.FREE))
 
   val elements2: Elements =
     Elements(
@@ -82,11 +90,19 @@
     Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
       HTML.descr.name)
 
+  case class Entity_Context(node: Document.Node.Name) {
+    val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+  }
+
   def make_html(
+    name: Document.Node.Name,
     elements: Elements,
-    entity_link: (Properties.T, XML.Body) => Option[XML.Tree],
+    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)
@@ -98,46 +114,65 @@
       else if (html_div(html)) List(HTML.div(c, html))
       else List(HTML.span(c, html))
 
-    def html_body(xml_body: XML.Body): XML.Body =
-      xml_body flatMap {
-        case XML.Wrapped_Elem(markup, _, body) => html_body(List(XML.Elem(markup, body)))
+    def html_body(xml_body: XML.Body, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
+      xml_body.foldRight((List.empty[XML.Tree], end_offset)) { case (tree, (res, end_offset1)) =>
+        val (res1, offset) = html_body_single(tree, end_offset1)
+        (res1 ++ res, offset)
+      }
+
+    @tailrec
+    def html_body_single(xml_tree: XML.Tree, end_offset: Symbol.Offset): (XML.Body, Symbol.Offset) =
+      xml_tree match {
+        case XML.Wrapped_Elem(markup, _, body) => html_body_single(XML.Elem(markup, body), end_offset)
         case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
-          val body1 = html_body(body)
+          val (body1, offset) = html_body(body, end_offset)
           if (elements.entity(kind)) {
-            entity_link(props, body1) match {
-              case Some(link) => List(link)
-              case None => body1
+            entity_link(context, props, body1) match {
+              case Some(link) => (List(link), offset)
+              case None => (body1, offset)
             }
           }
-          else body1
+          else (body1, offset)
         case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
-          html_class(if (elements.language(name)) name else "", html_body(body))
+          val (body1, offset) = html_body(body, end_offset)
+          (html_class(if (elements.language(name)) name else "", body1), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), body) =>
-          List(HTML.par(html_body(body)))
+          val (body1, offset) = html_body(body, end_offset)
+          (List(HTML.par(body1)), offset)
         case XML.Elem(Markup(Markup.MARKDOWN_ITEM, _), body) =>
-          List(HTML.item(html_body(body)))
-        case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), _) => Nil
+          val (body1, offset) = html_body(body, end_offset)
+          (List(HTML.item(body1)), offset)
+        case XML.Elem(Markup(Markup.Markdown_Bullet.name, _), text) =>
+          (Nil, end_offset - Symbol.length(Symbol.decode(XML.content(text))))
         case XML.Elem(Markup.Markdown_List(kind), body) =>
-          if (kind == Markup.ENUMERATE) List(HTML.enum(html_body(body)))
-          else List(HTML.list(html_body(body)))
+          val (body1, offset) = html_body(body, end_offset)
+          if (kind == Markup.ENUMERATE) (List(HTML.enum(body1)), offset)
+          else (List(HTML.list(body1)), offset)
         case XML.Elem(markup, body) =>
           val name = markup.name
+          val (body1, offset) = html_body(body, end_offset)
           val html =
             markup.properties match {
               case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
-                html_class(kind, html_body(body))
+                html_class(kind, body1)
               case _ =>
-                html_body(body)
+                body1
             }
           Rendering.foreground.get(name) orElse Rendering.text_color.get(name) match {
-            case Some(c) => html_class(c.toString, html)
-            case None => html_class(name, html)
+            case Some(c) => (html_class(c.toString, html), offset)
+            case None => (html_class(name, html), offset)
           }
         case XML.Text(text) =>
-          HTML.text(Symbol.decode(text))
+          val decoded = Symbol.decode(text)
+          val offset = end_offset - Symbol.length(decoded)
+          val body = HTML.text(decoded)
+          entity_anchor(context, Text.Range(offset, end_offset), body) match {
+            case Some(body1) => (List(body1), offset)
+            case None => (body, offset)
+          }
       }
 
-    html_body(xml)
+    html_body(xml, Symbol.length(Symbol.decode(XML.content(xml))) + 1)._1
   }
 
 
@@ -163,7 +198,8 @@
         val title =
           if (name.is_theory) "Theory " + quote(name.theory_base_name)
           else "File " + Symbol.cartouche_decoded(name.path.file_name)
-        val body = make_html(elements, (_, _) => None, snapshot.xml_markup(elements = elements.html))
+        val xml = snapshot.xml_markup(elements = elements.html)
+        val body = make_html(name, elements, (_, _, _) => None, (_, _, _) => None, xml)
         html_context.html_document(title, body)
       }
     }
@@ -266,7 +302,7 @@
   <center>
     <table width="100%" border="0" cellspacing="10" cellpadding="0">
       <tr>
-        <td width="20%" valign="middle" align="center"><a href="http://isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td>
+        <td width="20%" valign="middle" align="center"><a href="//isabelle.in.tum.de/"><img align="bottom" src="isabelle.gif" width="100" height="86" alt="[Isabelle]" border="0" /></a></td>
 
         <td width="80%" valign="middle" align="center">
           <table width="90%" border="0" cellspacing="0" cellpadding="20">
@@ -286,7 +322,7 @@
       <ul>
         <li><a href="HOL/index.html">HOL (Higher-Order Logic)</a>
         is a version of classical higher-order logic resembling
-        that of the <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
+        that of the <a href="//www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</a>.
         </li>
       </ul>
     </li>
@@ -345,16 +381,35 @@
   val readme_path = Path.explode("README.html")
   val files_path = Path.explode("files")
 
-  def html_name(name: Document.Node.Name): String = name.theory_base_name + ".html"
+  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] =
+  {
+    for {
+      info0 <- deps.sessions_structure.get(session0)
+      info1 <- deps.sessions_structure.get(session1)
+    } yield info0.relative_path(info1)
+  }
+
+  def node_relative(
+    deps: Sessions.Deps,
+    session0: String,
+    node_name: Document.Node.Name): Option[String] =
+  {
+    val session1 = deps(session0).theory_qualifier(node_name)
+    session_relative(deps, session0, session1)
+  }
 
   def theory_link(deps: Sessions.Deps, session0: String,
-    name: Document.Node.Name, body: XML.Body): Option[XML.Tree] =
+    name: Document.Node.Name, body: XML.Body, anchor: Option[String] = None): Option[XML.Tree] =
   {
     val session1 = deps(session0).theory_qualifier(name)
     val info0 = deps.sessions_structure.get(session0)
     val info1 = deps.sessions_structure.get(session1)
+    val fragment = if (anchor.isDefined) "#" + anchor.get else ""
     if (info0.isDefined && info1.isDefined) {
-      Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name), body))
+      Some(HTML.link(info0.get.relative_path(info1.get) + html_name(name) + fragment, body))
     }
     else None
   }
@@ -411,17 +466,101 @@
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
+    def read_exports(name: Document.Node.Name) =
+    {
+      if (Sessions.is_pure(name.theory_base_name)) {
+        Vector.empty
+      } else {
+        val session1 = deps(session).theory_qualifier(name)
+        val provider = Export.Provider.database_context(db_context, List(session1), name.theory)
+        provider(Export.THEORY_PREFIX + "parents") match {
+          case Some(_) =>
+            val theory = Export_Theory.read_theory(provider, session1, name.theory)
+            theory.entity_iterator.toVector
+          case None =>
+            progress.echo_error_message("No exports for: " + name)
+            Vector.empty
+        }
+      }
+    }
+
+    val exports = base.known_theories.map(_._2.name).map(node => node -> read_exports(node)).toMap
+
+    val export_ranges = exports.view.mapValues(_.groupBy { entity =>
+      Text.Range(Position.Offset.get(entity.pos), Position.End_Offset.get(entity.pos))
+    }).toMap
+
+    val export_names = exports.map {
+      case (node, entities) => node.theory -> entities.map(entity => entity.name -> entity).toMap
+    }
+
     val theories: List[XML.Body] =
     {
       var seen_files = List.empty[(Path, String, Document.Node.Name)]
 
-      def entity_link(props: Properties.T, body: XML.Body): Option[XML.Tree] =
-        (props, props, props) match {
-          case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file)) =>
+      def node_file(node: Document.Node.Name) =
+        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) =
+      {
+        body match {
+          case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
+          case _ =>
+            Some {
+              val body1 = if (context.seen_ranges.contains(range)) {
+                HTML.span(HTML.id(html_context.offset_ref(range)), body)
+              } else HTML.span(body)
+              export_ranges.get(context.node).flatMap(_.get(range)) match {
+                case Some(entities) =>
+                  entities.map(html_context.export_ref).foldLeft(body1) {
+                    case (elem, id) => HTML.span(HTML.id(id), List(elem))
+                  }
+                case None => body1
+              }
+            }
+        }
+      }
+
+      def entity_ref(theory: String, name: String) =
+      {
+        export_names.get(theory).flatMap(_.get(name)).map(html_context.export_ref)
+      }
+
+      def offset_ref(context: Entity_Context, theory: String, props: Properties.T) = {
+        if (theory == context.node.theory) {
+          for {
+            offset <- Position.Def_Offset.unapply(props)
+            end_offset <- Position.Def_End_Offset.unapply(props)
+            range = Text.Range(offset, end_offset)
+          } yield {
+            context.seen_ranges += range
+            html_context.offset_ref(range)
+          }
+        } else None
+      }
+
+      def entity_link(context: Entity_Context, props: Properties.T, body: XML.Body) =
+      {
+        (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)
-            theory_link(deps, session, node_name, body)
+            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.Name(name)) =>
+            val theory = if (def_theory.nonEmpty) def_theory else context.node.theory
+            val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
+            for {
+              html_dir <- node_relative(deps, session, node_name)
+              html_file = node_file(node_name)
+              html_ref <- entity_ref(theory, name).orElse(offset_ref(context, theory, props))
+            } yield {
+              HTML.link(html_dir + html_file + "#" + html_ref, body)
+            }
           case _ => None
         }
+      }
 
       sealed case class Theory(
         name: Document.Node.Name,
@@ -447,12 +586,14 @@
               progress.expose_interrupt()
               if (verbose) progress.echo("Presenting file " + src_path)
 
-              (src_path, html_context.source(make_html(elements, entity_link, xml)))
+              (src_path, html_context.source(
+                make_html(name, elements, entity_anchor, entity_link, xml)))
             }
 
           val html =
             html_context.source(
-              make_html(elements, entity_link, snapshot.xml_markup(elements = elements.html)))
+              make_html(name, elements, entity_anchor, entity_link,
+                snapshot.xml_markup(elements = elements.html)))
 
           Theory(name, command, files_html, html)
         }
@@ -463,7 +604,7 @@
         val files =
           for { (src_path, file_html) <- thy.files_html }
           yield {
-            val file_name = (files_path + src_path.squash.html).implode
+            val file_name = html_path(src_path)
 
             seen_files.find(p => p._1 == src_path || p._2 == file_name) match {
               case None => seen_files ::= (src_path, file_name, thy.name)