summaryrefslogtreecommitdiff
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
parentebbae2ae752fe3b0774207920c7510853ffcbdcf (diff)
url demo
-rw-r--r--demo/prose6
-rw-r--r--demo/url.ur13
-rw-r--r--demo/url.urp4
-rw-r--r--demo/url.urs1
-rw-r--r--src/demo.sml31
5 files changed, 54 insertions, 1 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
diff --git a/src/demo.sml b/src/demo.sml
index 55ff5bb8..fb4158a4 100644
--- a/src/demo.sml
+++ b/src/demo.sml
@@ -104,7 +104,7 @@ fun make {prefix, dirname, guided} =
clientOnly = [],
serverOnly = [],
jsFuncs = [],
- rewrites = [],
+ rewrites = #rewrites combined @ #rewrites urp,
filterUrl = #filterUrl combined @ #filterUrl urp,
filterMime = #filterMime combined @ #filterMime urp
}
@@ -372,6 +372,35 @@ fun make {prefix, dirname, guided} =
TextIO.output (outf, "prefix ");
TextIO.output (outf, prefix);
TextIO.output (outf, "\n");
+ app (fn rule =>
+ (TextIO.output (outf, "rewrite ");
+ TextIO.output (outf, case #pkind rule of
+ Settings.Any => "any"
+ | Settings.Url => "url"
+ | Settings.Table => "table"
+ | Settings.Sequence => "sequence"
+ | Settings.View => "view"
+ | Settings.Relation => "relation"
+ | Settings.Cookie => "cookie"
+ | Settings.Style => "style");
+ TextIO.output (outf, " ");
+ TextIO.output (outf, #from rule);
+ case #kind rule of
+ Settings.Exact => ()
+ | Settings.Prefix => TextIO.output (outf, "*");
+ TextIO.output (outf, " ");
+ TextIO.output (outf, #to rule);
+ TextIO.output (outf, "\n"))) (#rewrites combined);
+ app (fn rule =>
+ (TextIO.output (outf, case #action rule of
+ Settings.Allow => "allow"
+ | Settings.Deny => "deny");
+ TextIO.output (outf, " url ");
+ TextIO.output (outf, #pattern rule);
+ case #kind rule of
+ Settings.Exact => ()
+ | Settings.Prefix => TextIO.output (outf, "*");
+ TextIO.output (outf, "\n"))) (#filterUrl combined);
TextIO.output (outf, "\n");
app (fn s =>