--- a/src/Pure/General/html.scala Fri Dec 27 16:54:48 2024 +0100
+++ b/src/Pure/General/html.scala Fri Dec 27 17:26:01 2024 +0100
@@ -7,6 +7,9 @@
package isabelle
+import java.awt.Color
+import java.util.Locale
+
import org.jsoup.nodes.{Entities => Jsoup_Entities, Document => Jsoup_Document}
import org.jsoup.Jsoup
@@ -111,6 +114,21 @@
def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))
+ def color(c: Color): String = {
+ val r = Integer.valueOf(c.getRed)
+ val g = Integer.valueOf(c.getGreen)
+ val b = Integer.valueOf(c.getBlue)
+ c.getAlpha match {
+ case 255 => String.format(Locale.ROOT, "rgb(%d,%d,%d)", r, g, b)
+ case a =>
+ String.format(Locale.ROOT, "rgba(%d,%d,%d,%.2f)", r, g, b,
+ java.lang.Double.valueOf(a.toDouble / 255))
+ }
+ }
+
+ def color_property(c: Color): String = "color: " + color(c)
+ def background_property(c: Color): String = "background: " + color(c)
+
/* href */