summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 17:30:06 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-10-21 17:30:06 -0400
commitd4e5d7bbce0aac719ac2c6451e0a6bfb675ab641 (patch)
tree5f06bbcd006f618093f9483a42e3e642ee9ea91c
parent5411e88620c19474569ce7c2280235beaa6cd1f5 (diff)
Form example
-rw-r--r--demo/form.ur18
-rw-r--r--demo/form.urp2
-rw-r--r--demo/form.urs1
-rw-r--r--demo/listShop.urp1
-rw-r--r--demo/prose8
-rw-r--r--lib/basis.urs14
6 files changed, 37 insertions, 7 deletions
diff --git a/demo/form.ur b/demo/form.ur
new file mode 100644
index 00000000..ec466db3
--- /dev/null
+++ b/demo/form.ur
@@ -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>
diff --git a/demo/form.urp b/demo/form.urp
new file mode 100644
index 00000000..73356d49
--- /dev/null
+++ b/demo/form.urp
@@ -0,0 +1,2 @@
+
+form
diff --git a/demo/form.urs b/demo/form.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/form.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page
diff --git a/demo/listShop.urp b/demo/listShop.urp
index 219c6828..85d318d4 100644
--- a/demo/listShop.urp
+++ b/demo/listShop.urp
@@ -1,4 +1,3 @@
-debug
list
listFun
diff --git a/demo/prose b/demo/prose
index 36fd14ea..fe4eb1ea 100644
--- a/demo/prose
+++ b/demo/prose
@@ -36,7 +36,13 @@ hello.urp
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
diff --git a/lib/basis.urs b/lib/basis.urs
index de4204b3..212cccc6 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -366,15 +366,19 @@ val option : unit -> tag [Value = string] select [] [] []
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 *)