diff -r c03e21a4cc26 -r ca4ecbbdd728 src/Pure/General/html.scala --- 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 */