changeset 93:94afff1ff7f6

More fun with HTML
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jul 2008 17:14:35 -0400
parents 1a4c51fa615c
children 40d146f467c5
files lib/basis.lig src/elaborate.sml src/lacweb.grm tests/html.lac
diffstat 4 files changed, 21 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/lib/basis.lig	Thu Jul 03 17:02:42 2008 -0400
+++ b/lib/basis.lig	Thu Jul 03 17:14:35 2008 -0400
@@ -20,3 +20,8 @@
 
 val head : tag [Html] [Head]
 val title : tag [Head] []
+
+val body : tag [Html] [Body]
+val p : tag [Body] [Body]
+val b : tag [Body] [Body]
+val i : tag [Body] [Body]
--- a/src/elaborate.sml	Thu Jul 03 17:02:42 2008 -0400
+++ b/src/elaborate.sml	Thu Jul 03 17:14:35 2008 -0400
@@ -1810,6 +1810,11 @@
 
       | L.DStr (x, sgno, str) =>
         let
+            val () = if x = "Basis" then
+                         raise Fail "Not allowed to redefine structure 'Basis'"
+                     else
+                         ()
+
             val formal = Option.map (elabSgn (env, denv)) sgno
 
             val (str', sgn', gs') =
--- a/src/lacweb.grm	Thu Jul 03 17:02:42 2008 -0400
+++ b/src/lacweb.grm	Thu Jul 03 17:14:35 2008 -0400
@@ -259,7 +259,12 @@
        | FN SYMBOL kcolon kind DARROW eexp (ECAbs (kcolon, SYMBOL, kind, eexp), s (FNleft, eexpright))
        | FN SYMBOL COLON cexp DARROW eexp (EAbs (SYMBOL, SOME cexp, eexp), s (FNleft, eexpright))
        | FN SYMBOL DARROW eexp          (EAbs (SYMBOL, NONE, eexp), s (FNleft, eexpright))
-       | FN cterm TWIDDLE cterm DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (cterm1left, eexpright))
+       | LBRACK cterm TWIDDLE cterm RBRACK DARROW eexp(EDisjoint (cterm1, cterm2, eexp), s (LBRACKleft, RBRACKright))
+       | FN UNIT DARROW eexp            (let
+                                             val loc = s (FNleft, eexpright)
+                                         in
+                                             (EAbs ("_", SOME (TRecord (CRecord [], loc), loc), eexp), loc)
+                                         end)
 
        | LPAREN eexp RPAREN DCOLON cexp (EAnnot (eexp, cexp), s (LPARENleft, cexpright))
        | eterm DOT ident                (EField (eterm, ident), s (etermleft, identright))
--- a/tests/html.lac	Thu Jul 03 17:02:42 2008 -0400
+++ b/tests/html.lac	Thu Jul 03 17:14:35 2008 -0400
@@ -1,5 +1,9 @@
-val text : xml[Html] = <html>
+val main = fn () => <html>
         <head>
                 <title>Hello World!</title>
         </head>
+
+        <body>
+                <b>Hello</b> <i>World</i>!
+        </body>
 </html>