Mercurial > urweb

annotate demo/more/dbgrid.urs @ 917:321a2d6feb40

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dragList demo working, save for Gecko load delay and highlighting
author Adam Chlipala <adamc@hcoop.net>
date Tue, 08 Sep 2009 10:55:49 -0400
parents 5e8b6fa5b48f
children 51bc7681c47e
rev   line source
adamc@915 1 con rawMeta = fn t :: Type =>
adamc@915 2 {New : transaction t,
adamc@915 3 Inj : sql_injectable t}
adamc@915 4
adamc@915 5 con colMeta' = fn (row :: {Type}) (t :: Type) =>
adamc@915 6 {Header : string,
adamc@915 7 Project : $row -> transaction t,
adamc@915 8 Update : $row -> t -> transaction ($row),
adamc@915 9 Display : t -> xbody,
adamc@915 10 Edit : t -> xbody,
adamc@915 11 Validate : t -> signal bool}
adamc@915 12
adamc@915 13 con colMeta = fn (row :: {Type}) (global_t :: (Type * Type)) =>
adamc@915 14 {Initialize : transaction global_t.1,
adamc@915 15 Handlers : global_t.1 -> colMeta' row global_t.2}
adamc@915 16
adamc@915 17 structure Direct : sig
adamc@915 18 con meta = fn global_actual_input :: (Type * Type * Type) =>
adamc@915 19 {Initialize : transaction global_actual_input.1,
adamc@915 20 Handlers : global_actual_input.1
adamc@915 21 -> {Display : global_actual_input.3 -> xbody,
adamc@915 22 Edit : global_actual_input.3 -> xbody,
adamc@915 23 Initialize : global_actual_input.2 -> transaction global_actual_input.3,
adamc@915 24 Parse : global_actual_input.3 -> signal (option global_actual_input.2)}}
adamc@915 25
adamc@915 26 con editableState :: (Type * Type * Type) -> (Type * Type)
adamc@915 27 val editable : ts ::: (Type * Type * Type) -> rest ::: {Type}
adamc@915 28 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
adamc@915 29 -> colMeta ([nm = ts.2] ++ rest)
adamc@915 30 (editableState ts)
adamc@915 31
adamc@915 32 con readOnlyState :: (Type * Type * Type) -> (Type * Type)
adamc@915 33 val readOnly : ts ::: (Type * Type * Type) -> rest ::: {Type}
adamc@915 34 -> nm :: Name -> [[nm] ~ rest] => string -> meta ts
adamc@915 35 -> colMeta ([nm = ts.2] ++ rest)
adamc@915 36 (readOnlyState ts)
adamc@915 37
adamc@915 38 type intGlobal
adamc@915 39 type intInput
adamc@915 40 val int : meta (intGlobal, int, intInput)
adamc@915 41
adamc@915 42 type stringGlobal
adamc@915 43 type stringInput
adamc@915 44 val string : meta (stringGlobal, string, stringInput)
adamc@915 45
adamc@915 46 type boolGlobal
adamc@915 47 type boolInput
adamc@915 48 val bool : meta (boolGlobal, bool, boolInput)
adamc@915 49
adamc@915 50 functor Foreign (M : sig
adamc@915 51 con row :: {Type}
adamc@915 52 con t :: Type
adamc@915 53 val show_t : show t
adamc@915 54 val read_t : read t
adamc@915 55 val eq_t : eq t
adamc@915 56 val inj_t : sql_injectable t
adamc@915 57 con nm :: Name
adamc@915 58 constraint [nm] ~ row
adamc@915 59 table tab : ([nm = t] ++ row)
adamc@915 60 val render : $([nm = t] ++ row) -> string
adamc@915 61 end) : sig
adamc@915 62 con global :: Type
adamc@915 63 con input :: Type
adamc@915 64 val meta : meta (global, M.t, input)
adamc@915 65 end
adamc@915 66 end
adamc@915 67
adamc@915 68 con computedState :: (Type * Type)
adamc@915 69 val computed : row ::: {Type} -> t ::: Type -> show t
adamc@915 70 -> string -> ($row -> t) -> colMeta row computedState
adamc@915 71 val computedHtml : row ::: {Type} -> string -> ($row -> xbody) -> colMeta row computedState
adamc@915 72
adamc@915 73 functor Make(M : sig
adamc@915 74 con key :: {Type}
adamc@915 75 con row :: {Type}
adamc@915 76 constraint key ~ row
adamc@915 77 table tab : (key ++ row)
adamc@915 78
adamc@915 79 val raw : $(map rawMeta (key ++ row))
adamc@915 80
adamc@915 81 con cols :: {(Type * Type)}
adamc@915 82 val cols : $(map (colMeta (key ++ row)) cols)
adamc@915 83
adamc@915 84 val keyFolder : folder key
adamc@915 85 val rowFolder : folder row
adamc@915 86 val colsFolder : folder cols
adamc@915 87 end) : sig
adamc@915 88 type grid
adamc@915 89
adamc@915 90 val grid : transaction grid
adamc@915 91 val sync : grid -> transaction unit
adamc@915 92 val render : grid -> xbody
adamc@915 93 end