clarified signature: more operations;
authorwenzelm
Fri, 27 Dec 2024 17:26:01 +0100
changeset 81668 ca4ecbbdd728
parent 81667 c03e21a4cc26
child 81669 09c16e5636ad
clarified signature: more operations;
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 */