Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more links;
authorwenzelm
Sun, 28 Aug 2022 11:57:38 +0200
changeset 76008 8897dfc2e7b0
parent 76007 08288b406005
child 76009 adf9c4d68581
more links;
src/Pure/Thy/browser_info.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/browser_info.scala	Sun Aug 28 11:53:48 2022 +0200
+++ b/src/Pure/Thy/browser_info.scala	Sun Aug 28 11:57:38 2022 +0200
@@ -158,7 +158,7 @@
   val default_elements: Elements =
     Elements(
       html = Rendering.foreground_elements ++ Rendering.text_color_elements +
-        Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE,
+        Markup.NUMERAL + Markup.COMMENT + Markup.ENTITY + Markup.LANGUAGE + Markup.URL,
       entity = Markup.Elements(Markup.THEORY, Markup.TYPE_NAME, Markup.CONSTANT, Markup.FACT,
         Markup.CLASS, Markup.LOCALE, Markup.FREE))
 
@@ -477,6 +477,9 @@
               }
             }
             else (body1, offset)
+          case XML.Elem(Markup.Url(href), body) =>
+            val (body1, offset) = html_body(body, end_offset)
+            (List(HTML.link(href, body1)), offset)
           case XML.Elem(Markup(Markup.LANGUAGE, Markup.Name(name)), body) =>
             val (body1, offset) = html_body(body, end_offset)
             (html_class(if (elements.language(name)) name else "", body1), offset)
isabelle