Mercurial > urweb

annotate demo/more/grid.urs @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 bb3fc575cfe7
children be0c4e2e488a
rev   line source
adamc@944 1 con colMeta' = fn (row :: Type) (input :: Type) (filter :: Type) =>
adamc@915 2 {Header : string,
adamc@944 3 Project : row -> transaction input,
adamc@944 4 Update : row -> input -> transaction row,
adamc@944 5 Display : input -> xbody,
adamc@944 6 Edit : input -> xbody,
adamc@944 7 Validate : input -> signal bool,
adamc@944 8 CreateFilter : transaction filter,
adamc@944 9 DisplayFilter : filter -> xbody,
adamc@961 10 Filter : filter -> row -> signal bool,
adamc@961 11 Sort : option (row -> row -> bool)}
adamc@915 12
adamc@1002 13 con colMeta = fn (row :: Type) (global :: Type, input :: Type, filter :: Type) =>
adamc@1002 14 {Initialize : transaction global,
adamc@1002 15 Handlers : global -> colMeta' row input filter}
adamc@915 16
adamc@935 17 con aggregateMeta = fn (row :: Type) (acc :: Type) =>
adamc@935 18 {Initial : acc,
adamc@935 19 Step : row -> acc -> acc,
adamc@935 20 Display : acc -> xbody}
adamc@935 21
adamc@915 22 functor Make(M : sig
adamc@915 23 type row
adamc@936 24 type key
adamc@936 25 val keyOf : row -> key
adamc@936 26
adamc@915 27 val list : transaction (list row)
adamc@915 28 val new : transaction row
adamc@936 29 val save : key -> row -> transaction unit
adamc@936 30 val delete : key -> transaction unit
adamc@915 31
adamc@944 32 con cols :: {(Type * Type * Type)}
adamc@915 33 val cols : $(map (colMeta row) cols)
adamc@915 34
adamc@915 35 val folder : folder cols
adamc@935 36
adamc@935 37 con aggregates :: {Type}
adamc@935 38 val aggregates : $(map (aggregateMeta row) aggregates)
adamc@937 39 val aggFolder : folder aggregates
adamc@964 40
adamc@964 41 val pageLength : option int
adamc@915 42 end) : sig
adamc@915 43 type grid
adamc@915 44
adamc@915 45 val grid : transaction grid
adamc@915 46 val sync : grid -> transaction unit
adamc@915 47 val render : grid -> xbody
adamc@940 48
adamc@940 49 val showSelection : grid -> source bool
adamc@940 50 val selection : grid -> signal (list M.row)
adamc@940 51
adamc@915 52 style tabl
adamc@915 53 style tr
adamc@915 54 style th
adamc@915 55 style td
adamc@943 56 style agg
adamc@915 57 end