--- a/src/Pure/System/web_app.scala Tue Aug 06 15:40:51 2024 +0200
+++ b/src/Pure/System/web_app.scala Tue Aug 06 16:58:05 2024 +0200
@@ -20,6 +20,7 @@
def name(n: String): Attribute = new Attribute("name", n)
def value(v: String): Attribute = new Attribute("value", v)
def placeholder(p: String): Attribute = new Attribute("placeholder", p)
+ def rowspan(n: Int): Attribute = new Attribute("rowspan", n.toString)
val nav = new Operator("nav")
val header = new Operator("header")
@@ -28,6 +29,11 @@
val fieldset = new Operator("fieldset")
val button = new Operator("button")
+ val table = new Operator("table")
+ val th = new Operator("th")
+ val tr = new Operator("tr")
+ val td = new Operator("td")
+
def icon(href: String): XML.Elem =
XML.Elem(Markup("link", List("rel" -> "icon", "type" -> "image/x-icon", "href" -> href)), Nil)