diff lib/ur/basis.urs @ 758:8323c1beef2e

Subforms type-checks; lists urlified and unurlified
author Adam Chlipala <adamc@hcoop.net>
date Thu, 30 Apr 2009 11:48:56 -0400
parents fa2019a63ea4
children 21f6d2e65685
line wrap: on
line diff
--- a/lib/ur/basis.urs	Thu Apr 30 11:07:29 2009 -0400
+++ b/lib/ur/basis.urs	Thu Apr 30 11:48:56 2009 -0400
@@ -566,7 +566,18 @@
     nm :: Name -> [[nm] ~ use] =>
     xml form [] bind
     -> xml ([Form] ++ ctx) use [nm = $bind]
-       
+
+val subforms : ctx ::: {Unit} -> use ::: {Type} -> bind ::: {Type}
+              -> [[Form] ~ ctx] =>
+    nm :: Name -> [[nm] ~ use] =>
+    xml [Body, Subform] [Entry = $bind] []
+    -> xml ([Form] ++ ctx) use [nm = list ($bind)]
+
+val entry : ctx ::: {Unit} -> bind ::: {Type}
+              -> [[Subform] ~ ctx] =>
+    xml form [] bind
+    -> xml ([Subform] ++ ctx) [Entry = $bind] []
+
 con formTag = fn (ty :: Type) (inner :: {Unit}) (attrs :: {Type}) =>
                   ctx ::: {Unit}
                   -> [[Form] ~ ctx] =>