clarified signature: prefer enum types;

--- a/src/Pure/Thy/html.scala	Tue Aug 29 16:52:59 2023 +0200
+++ b/src/Pure/Thy/html.scala	Tue Aug 29 16:55:49 2023 +0200
@@ -355,15 +355,13 @@
   /* GUI layout */
 
   object Wrap_Panel {
-    object Alignment extends Enumeration {
-      val left, right, center = Value
-    }
+    enum Alignment { case left, right, center }
 
     def apply(
       contents: List[XML.Elem],
       name: String = "",
       action: String = "",
-      alignment: Alignment.Value = Alignment.right
+      alignment: Alignment = Alignment.right
     ): XML.Elem = {
       val body = Library.separate(XML.Text(" "), contents)
       GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),