src/Pure/Thy/html.scala

--- a/src/Pure/Thy/html.scala	Tue Jun 27 00:07:34 2017 +0200
+++ b/src/Pure/Thy/html.scala	Tue Jun 27 11:47:14 2017 +0200
@@ -279,6 +279,25 @@
   }
 
 
+  /* GUI layout */
+
+  object Wrap_Panel
+  {
+    object Alignment extends Enumeration
+    {
+      val left, right, center = Value
+    }
+
+    def apply(contents: List[XML.Elem], name: String = "", action: String = "",
+      alignment: Alignment.Value = Alignment.center): XML.Elem =
+    {
+      val body = Library.separate(XML.Text(" "), contents)
+      GUI.form(List(div(body) + ("style" -> ("text-align: " + alignment))),
+        name = name, action = action)
+    }
+  }
+
+
   /* document */
 
   val header: String =