From 4bc363c5ec2724b9d310e17181ca87517c98aa68 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 10 Mar 2009 16:38:38 -0400 Subject: BatchG demo --- demo/prose | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'demo/prose') diff --git a/demo/prose b/demo/prose index dd764ae4..57722a81 100644 --- a/demo/prose +++ b/demo/prose @@ -213,3 +213,20 @@ increment.urp batch.urp

This example shows more of what is possible with mixed client/server code. The application is an editor for a simple database table, where additions of new rows can be batched in the client, before a button is clicked to trigger a mass addition.

+ +batchG.urp + +

We can redo the last example with a generic component, like we did in the Crud examples. The module BatchFun is analogous to the Crud module. It contains a functor that builds a batching editor, when given a suitable description of a table.

+ +

The signature of the functor is the same as for Crud. We change the definition of colMeta to reflect the different kinds of column metadata that we need. Each column is still described by a pair of types, and the first element of each pair still gives the SQL type for a column. Now, however, the second type in a pair gives a type of local state to be used in a reactive widget for inputing that column.

+ +

The first three fields of a colMeta record are the same as for Crud. The rest of the fields are:

+
    +
  1. NewState, which allocates some new widget local state
    2. +
  2. Widget, which produces a reactive widget from some state
    3. +
  3. ReadState, which reads the current value of some state to determine which SQL value it encodes
    4. +
+ +

BatchFun.Make handles the plumbing of allocating the local state, using it to create widgets, and reading the state values when the user clicks "Batch it."

+ +

batchG.ur contains an example instantiation, which is just as easy to write as in the Crud1 example.

-- cgit v1.2.3