some HTML GUI elements;
authorwenzelm
Mon Jun 26 23:12:39 2017 +0200 (2017-06-26 ago)
changeset 6619631c9b09cc1d4
parent 66195 bb886f13623a
child 66197 c8604c9f3a8a
some HTML GUI elements;
src/Pure/PIDE/xml.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/PIDE/xml.scala	Mon Jun 26 15:57:20 2017 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Mon Jun 26 23:12:39 2017 +0200
     1.3 @@ -35,6 +35,7 @@
     1.4    }
     1.5    case class Text(content: String) extends Tree
     1.6  
     1.7 +  def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
     1.8    def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
     1.9    def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
    1.10  
     2.1 --- a/src/Pure/Thy/html.scala	Mon Jun 26 15:57:20 2017 +0200
     2.2 +++ b/src/Pure/Thy/html.scala	Mon Jun 26 23:12:39 2017 +0200
     2.3 @@ -224,6 +224,61 @@
     2.4      HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
     2.5  
     2.6  
     2.7 +  /* GUI elements */
     2.8 +
     2.9 +  object GUI
    2.10 +  {
    2.11 +    private def optional_value(text: String): XML.Attributes =
    2.12 +      proper_string(text).map(a => "value" -> a).toList
    2.13 +
    2.14 +    private def optional_name(name: String): XML.Attributes =
    2.15 +      proper_string(name).map(a => "name" -> a).toList
    2.16 +
    2.17 +    private def optional_title(tooltip: String): XML.Attributes =
    2.18 +      proper_string(tooltip).map(a => "title" -> a).toList
    2.19 +
    2.20 +    private def optional_submit(submit: Boolean): XML.Attributes =
    2.21 +      if (submit) List("onChange" -> "this.form.submit()") else Nil
    2.22 +
    2.23 +    private def optional_checked(selected: Boolean): XML.Attributes =
    2.24 +      if (selected) List("checked" -> "") else Nil
    2.25 +
    2.26 +    private def optional_action(action: String): XML.Attributes =
    2.27 +      proper_string(action).map(a => "action" -> a).toList
    2.28 +
    2.29 +    def button(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false)
    2.30 +        : XML.Elem =
    2.31 +      XML.Elem(
    2.32 +        Markup("button",
    2.33 +          List("type" -> (if (submit) "submit" else "button"), "value" -> "true") :::
    2.34 +          optional_name(name) ::: optional_title(tooltip)), body)
    2.35 +
    2.36 +    def checkbox(body: XML.Body, name: String = "", tooltip: String = "", submit: Boolean = false,
    2.37 +        selected: Boolean = false): XML.Elem =
    2.38 +      XML.elem("label",
    2.39 +        XML.elem(
    2.40 +          Markup("input",
    2.41 +            List("type" -> "checkbox", "value" -> "true") ::: optional_name(name) :::
    2.42 +              optional_title(tooltip) ::: optional_submit(submit) :::
    2.43 +              optional_checked(selected))) :: body)
    2.44 +
    2.45 +    def text_field(columns: Int = 0, text: String = "", name: String = "", tooltip: String = "",
    2.46 +        submit: Boolean = false): XML.Elem =
    2.47 +      XML.elem(Markup("input",
    2.48 +        List("type" -> "text") :::
    2.49 +          (if (columns > 0) List("size" -> columns.toString) else Nil) :::
    2.50 +          optional_value(text) ::: optional_name(name) :::
    2.51 +          optional_title(tooltip) ::: optional_submit(submit)))
    2.52 +
    2.53 +    def parameter(text: String = "", name: String = ""): XML.Elem =
    2.54 +      XML.elem(
    2.55 +        Markup("input", List("type" -> "hidden") ::: optional_value(text) ::: optional_name(name)))
    2.56 +
    2.57 +    def form(body: XML.Body, name: String = "", action: String = ""): XML.Elem =
    2.58 +      XML.Elem(Markup("form", optional_name(name) ::: optional_action(action)), body)
    2.59 +  }
    2.60 +
    2.61 +
    2.62    /* document */
    2.63  
    2.64    val header: String =