# HG changeset patch # User desharna # Date 1718019549 -7200 # Node ID cdf26ac90f873f3686786055bfc6fdd06807ec09 # Parent be2e772e0adff76b0d53fe1d1e9a8ac13de82c95# Parent a82db14570cd027edb9da02baf162ae1a37e3fdb merged diff -r be2e772e0adf -r cdf26ac90f87 src/Pure/Build/build_manager.scala --- a/src/Pure/Build/build_manager.scala Mon Jun 10 08:34:09 2024 +0200 +++ b/src/Pure/Build/build_manager.scala Mon Jun 10 13:39:09 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 be2e772e0adf -r cdf26ac90f87 src/Pure/System/web_app.scala --- a/src/Pure/System/web_app.scala Mon Jun 10 08:34:09 2024 +0200 +++ b/src/Pure/System/web_app.scala Mon Jun 10 13:39:09 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 =