Ur/Web: demo/more/bulkEdit.urs annotate

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	c6e948ec79e9
children

rev	line source
adamc@1004	1 functor Make(M : sig
adamc@1004	2 con keyName :: Name
adamc@1004	3 con keyType :: Type
adamc@1004	4 val showKey : show keyType
adamc@1005	5 val readKey : read keyType
adamc@1005	6 val injKey : sql_injectable keyType
adamc@1004	7
adamc@1004	8 con visible :: {(Type * Type)}
adamc@1004	9 constraint [keyName] ~ visible
adamc@1004	10 val folder : folder visible
adamc@1004	11 val visible : $(map Meta.meta visible)
adamc@1004	12
adamc@1004	13 con invisible :: {Type}
adamc@1004	14 constraint [keyName] ~ invisible
adamc@1004	15 constraint visible ~ invisible
adamc@1004	16
adamc@1004	17 val title : string
adamc@1004	18 val isAllowed : transaction bool
adamc@1004	19 table t : ([keyName = keyType] ++ map fst visible ++ invisible)
adamc@1004	20 end) : sig
adamc@1004	21
adamc@1004	22 val main : unit -> transaction page
adamc@1004	23
adamc@1004	24 end

Mercurial > urweb