# HG changeset patch
# User wenzelm
# Date 1693320949 -7200
# Node ID 2401b5d9cee91230e87f779d1fd26afad3a7ba5c
# Parent  92b6958e87874b0b15d00c40bdb4f21f4fc060ed
clarified signature: prefer enum types;

diff -r 92b6958e8787 -r 2401b5d9cee9 src/Pure/Thy/html.scala
--- 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))),