aboutsummaryrefslogtreecommitdiffhomepage
path: root/demo
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 12:24:39 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-05-03 12:24:39 -0400
commitd8de44ce7c70fc8ce462e764223e413a9a6ea6b6 (patch)
treebbd4fa663e5c412c295510f3cc6c75afa5191e48 /demo
parentebbae2ae752fe3b0774207920c7510853ffcbdcf (diff)
url demo
Diffstat (limited to 'demo')
-rw-r--r--demo/prose6
-rw-r--r--demo/url.ur13
-rw-r--r--demo/url.urp4
-rw-r--r--demo/url.urs1
4 files changed, 24 insertions, 0 deletions
diff --git a/demo/prose b/demo/prose
index 4dd15565..c6acf57d 100644
--- a/demo/prose
+++ b/demo/prose
@@ -64,6 +64,12 @@ cookie.urp
<p>After setting the cookie, try browsing back to this demo from the main index. The data you entered should still be there.</p>
+url.urp
+
+<p>Up to this point, we haven't included a single URL in our source code. This may be very surprising to programmers used to working with traditional web frameworks! In Ur/Web, we avoid writing URLs explicitly wherever possible. To link to an external web page, we rely on an abstract type <tt>url</tt>. Strings can't be treated implicitly as URLs; rather, they must be "blessed" explicitly. This helps avoid some classes of code injection attacks.</p>
+
+<p>Further, each Ur/Web application enforces a global condition on which strings are allowed as URLs. The <tt>.urp</tt> file for this demo shows an example that specifies particular rules about which URLs are allowed. You can try entering a variety of URLs on the form on the front page. Only those satisfying the <tt>allow url</tt>/<tt>deny url</tt> conditions should be permitted.</p>
+
listShop.urp
<p>This example shows off algebraic datatypes, parametric polymorphism, and functors.</p>
diff --git a/demo/url.ur b/demo/url.ur
new file mode 100644
index 00000000..48d1bdc3
--- /dev/null
+++ b/demo/url.ur
@@ -0,0 +1,13 @@
+fun yourChoice r = return <xml><body>
+ {case checkUrl r.Url of
+ None => <xml>You aren't allowed to link to there.</xml>
+ | Some url => <xml><a href={url}>Enjoy!</a></xml>}
+</body></xml>
+
+fun main () = return <xml><body>
+ <a href="http://en.wikipedia.org/wiki/Type_inference">Learn something</a><br/>
+ <br/>
+ <form>
+ URL of your choice: <textbox{#Url}/> <submit action={yourChoice}/>
+ </form>
+</body></xml>
diff --git a/demo/url.urp b/demo/url.urp
new file mode 100644
index 00000000..945e11d7
--- /dev/null
+++ b/demo/url.urp
@@ -0,0 +1,4 @@
+deny url http://en.wikipedia.org/wiki/PHP
+allow url http://en.wikipedia.org/wiki/*
+
+url
diff --git a/demo/url.urs b/demo/url.urs
new file mode 100644
index 00000000..6ac44e0b
--- /dev/null
+++ b/demo/url.urs
@@ -0,0 +1 @@
+val main : unit -> transaction page