annotate tests/blob.ur @ 1034:a779402841f6
Hooks for measuring how much interesting proving is going on in elaboration
author |
Adam Chlipala <adamc@hcoop.net> |
date |
Tue, 17 Nov 2009 12:44:14 -0500 |
parents |
034eeb099564 |
children |
67ebd30a2283 |
rev |
line source |
adamc@737
|
1 sequence s
|
adamc@740
|
2 table t : { Id : int, Nam : option string, Data : blob, Desc : string, Typ : string }
|
adamc@737
|
3
|
adamc@890
|
4 fun see id =
|
adamc@742
|
5 r <- oneRow (SELECT t.Data, t.Typ FROM t WHERE t.Id = {[id]});
|
adamc@742
|
6 returnBlob r.T.Data (blessMime r.T.Typ)
|
adamc@742
|
7
|
adamc@737
|
8 fun save r =
|
adamc@739
|
9 id <- nextval s;
|
adamc@740
|
10 dml (INSERT INTO t (Id, Nam, Data, Desc, Typ)
|
adamc@740
|
11 VALUES ({[id]}, {[fileName r.Data]}, {[fileData r.Data]}, {[r.Desc]}, {[fileMimeType r.Data]}));
|
adamc@739
|
12 main ()
|
adamc@737
|
13
|
adamc@742
|
14 and main () =
|
adamc@746
|
15 ls <- queryX (SELECT t.Id, t.Desc, octet_length(t.Data) AS Len FROM t ORDER BY t.Desc)
|
adamc@890
|
16 (fn r => <xml><li><a link={see r.T.Id}>{[r.T.Desc]} ({[r.Len]})</a></li></xml>);
|
adamc@742
|
17 return <xml><body>
|
adamc@742
|
18 {ls}
|
adamc@742
|
19
|
adamc@742
|
20 <br/>
|
adamc@742
|
21
|
adamc@742
|
22 <form>
|
adamc@742
|
23 <textbox{#Desc}/>
|
adamc@742
|
24 <upload{#Data}/>
|
adamc@742
|
25 <submit action={save}/>
|
adamc@742
|
26 </form>
|
adamc@742
|
27 </body></xml>
|