diff options
author | Adam Chlipala <adamc@hcoop.net> | 2009-05-03 12:24:39 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-03 12:24:39 -0400 |
commit | d8de44ce7c70fc8ce462e764223e413a9a6ea6b6 (patch) | |
tree | bbd4fa663e5c412c295510f3cc6c75afa5191e48 | |
parent | ebbae2ae752fe3b0774207920c7510853ffcbdcf (diff) |
url demo
-rw-r--r-- | demo/prose | 6 | ||||
-rw-r--r-- | demo/url.ur | 13 | ||||
-rw-r--r-- | demo/url.urp | 4 | ||||
-rw-r--r-- | demo/url.urs | 1 | ||||
-rw-r--r-- | src/demo.sml | 31 |
5 files changed, 54 insertions, 1 deletions
@@ -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 => |