Basic XML stuff

3 files changed, 420 insertions, 177 deletions

diff --git a/src/elaborate.sml b/src/elaborate.sml
index 7a8c06a8..6a824394 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -906,205 +906,316 @@ fun elabHead (env, denv) (e as (_, loc)) t =
     end
 
 fun elabExp (env, denv) (e, loc) =
-    case e of
-        L.EAnnot (e, t) =>
-        let
-            val (e', et, gs1) = elabExp (env, denv) e
-            val (t', _, gs2) = elabCon (env, denv) t
-            val gs3 = checkCon (env, denv) e' et t'
-        in
-            (e', t', gs1 @ gs2 @ gs3)
-        end
+    let
+        fun doApp (e1, e2) =
+            let
+                val (e1', t1, gs1) = elabExp (env, denv) e1
+                val (e1', t1, gs2) = elabHead (env, denv) e1' t1
+                val (e2', t2, gs3) = elabExp (env, denv) e2
 
-      | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
-      | L.EVar ([], s) =>
-        (case E.lookupE env s of
-             E.NotBound =>
-             (expError env (UnboundExp (loc, s));
-              (eerror, cerror, []))
-           | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
-           | E.Named (n, t) => ((L'.ENamed n, loc), t, []))
-      | L.EVar (m1 :: ms, s) =>
-        (case E.lookupStr env m1 of
-             NONE => (expError env (UnboundStrInExp (loc, m1));
-                      (eerror, cerror, []))
-           | SOME (n, sgn) =>
-             let
-                 val (str, sgn) = foldl (fn (m, (str, sgn)) =>
-                                     case E.projectStr env {sgn = sgn, str = str, field = m} of
-                                         NONE => (conError env (UnboundStrInCon (loc, m));
-                                                  (strerror, sgnerror))
-                                       | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
-                                  ((L'.StrVar n, loc), sgn) ms
+                val dom = cunif (loc, ktype)
+                val ran = cunif (loc, ktype)
+                val t = (L'.TFun (dom, ran), dummy)
 
-                 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
-                             NONE => (expError env (UnboundExp (loc, s));
-                                      cerror)
-                           | SOME t => t
-             in
-                 ((L'.EModProj (n, ms, s), loc), t, [])
-             end)
+                val gs4 = checkCon (env, denv) e1' t1 t
+                val gs5 = checkCon (env, denv) e2' t2 dom
+            in
+                ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
+            end
+    in
+        case e of
+            L.EAnnot (e, t) =>
+            let
+                val (e', et, gs1) = elabExp (env, denv) e
+                val (t', _, gs2) = elabCon (env, denv) t
+                val gs3 = checkCon (env, denv) e' et t'
+            in
+                (e', t', gs1 @ gs2 @ gs3)
+            end
 
-      | L.EApp (e1, e2) =>
-        let
-            val (e1', t1, gs1) = elabExp (env, denv) e1
-            val (e1', t1, gs2) = elabHead (env, denv) e1' t1
-            val (e2', t2, gs3) = elabExp (env, denv) e2
+          | L.EPrim p => ((L'.EPrim p, loc), primType env p, [])
+          | L.EVar ([], s) =>
+            (case E.lookupE env s of
+                 E.NotBound =>
+                 (expError env (UnboundExp (loc, s));
+                  (eerror, cerror, []))
+               | E.Rel (n, t) => ((L'.ERel n, loc), t, [])
+               | E.Named (n, t) => ((L'.ENamed n, loc), t, []))
+          | L.EVar (m1 :: ms, s) =>
+            (case E.lookupStr env m1 of
+                 NONE => (expError env (UnboundStrInExp (loc, m1));
+                          (eerror, cerror, []))
+               | SOME (n, sgn) =>
+                 let
+                     val (str, sgn) = foldl (fn (m, (str, sgn)) =>
+                                                case E.projectStr env {sgn = sgn, str = str, field = m} of
+                                                    NONE => (conError env (UnboundStrInCon (loc, m));
+                                                             (strerror, sgnerror))
+                                                  | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
+                                            ((L'.StrVar n, loc), sgn) ms
+
+                     val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
+                                 NONE => (expError env (UnboundExp (loc, s));
+                                          cerror)
+                               | SOME t => t
+                 in
+                     ((L'.EModProj (n, ms, s), loc), t, [])
+                 end)
+
+          | L.EApp (arg as ((L.EApp ((L.ECApp ((L.EVar (["Basis"], "join"), _), (L.CWild _, _)), _), xml1), _), xml2)) =>
+            let
+                val (xml1', t1, gs1) = elabExp (env, denv) xml1
+                val (xml2', t2, gs2) = elabExp (env, denv) xml2
 
-            val dom = cunif (loc, ktype)
-            val ran = cunif (loc, ktype)
-            val t = (L'.TFun (dom, ran), dummy)
+                val kunit = (L'.KUnit, loc)
+                val k = (L'.KRecord kunit, loc)
 
-            val gs4 = checkCon (env, denv) e1' t1 t
-            val gs5 = checkCon (env, denv) e2' t2 dom
-        in
-            ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
-        end
-      | L.EAbs (x, to, e) =>
-        let
-            val (t', gs1) = case to of
-                                NONE => (cunif (loc, ktype), [])
-                              | SOME t =>
-                                let
-                                    val (t', tk, gs) = elabCon (env, denv) t
-                                in
-                                    checkKind env t' tk ktype;
-                                    (t', gs)
-                                end
-            val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
-        in
-            ((L'.EAbs (x, t', et, e'), loc),
-             (L'.TFun (t', et), loc),
-             gs1 @ gs2)
-        end
-      | L.ECApp (e, c) =>
-        let
-            val (e', et, gs1) = elabExp (env, denv) e
-            val (e', et, gs2) = elabHead (env, denv) e' et
-            val (c', ck, gs3) = elabCon (env, denv) c
-            val ((et', _), gs4) = hnormCon (env, denv) et
-        in
-            case et' of
-                L'.CError => (eerror, cerror, [])
-              | L'.TCFun (_, _, k, eb) =>
-                let
-                    val () = checkKind env c' ck k
-                    val eb' = subConInCon (0, c') eb
-                              handle SynUnif => (expError env (Unif ("substitution", eb));
-                                                 cerror)
-                in
-                    ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
-                end
+                val basis =
+                    case E.lookupStr env "Basis" of
+                        NONE => raise Fail "elabExp: Unbound Basis"
+                      | SOME (n, _) => n
 
-              | L'.CUnif _ =>
-                (expError env (Unif ("application", et));
-                 (eerror, cerror, []))
+                fun xml () =
+                    let
+                        val ns = cunif (loc, k)
+                    in
+                        (ns, (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), ns), loc))
+                    end
 
-              | _ =>
-                (expError env (WrongForm ("constructor function", e', et));
-                 (eerror, cerror, []))
-        end
-      | L.ECAbs (expl, x, k, e) =>
-        let
-            val expl' = elabExplicitness expl
-            val k' = elabKind k
-            val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
-        in
-            ((L'.ECAbs (expl', x, k', e'), loc),
-             (L'.TCFun (expl', x, k', et), loc),
-             gs)
-        end
+                val (ns1, c1) = xml ()
+                val (ns2, c2) = xml ()
 
-      | L.EDisjoint (c1, c2, e) =>
-        let
-            val (c1', k1, gs1) = elabCon (env, denv) c1
-            val (c2', k2, gs2) = elabCon (env, denv) c2
+                val gs3 = checkCon (env, denv) xml1' t1 c1
+                val gs4 = checkCon (env, denv) xml2' t2 c2
 
-            val ku1 = kunif loc
-            val ku2 = kunif loc
+                val (ns1, gs5) = hnormCon (env, denv) ns1
+                val (ns2, gs6) = hnormCon (env, denv) ns2
 
-            val (denv', gs3) = D.assert env denv (c1', c2')
-            val (e', t, gs4) = elabExp (env, denv') e
-        in
-            checkKind env c1' k1 (L'.KRecord ku1, loc);
-            checkKind env c2' k2 (L'.KRecord ku2, loc);
+                val cemp = (L'.CRecord (kunit, []), loc)
 
-            (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
-        end
+                val (shared, ctx1, ctx2) =
+                    case (#1 ns1, #1 ns2) of
+                        (L'.CRecord (_, ns1), L'.CRecord (_, ns2)) =>
+                        let
+                            val ns = List.filter (fn ((nm, _), _) =>
+                                                     case nm of
+                                                         L'.CName s =>
+                                                         List.exists (fn ((L'.CName s', _), _) => s' = s
+                                                                       | _ => false) ns2
+                                                       | _ => false) ns1
+                        in
+                            ((L'.CRecord (kunit, ns), loc), cunif (loc, k), cunif (loc, k))
+                        end
+                      | (_, L'.CRecord _) => (ns2, cemp, cemp)
+                      | _ => (ns1, cemp, cemp)
 
-      | L.ERecord xes =>
-        let
-            val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
-                                                   let
-                                                       val (x', xk, gs1) = elabCon (env, denv) x
-                                                       val (e', et, gs2) = elabExp (env, denv) e
-                                                   in
-                                                       checkKind env x' xk kname;
-                                                       ((x', e', et), gs1 @ gs2 @ gs)
-                                                   end)
-                                               [] xes
+                val ns1' = (L'.CConcat (shared, ctx1), loc)
+                val ns2' = (L'.CConcat (shared, ctx2), loc)
 
-            val k = (L'.KType, loc)
+                val e = (L'.EModProj (basis, [], "join"), loc)
+                val e = (L'.ECApp (e, shared), loc)
+                val e = (L'.ECApp (e, ctx1), loc)
+                val e = (L'.ECApp (e, ctx2), loc)
+                val e = (L'.EApp (e, xml1'), loc)
+                val e = (L'.EApp (e, xml2'), loc)
 
-            fun prove (xets, gs) =
-                case xets of
-                    [] => gs
-                  | (x, _, t) :: rest =>
+                val t = (L'.CApp ((L'.CModProj (basis, [], "xml"), loc), shared), loc)
+
+                fun doUnify (ns, ns') =
                     let
-                        val xc = (x, t)
-                        val r1 = (L'.CRecord (k, [xc]), loc)
-                        val gs = foldl (fn ((x', _, t'), gs) =>
-                                           let
-                                               val xc' = (x', t')
-                                               val r2 = (L'.CRecord (k, [xc']), loc)
-                                           in
-                                               D.prove env denv (r1, r2, loc) @ gs
-                                           end)
-                                 gs rest
+                        fun setEmpty c =
+                            let
+                                val ((c, _), gs) = hnormCon (env, denv) c
+                            in
+                                case c of
+                                    L'.CUnif (_, _, _, r) =>
+                                    (r := SOME cemp;
+                                     gs)
+                                  | L'.CConcat (_, c') => setEmpty c' @ gs
+                                  | _ => gs
+                            end
+
+                        val gs1 = unifyCons (env, denv) ns ns'
+                        val gs2 = setEmpty ns'
+                        val gs3 = unifyCons (env, denv) ns ns'
                     in
-                        prove (rest, gs)
+                        gs1 @ gs2 @ gs3
                     end
-        in
-            ((L'.ERecord xes', loc),
-             (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
-             prove (xes', gs))
-        end
 
-      | L.EField (e, c) =>
-        let
-            val (e', et, gs1) = elabExp (env, denv) e
-            val (c', ck, gs2) = elabCon (env, denv) c
-
-            val ft = cunif (loc, ktype)
-            val rest = cunif (loc, ktype_record)
-            val first = (L'.CRecord (ktype, [(c', ft)]), loc)
-                       
-            val gs3 =
-                checkCon (env, denv) e' et
-                         (L'.TRecord (L'.CConcat (first, rest), loc), loc)
-            val gs4 = D.prove env denv (first, rest, loc)
-        in
-            ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
-        end
+                val gs7 = doUnify (ns1, ns1')
+                val gs8 = doUnify (ns2, ns2')
+            in
+                (e, t, (loc, env, denv, shared, ctx1)
+                       :: (loc, env, denv, shared, ctx2)
+                       :: gs1 @ gs2 @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 @ gs8)
+            end
 
-      | L.EFold =>
-        let
-            val dom = kunif loc
-        in
-            ((L'.EFold dom, loc), foldType (dom, loc), [])
-        end
+          | L.EApp (e1, e2) =>
+            let
+                val (e1', t1, gs1) = elabExp (env, denv) e1
+                val (e1', t1, gs2) = elabHead (env, denv) e1' t1
+                val (e2', t2, gs3) = elabExp (env, denv) e2
+
+                val dom = cunif (loc, ktype)
+                val ran = cunif (loc, ktype)
+                val t = (L'.TFun (dom, ran), dummy)
+
+                val gs4 = checkCon (env, denv) e1' t1 t
+                val gs5 = checkCon (env, denv) e2' t2 dom
+            in
+                ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2 @ gs3 @ gs4 @ gs5)
+            end
+          | L.EAbs (x, to, e) =>
+            let
+                val (t', gs1) = case to of
+                                    NONE => (cunif (loc, ktype), [])
+                                  | SOME t =>
+                                    let
+                                        val (t', tk, gs) = elabCon (env, denv) t
+                                    in
+                                        checkKind env t' tk ktype;
+                                        (t', gs)
+                                    end
+                val (e', et, gs2) = elabExp (E.pushERel env x t', denv) e
+            in
+                ((L'.EAbs (x, t', et, e'), loc),
+                 (L'.TFun (t', et), loc),
+                 gs1 @ gs2)
+            end
+          | L.ECApp (e, c) =>
+            let
+                val (e', et, gs1) = elabExp (env, denv) e
+                val (e', et, gs2) = elabHead (env, denv) e' et
+                val (c', ck, gs3) = elabCon (env, denv) c
+                val ((et', _), gs4) = hnormCon (env, denv) et
+            in
+                case et' of
+                    L'.CError => (eerror, cerror, [])
+                  | L'.TCFun (_, _, k, eb) =>
+                    let
+                        val () = checkKind env c' ck k
+                        val eb' = subConInCon (0, c') eb
+                            handle SynUnif => (expError env (Unif ("substitution", eb));
+                                               cerror)
+                    in
+                        ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ gs3 @ gs4)
+                    end
+
+                  | L'.CUnif _ =>
+                    (expError env (Unif ("application", et));
+                     (eerror, cerror, []))
+
+                  | _ =>
+                    (expError env (WrongForm ("constructor function", e', et));
+                     (eerror, cerror, []))
+            end
+          | L.ECAbs (expl, x, k, e) =>
+            let
+                val expl' = elabExplicitness expl
+                val k' = elabKind k
+                val (e', et, gs) = elabExp (E.pushCRel env x k', D.enter denv) e
+            in
+                ((L'.ECAbs (expl', x, k', e'), loc),
+                 (L'.TCFun (expl', x, k', et), loc),
+                 gs)
+            end
+
+          | L.EDisjoint (c1, c2, e) =>
+            let
+                val (c1', k1, gs1) = elabCon (env, denv) c1
+                val (c2', k2, gs2) = elabCon (env, denv) c2
+
+                val ku1 = kunif loc
+                val ku2 = kunif loc
+
+                val (denv', gs3) = D.assert env denv (c1', c2')
+                val (e', t, gs4) = elabExp (env, denv') e
+            in
+                checkKind env c1' k1 (L'.KRecord ku1, loc);
+                checkKind env c2' k2 (L'.KRecord ku2, loc);
+
+                (e', (L'.TDisjoint (c1', c2', t), loc), gs1 @ gs2 @ gs3 @ gs4)
+            end
+
+          | L.ERecord xes =>
+            let
+                val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
+                                                       let
+                                                           val (x', xk, gs1) = elabCon (env, denv) x
+                                                           val (e', et, gs2) = elabExp (env, denv) e
+                                                       in
+                                                           checkKind env x' xk kname;
+                                                           ((x', e', et), gs1 @ gs2 @ gs)
+                                                       end)
+                                                   [] xes
+
+                val k = (L'.KType, loc)
+
+                fun prove (xets, gs) =
+                    case xets of
+                        [] => gs
+                      | (x, _, t) :: rest =>
+                        let
+                            val xc = (x, t)
+                            val r1 = (L'.CRecord (k, [xc]), loc)
+                            val gs = foldl (fn ((x', _, t'), gs) =>
+                                               let
+                                                   val xc' = (x', t')
+                                                   val r2 = (L'.CRecord (k, [xc']), loc)
+                                               in
+                                                   D.prove env denv (r1, r2, loc) @ gs
+                                               end)
+                                           gs rest
+                        in
+                            prove (rest, gs)
+                        end
+            in
+                ((L'.ERecord xes', loc),
+                 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc),
+                 prove (xes', gs))
+            end
+
+          | L.EField (e, c) =>
+            let
+                val (e', et, gs1) = elabExp (env, denv) e
+                val (c', ck, gs2) = elabCon (env, denv) c
+
+                val ft = cunif (loc, ktype)
+                val rest = cunif (loc, ktype_record)
+                val first = (L'.CRecord (ktype, [(c', ft)]), loc)
+                            
+                val gs3 =
+                    checkCon (env, denv) e' et
+                             (L'.TRecord (L'.CConcat (first, rest), loc), loc)
+                val gs4 = D.prove env denv (first, rest, loc)
+            in
+                ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ gs2 @ gs3 @ gs4)
+            end
+
+          | L.EFold =>
+            let
+                val dom = kunif loc
+            in
+                ((L'.EFold dom, loc), foldType (dom, loc), [])
+            end
+    end
             
 
 datatype decl_error =
-         KunifsRemain of ErrorMsg.span
-       | CunifsRemain of ErrorMsg.span
+         KunifsRemain of L'.decl list
+       | CunifsRemain of L'.decl list
+
+fun lspan [] = ErrorMsg.dummySpan
+  | lspan ((_, loc) :: _) = loc
 
 fun declError env err =
     case err of
-        KunifsRemain loc =>
-        ErrorMsg.errorAt loc "Some kind unification variables are undetermined in declaration"
-      | CunifsRemain loc =>
-        ErrorMsg.errorAt loc "Some constructor unification variables are undetermined in declaration"
+        KunifsRemain ds =>
+        (ErrorMsg.errorAt (lspan ds) "Some kind unification variables are undetermined in declaration";
+         eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
+      | CunifsRemain ds =>
+        (ErrorMsg.errorAt (lspan ds) "Some constructor unification variables are undetermined in declaration";
+         eprefaces' [("Decl", p_list_sep PD.newline (p_decl env) ds)])
 
 datatype sgn_error =
          UnboundSgn of ErrorMsg.span * string
@@ -1964,14 +2075,14 @@ fun elabFile basis env file =
                     ()
                 else (
                     if List.exists kunifsInDecl ds then
-                        declError env (KunifsRemain (#2 d))
+                        declError env (KunifsRemain ds)
                     else
                         ();
                     
                     case ListUtil.search cunifsInDecl ds of
                         NONE => ()
                       | SOME loc =>
-                        declError env (CunifsRemain loc)
+                        declError env (CunifsRemain ds)
                     );
 
                 (ds, (env, gs))
diff --git a/src/lacweb.grm b/src/lacweb.grm
index 95e13c50..115c528a 100644
--- a/src/lacweb.grm
+++ b/src/lacweb.grm
@@ -40,6 +40,7 @@ val s = ErrorMsg.spanOf
  | SYMBOL of string | CSYMBOL of string
  | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE
  | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER
+ | DIVIDE | GT
  | CON | LTYPE | VAL | FOLD | UNIT | KUNIT
  | TYPE | NAME
  | ARROW | LARROW | DARROW
@@ -47,6 +48,10 @@ val s = ErrorMsg.spanOf
  | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN
  | INCLUDE | OPEN | CONSTRAINT | CONSTRAINTS
 
+ | XML_BEGIN of string | XML_END
+ | NOTAGS of string 
+ | BEGIN_TAG of string | END_TAG of string
+
 %nonterm
    file of decl list
  | decls of decl list
@@ -78,6 +83,8 @@ val s = ErrorMsg.spanOf
  | eapps of exp
  | eterm of exp
  | rexp of (con * exp) list
+ | xml of exp
+ | xmlOne of exp
 
 %verbose                                (* print summary of errors *)
 %pos int                                (* positions *)
@@ -268,6 +275,32 @@ eterm  : LPAREN eexp RPAREN             (#1 eexp, s (LPARENleft, RPARENright))
 
        | FOLD                           (EFold, s (FOLDleft, FOLDright))
 
+       | XML_BEGIN xml XML_END          (xml)
+       | XML_BEGIN XML_END              (EApp ((EVar (["Basis"], "cdata"), s (XML_BEGINleft, XML_ENDright)),
+                                               (EPrim (Prim.String ""), s (XML_BEGINleft, XML_ENDright))),
+                                         s (XML_BEGINleft, XML_ENDright))
+
 rexp   :                                ([])
        | ident EQ eexp                  ([(ident, eexp)])
        | ident EQ eexp COMMA rexp       ((ident, eexp) :: rexp)
+
+xml    : xmlOne xml                  (let
+                                          val pos = s (xmlOneleft, xmlright)
+                                      in
+                                          (EApp ((EApp (
+                                                  (ECApp ((EVar (["Basis"], "join"), pos),
+                                                          (CWild (KRecord (KUnit, pos), pos), pos)), pos),
+                                                  xmlOne), pos),
+                                                  xml), pos)
+                                      end)
+       | xmlOne                      (xmlOne)
+
+xmlOne : NOTAGS                      (EApp ((EVar (["Basis"], "cdata"), s (NOTAGSleft, NOTAGSright)),
+                                            (EPrim (Prim.String NOTAGS), s (NOTAGSleft, NOTAGSright))),
+                                      s (NOTAGSleft, NOTAGSright))
+       | BEGIN_TAG DIVIDE GT         (EApp ((EApp ((EVar (["Basis"], "tag"), s (BEGIN_TAGleft, GTright)),
+                                                   (EVar ([], BEGIN_TAG), s (BEGIN_TAGleft, GTright))),
+                                             s (BEGIN_TAGleft, GTright)),
+                                            (EApp ((EVar (["Basis"], "cdata"), s (BEGIN_TAGleft, GTright)),
+                                                   (EPrim (Prim.String ""), s (BEGIN_TAGleft, GTright))),
+                                             s (BEGIN_TAGleft, GTright))), s (BEGIN_TAGleft, GTright))
diff --git a/src/lacweb.lex b/src/lacweb.lex
index 8b4a1789..3fc6577c 100644
--- a/src/lacweb.lex
+++ b/src/lacweb.lex
@@ -80,17 +80,42 @@ fun newline yypos =
 
 end
 
+val xmlTag = ref ([] : string list)
+val xmlString = ref true
+val braceLevels = ref ([] : ((unit -> unit) * int) list)
+
+fun pushLevel s = braceLevels := (s, 1) :: (!braceLevels)
+
+fun enterBrace () =
+    case !braceLevels of
+	(s, i) :: rest => braceLevels := (s, i+1) :: rest
+      | _ => ()
+
+fun exitBrace () =
+    case !braceLevels of
+	(s, i) :: rest =>
+	if i = 1 then
+	    (braceLevels := rest;
+	     s ())
+	else
+	    braceLevels := (s, i-1) :: rest
+      | _ => ()
+
+fun initialize () = (xmlTag := [];
+		     xmlString := false)
+
 
 %%
 %header (functor LacwebLexFn(structure Tokens : Lacweb_TOKENS));
 %full
-%s COMMENT STRING;
+%s COMMENT STRING XML XMLTAG;
 
 id = [a-z_][A-Za-z0-9_']*;
 cid = [A-Z][A-Za-z0-9_']*;
 ws = [\ \t\012];
 intconst = [0-9]+;
 realconst = [0-9]+\.[0-9]*;
+notags = [^<{\n]+;
 
 %%
 
@@ -98,6 +123,10 @@ realconst = [0-9]+\.[0-9]*;
                           continue ());
 <COMMENT> \n          => (newline yypos;
                           continue ());
+<XMLTAG> \n           => (newline yypos;
+                          continue ());
+<XML> \n              => (newline yypos;
+                          Tokens.NOTAGS (yytext, yypos, yypos + size yytext));
 
 <INITIAL> {ws}+       => (lex ());
 
@@ -120,6 +149,76 @@ realconst = [0-9]+\.[0-9]*;
 			  str := #"\n" :: !str; continue());
 <STRING> .            => (str := String.sub (yytext, 0) :: !str; continue());
 
+<INITIAL> "<" {id} ">"=> (let
+			      val tag = String.substring (yytext, 1, size yytext - 2)
+			  in
+			      YYBEGIN XML;
+			      xmlTag := tag :: (!xmlTag);
+			      Tokens.XML_BEGIN (tag, yypos, yypos + size yytext)
+			  end);
+<XML> "</" {id} ">"   => (let
+			      val id = String.substring (yytext, 2, size yytext - 3)
+			  in
+			      case !xmlTag of
+			          id' :: rest =>
+			          if id = id' then
+				      (YYBEGIN INITIAL;
+				       xmlTag := rest;
+				       Tokens.XML_END (yypos, yypos + size yytext))
+			          else
+				      Tokens.END_TAG (id, yypos, yypos + size yytext)
+			        | _ => 
+			          Tokens.END_TAG (id, yypos, yypos + size yytext)
+			  end);
+
+<XML> "<" {id}        => (YYBEGIN XMLTAG;
+			  Tokens.BEGIN_TAG (String.extract (yytext, 1, NONE),
+					    yypos, yypos + size yytext));
+
+<XMLTAG> "/"          => (Tokens.DIVIDE (yypos, yypos + size yytext));
+<XMLTAG> ">"          => (YYBEGIN XML;
+			  Tokens.GT (yypos, yypos + size yytext));
+
+<XMLTAG> {ws}+        => (lex ());
+
+<XMLTAG> {id}         => (Tokens.SYMBOL (yytext, yypos, yypos + size yytext));
+<XMLTAG> "="          => (Tokens.EQ (yypos, yypos + size yytext));
+
+<XMLTAG> {intconst}   => (case Int64.fromString yytext of
+                            SOME x => Tokens.INT (x, yypos, yypos + size yytext)
+                          | NONE   => (ErrorMsg.errorAt' (yypos, yypos)
+                                       ("Expected int, received: " ^ yytext);
+                                       continue ()));
+<XMLTAG> {realconst}  => (case Real.fromString yytext of
+                            SOME x => Tokens.FLOAT (x, yypos, yypos + size yytext)
+                          | NONE   => (ErrorMsg.errorAt' (yypos, yypos)
+                                       ("Expected float, received: " ^ yytext);
+                                       continue ()));
+<XMLTAG> "\""         => (YYBEGIN STRING;
+			  xmlString := true;
+			  strStart := yypos; str := []; continue());
+
+<XMLTAG> "{"          => (YYBEGIN INITIAL;
+			  pushLevel (fn () => YYBEGIN XMLTAG);
+			  Tokens.LBRACE (yypos, yypos + 1));
+<XMLTAG> "("          => (YYBEGIN INITIAL;
+			  pushLevel (fn () => YYBEGIN XMLTAG);
+			  Tokens.LPAREN (yypos, yypos + 1));
+
+<XMLTAG> .            => (ErrorMsg.errorAt' (yypos, yypos)
+                          ("illegal XML tag character: \"" ^ yytext ^ "\"");
+                          continue ());
+
+<XML> "{"             => (YYBEGIN INITIAL;
+			  pushLevel (fn () => YYBEGIN XML);
+			  Tokens.LBRACE (yypos, yypos + 1));
+
+<XML> {notags}        => (Tokens.NOTAGS (yytext, yypos, yypos + size yytext));
+
+<XML> .               => (ErrorMsg.errorAt' (yypos, yypos)
+                          ("illegal XML character: \"" ^ yytext ^ "\"");
+                          continue ());
+
 <INITIAL> "()"        => (Tokens.UNIT (pos yypos, pos yypos + size yytext));
 <INITIAL> "("         => (Tokens.LPAREN (pos yypos, pos yypos + size yytext));
 <INITIAL> ")"         => (Tokens.RPAREN (pos yypos, pos yypos + size yytext));