# HG changeset patch # User Adam Chlipala # Date 1224624606 14400 # Node ID a71600cac815a22dccd4a37095b04e60d6a51462 # Parent 948315ea84c30e7d7e24bd9fe6ecaa3a83a80faf Form example diff -r 948315ea84c3 -r a71600cac815 demo/form.ur --- /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 + + + + +

A:	{[r.A]}
B:	{[r.B]}
C:	{[r.C]}

+ + +fun main () = return + + diff -r 948315ea84c3 -r a71600cac815 demo/form.urp --- /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 diff -r 948315ea84c3 -r a71600cac815 demo/form.urs --- /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 diff -r 948315ea84c3 -r a71600cac815 demo/listShop.urp --- 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 diff -r 948315ea84c3 -r a71600cac815 demo/prose --- 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 -

This is my second favorite.

In link.ur, 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.

+ +form.urp + +

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.

+ +

In the implementation of handler, we see the notation {[...]}, which uses type classes to inject values of different types (string and bool in this case) into XML. It's probably worth stating explicitly that XML fragments are not strings, so that the type-checker will enforce that our final piece of XML is valid.

listShop.urp diff -r 948315ea84c3 -r a71600cac815 lib/basis.urs --- 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 *)