Mercurial > urweb
changeset 406:a71600cac815
Form example
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 21 Oct 2008 17:30:06 -0400 |
| parents | 948315ea84c3 |
| children | 345fcf91c806 |
| files | demo/form.ur demo/form.urp demo/form.urs demo/listShop.urp demo/prose lib/basis.urs |
| diffstat | 6 files changed, 37 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/form.ur Tue Oct 21 17:30:06 2008 -0400 @@ -0,0 +1,18 @@ +fun handler r = return <xml><body> + <table> + <tr> <th>A:</th> <td>{[r.A]}</td> </tr> + <tr> <th>B:</th> <td>{[r.B]}</td> </tr> + <tr> <th>C:</th> <td>{[r.C]}</td> </tr> + </table> +</body></xml> + +fun main () = return <xml><body> + <form> + <table> + <tr> <th>A:</th> <td><textbox{#A}/></td> </tr> + <tr> <th>B:</th> <td><textbox{#B}/></td> </tr> + <tr> <th>C:</th> <td><checkbox{#C}/></td> </tr> + <tr> <th/> <td><submit action={handler}/></td> </tr> + </table> + </form> +</body></xml>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/form.urp Tue Oct 21 17:30:06 2008 -0400 @@ -0,0 +1,2 @@ + +form
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/form.urs Tue Oct 21 17:30:06 2008 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page
--- a/demo/listShop.urp Tue Oct 21 17:12:22 2008 -0400 +++ b/demo/listShop.urp Tue Oct 21 17:30:06 2008 -0400 @@ -1,4 +1,3 @@ -debug list listFun
--- a/demo/prose Tue Oct 21 17:12:22 2008 -0400 +++ b/demo/prose Tue Oct 21 17:30:06 2008 -0400 @@ -36,7 +36,13 @@ link.urp -<p>This is my second favorite.</p> +<p>In <tt>link.ur</tt>, we see how easy it is to link to another page. The Ur/Web compiler guarantees that all links are valid. We just write some Ur/Web code inside an "antiquote" in our XML, denoting a transaction that will produce the new page if the link is clicked.</p> + +form.urp + +<p>Here we see a basic form. The type system tracks which form inputs we include, and it enforces that the form handler function expects a record containing exactly those fields, with exactly the proper types.</p> + +<p>In the implementation of <tt>handler</tt>, we see the notation <tt>{[...]}</tt>, which uses type classes to inject values of different types (<tt>string</tt> and <tt>bool</tt> in this case) into XML. It's probably worth stating explicitly that XML fragments <i>are not strings</i>, so that the type-checker will enforce that our final piece of XML is valid.</p> listShop.urp
--- a/lib/basis.urs Tue Oct 21 17:12:22 2008 -0400 +++ b/lib/basis.urs Tue Oct 21 17:30:06 2008 -0400 @@ -366,15 +366,19 @@ val submit : ctx ::: {Unit} -> use ::: {Type} -> fn [[Form] ~ ctx] => unit - -> tag [Action = $use -> transaction page] + -> tag [Value = string, Action = $use -> transaction page] ([Form] ++ ctx) ([Form] ++ ctx) use [] (*** Tables *) -val tabl : unit -> tag [Border = int] [Body] [Body, Table] [] [] -val tr : unit -> tag [] [Body, Table] [Body, Tr] [] [] -val th : unit -> tag [] [Body, Tr] [Body] [] [] -val td : unit -> tag [] [Body, Tr] [Body] [] [] +val tabl : other ::: {Unit} -> fn [other ~ [Body, Table]] => + unit -> tag [Border = int] ([Body] ++ other) ([Body, Table] ++ other) [] [] +val tr : other ::: {Unit} -> fn [other ~ [Body, Table, Tr]] => + unit -> tag [] ([Body, Table] ++ other) ([Body, Tr] ++ other) [] [] +val th : other ::: {Unit} -> fn [other ~ [Body, Tr]] => + unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] +val td : other ::: {Unit} -> fn [other ~ [Body, Tr]] => + unit -> tag [] ([Body, Tr] ++ other) ([Body] ++ other) [] [] (** Aborting *)