# HG changeset patch
# User wenzelm
# Date 1498556834 -7200
# Node ID 02c66b71c01372303496256a003a83d6fbde1a24
# Parent  4a5589dd8e1a8747fc63a0a499d2df6beb1bb996
GUI layout similar to Pure/GUI/wrap_panel.scala;

diff -r 4a5589dd8e1a -r 02c66b71c013 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 =