Mercurial > urweb
annotate demo/more/conferenceFields.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 | 5d9f47124c4c |
children |
rev | line source |
---|---|
adamc@1007 | 1 open Meta |
adamc@1007 | 2 |
adamc@1007 | 3 val title = string "Title" |
adamc@1007 | 4 val abstract = textarea "Abstract" |
adamc@1029 | 5 val commentsForAuthors = textarea "Comments for Authors" |
adamc@1011 | 6 |
adamc@1011 | 7 fun charIn s = |
adamc@1011 | 8 if String.length s = 0 then |
adamc@1011 | 9 error <xml>Impossible: Empty option value</xml> |
adamc@1011 | 10 else |
adamc@1011 | 11 String.sub s 0 |
adamc@1011 | 12 |
adamc@1011 | 13 con dropdown = (char, string) |
adamc@1011 | 14 fun dropdown name opts = {Nam = name, |
adamc@1011 | 15 Show = txt, |
adamc@1011 | 16 Widget = fn [nm :: Name] => <xml><select{nm}> |
adamc@1011 | 17 {List.mapX (fn x => <xml><option>{[x]}</option></xml>) opts} |
adamc@1011 | 18 </select></xml>, |
adamc@1011 | 19 WidgetPopulated = fn [nm :: Name] v => <xml><select{nm}> |
adamc@1011 | 20 {List.mapX (fn x => <xml><option selected={x = v}>{[x]}</option></xml>) opts} |
adamc@1011 | 21 </select></xml>, |
adamc@1011 | 22 Parse = charIn, |
adamc@1011 | 23 Inject = _} |
adamc@1011 | 24 |
adamc@1032 | 25 val dropdown_show = _ |