annotate html.ur @ 18:6cd839818393

Adjust to name change for [Top.id]
author Adam Chlipala <adam@chlipala.net>
date Thu, 29 Dec 2011 14:15:02 -0500
parents 1a915f89f23a
children 693ab4dd1e9e
rev   line source
adam@9 1 open Parse
adam@9 2
adam@9 3 con attribute = fn t => {Nam : string,
adam@9 4 Parse : string -> option t}
adam@9 5
adam@9 6 con tag = fn ts => {Nam : string,
adam@9 7 Attributes : $(map attribute ts),
adam@9 8 Folder : folder ts,
adam@9 9 Construct : ctx ::: {Unit} -> [[Body] ~ ctx] => $ts
adam@9 10 -> xml ([Body] ++ ctx) [] [] -> xml ([Body] ++ ctx) [] []}
adam@9 11
adam@9 12 fun tag [use] [ignore] [use ~ ignore] (fl : folder use) (name : string) (attrs : $(map attribute use))
adam@9 13 (construct : ctx ::: {Unit} -> [[Body] ~ ctx] => Basis.tag (use ++ ignore) ([Body] ++ ctx) ([Body] ++ ctx) [] []) =
adam@9 14 {Nam = name,
adam@9 15 Attributes = attrs,
adam@9 16 Folder = fl,
adam@9 17 Construct = fn [ctx] [[Body] ~ ctx] (ats : $use) (inner : xml ([Body] ++ ctx) [] []) =>
adam@17 18 Basis.tag None None ats construct inner}
adam@9 19
adam@9 20 fun simpleTag [ignore] name (bt : bodyTag ignore) : tag [] =
adam@9 21 @@tag [[]] [ignore] ! _ name {} (fn [ctx] [[Body] ~ ctx] => bt ())
adam@9 22
adam@9 23 fun simpleTag' [use] [ignore] [use ~ ignore] (fl : folder use)
adam@9 24 name (bt : bodyTag (use ++ ignore)) (ats : $(map attribute use)) : tag use =
adam@9 25 @@tag [use] [ignore] ! fl name ats (fn [ctx] [[Body] ~ ctx] => bt ())
adam@9 26
adam@9 27 fun url name = {Nam = name,
adam@9 28 Parse = checkUrl}
adam@9 29
adam@9 30 datatype error a =
adam@9 31 Good of a
adam@9 32 | Bad of string
adam@9 33
adam@9 34 fun format [tags] (fl : folder tags) (tags : $(map tag tags)) [ctx] [[Body] ~ ctx] s =
adam@9 35 let
adam@9 36 fun loop s : error (xml ([Body] ++ ctx) [] [] * string) =
adam@9 37 case String.msplit {Haystack = s, Needle = "&<"} of
adam@9 38 None => Good (cdata s, "")
adam@9 39 | Some (pre, ch, post) =>
adam@9 40 case ch of
adam@9 41 #"&" =>
adam@9 42 (case String.split post #";" of
adam@9 43 None => Bad "No ';' after '&'"
adam@9 44 | Some (code, post) =>
adam@9 45 let
adam@9 46 val xml =
adam@9 47 case code of
adam@9 48 "lt" => <xml>&lt;</xml>
adam@9 49 | "gt" => <xml>&gt;</xml>
adam@9 50 | "amp" => <xml>&amp;</xml>
adam@9 51 | _ => <xml/>
adam@9 52 in
adam@9 53 case loop post of
adam@9 54 Good (after, post) => Good (<xml>{[pre]}{xml}{after}</xml>, post)
adam@9 55 | x => x
adam@9 56 end)
adam@9 57 | _ =>
adam@9 58 if String.length post > 0 && String.sub post 0 = #"/" then
adam@9 59 case String.split post #"\x3E" of
adam@9 60 None => Bad "No '>' after '</'"
adam@9 61 | Some (_, post) => Good (<xml>{[pre]}</xml>, post)
adam@9 62 else
adam@9 63 case String.msplit {Haystack = post, Needle = " >"} of
adam@9 64 None => Bad "No '>' after '<'"
adam@9 65 | Some (tname, ch, post) =>
adam@9 66 @foldR [tag] [fn _ => unit -> error (xml ([Body] ++ ctx) [] [] * string)]
adam@9 67 (fn [nm :: Name] [ts :: {Type}] [r :: {{Type}}] [[nm] ~ r] (meta : tag ts) acc () =>
adam@9 68 if meta.Nam = tname then
adam@9 69 let
adam@9 70 fun doAttrs (ch, post, ats : $(map option ts)) =
adam@9 71 if String.length post > 0 && Char.isSpace (String.sub post 0) then
adam@9 72 doAttrs (ch, String.substring post {Start = 1,
adam@9 73 Len = String.length post - 1},
adam@9 74 ats)
adam@9 75 else
adam@9 76 case ch of
adam@9 77 #"\x3E" => Good (ats, post)
adam@9 78 | _ =>
adam@9 79 case String.split post #"=" of
adam@9 80 None =>
adam@9 81 (case String.split post #"\x3E" of
adam@9 82 None => Bad "No tag ender '\x3E'"
adam@9 83 | Some (_, post) => Good (ats, post))
adam@9 84 | Some (aname, post) =>
adam@9 85 if String.length post >= 1 && String.sub post 0 = #"\"" then
adam@9 86 case String.split (String.substring post
adam@9 87 {Start = 1,
adam@9 88 Len = String.length post
adam@9 89 - 1})
adam@9 90 #"\"" of
adam@9 91 None => Bad "No '\"' to end attribute value"
adam@9 92 | Some (aval, post) =>
adam@9 93 let
adam@9 94 val ats =
adam@9 95 @map2 [attribute] [option] [option]
adam@9 96 (fn [t] meta v =>
adam@9 97 if aname = meta.Nam then
adam@9 98 meta.Parse aval
adam@9 99 else
adam@9 100 v)
adam@9 101 meta.Folder meta.Attributes ats
adam@9 102 in
adam@9 103 doAttrs (#" ", post, ats)
adam@9 104 end
adam@9 105 else
adam@9 106 Bad "Attribute value doesn't begin with quote"
adam@9 107 in
adam@9 108 case doAttrs (ch, post, @map0 [option] (fn [t :: Type] => None)
adam@9 109 meta.Folder) of
adam@9 110 Good (ats, post) =>
adam@9 111 let
adam@9 112 val ats =
adam@18 113 @map2 [attribute] [option] [ident]
adam@9 114 (fn [t] meta v =>
adam@9 115 case v of
adam@9 116 None => error <xml>Missing attribute {[meta.Nam]}
adam@9 117 for {[tname]}</xml>
adam@9 118 | Some v => v)
adam@9 119 meta.Folder meta.Attributes ats
adam@9 120 in
adam@9 121 case loop post of
adam@9 122 Good (inner, post) =>
adam@9 123 (case loop post of
adam@9 124 Good (after, post) =>
adam@9 125 Good (<xml>{[pre]}{meta.Construct [ctx] !
adam@9 126 ats inner}{after}</xml>, post)
adam@9 127 | x => x)
adam@9 128 | x => x
adam@9 129 end
adam@9 130 | Bad s => Bad s
adam@9 131 end
adam@9 132 else
adam@9 133 acc ())
adam@9 134 (fn () => Bad ("Unknown HTML tag " ^ tname)) fl tags ()
adam@9 135 in
adam@9 136 case loop s of
adam@9 137 Bad msg => Failure msg
adam@9 138 | Good (xml, _) => Success xml
adam@9 139 end
adam@9 140
adam@9 141 val b = simpleTag "b" @@b
adam@9 142 val i = simpleTag "i" @@i
adam@9 143 val a = simpleTag' "a" @@a {Href = url "href"}
adam@9 144