--- 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 =