# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717780476 -7200
# Node ID a82db14570cd027edb9da02baf162ae1a37e3fdb
# Parent  594356f1681084df2a44db34dd61172f839eeffc
add favicon to web app;

diff -r 594356f16810 -r a82db14570cd src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Sun Jun 09 22:40:13 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 07 19:14:36 2024 +0200
@@ -1095,8 +1095,10 @@
         Get(Page.OVERVIEW, "overview", get_overview),
         Get(Page.BUILD, "build", get_build),
         Post(API.BUILD_CANCEL, "cancel build", cancel_build))
+      val logo = Bytes.read(Path.explode("$ISABELLE_HOME/lib/logo/isabelle_transparent-48.gif"))
       val head =
         List(
+          Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64),
           HTML.style_file("https://hawkz.github.io/gdcss/gd.css"),
           HTML.style("html { background-color: white; }"))
     }
diff -r 594356f16810 -r a82db14570cd src/Pure/System/web_app.scala
--- a/src/Pure/System/web_app.scala	Sun Jun 09 22:40:13 2024 +0200
+++ b/src/Pure/System/web_app.scala	Fri Jun 07 19:14:36 2024 +0200
@@ -28,6 +28,9 @@
     val fieldset = new Operator("fieldset")
     val button = new Operator("button")
 
+    def icon(href: String): XML.Elem =
+      XML.Elem(Markup("link", List("rel" -> "icon", "type" -> "image/x-icon", "href" -> href)), Nil)
+
     def legend(txt: String): XML.Elem = XML.Elem(Markup("legend", Nil), text(txt))
     def input(typ: String): XML.Elem = XML.Elem(Markup("input", List("type" -> typ)), Nil)
     def hidden(k: Params.Key, v: String): XML.Elem =