src/Tools/WWW_Find/xhtml.ML
changeset 56738 13b0fc4ece42
parent 56737 e4f363e16bdc
child 56739 0d56854096ba
equal deleted inserted replaced
56737:e4f363e16bdc 56738:13b0fc4ece42
     1 (*  Title:      Tools/WWW_Find/xhtml.ML
       
     2     Author:     Timothy Bourke, NICTA
       
     3 
       
     4 Rudimentary XHTML construction.
       
     5 *)
       
     6 
       
     7 signature XHTML =
       
     8 sig
       
     9   type attribute
       
    10   type common_atts = { id : string option,
       
    11                        class : string option };
       
    12   val noid : common_atts;
       
    13   val id : string -> common_atts;
       
    14   val class : string -> common_atts;
       
    15 
       
    16   type tag
       
    17 
       
    18   val doctype_xhtml1_0_strict: string;
       
    19 
       
    20   val att: string -> string -> attribute
       
    21   val bool_att: string * bool -> attribute list
       
    22 
       
    23   val tag: string -> attribute list -> tag list -> tag
       
    24   val tag': string -> common_atts -> tag list -> tag
       
    25   val text: string -> tag
       
    26   val raw_text: string -> tag
       
    27 
       
    28   val add_attributes: attribute list -> tag -> tag
       
    29   val append: tag -> tag list -> tag
       
    30 
       
    31   val show: tag -> string list
       
    32 
       
    33   val write: (string -> unit) -> tag -> unit
       
    34   val write_enclosed: (string -> unit) -> tag -> ((string -> unit) -> unit) -> unit
       
    35 
       
    36   val html: { lang : string } -> tag list -> tag
       
    37   val head: { title : string, stylesheet_href : string } -> tag list -> tag
       
    38   val body: common_atts -> tag list -> tag
       
    39   val divele: common_atts -> tag list -> tag
       
    40   val span: common_atts * string -> tag
       
    41   val span': common_atts -> tag list -> tag
       
    42 
       
    43   val pre: common_atts -> string -> tag
       
    44 
       
    45   val table: common_atts -> tag list -> tag
       
    46   val thead: common_atts -> tag list -> tag
       
    47   val tbody: common_atts -> tag list -> tag
       
    48   val tr: tag list -> tag
       
    49   val th: common_atts * string -> tag
       
    50   val th': common_atts -> tag list -> tag
       
    51   val td: common_atts * string -> tag
       
    52   val td': common_atts -> tag list -> tag
       
    53   val td'': common_atts * { colspan : int option, rowspan : int option }
       
    54            -> tag list -> tag
       
    55 
       
    56   val p: common_atts * string -> tag
       
    57   val p': common_atts * tag list -> tag
       
    58   val h: common_atts * int * string -> tag
       
    59   val strong: string -> tag
       
    60   val em: string -> tag
       
    61   val a: { href : string, text : string } -> tag
       
    62 
       
    63   val ul: common_atts * tag list -> tag
       
    64   val ol: common_atts * tag list -> tag
       
    65   val dl: common_atts * (string * tag) list -> tag
       
    66 
       
    67   val alternate_class: { class0 : string, class1 : string }
       
    68                       -> tag list -> tag list
       
    69 
       
    70   val form: common_atts * { method : string, action : string }
       
    71             -> tag list -> tag
       
    72 
       
    73   datatype input_type =
       
    74       TextInput of { value: string option, maxlength: int option }
       
    75     | Password of int option
       
    76     | Checkbox of { checked : bool, value : string option }
       
    77     | Radio of { checked : bool, value : string option }
       
    78     | Submit
       
    79     | Reset
       
    80     | Hidden
       
    81     | Image of { src : string, alt : string }
       
    82     | File of { accept : string }
       
    83     | Button;
       
    84 
       
    85   val input: common_atts * { name : string, itype : input_type } -> tag
       
    86   val select: common_atts * { name : string, value : string option }
       
    87               -> string list -> tag
       
    88   val label: common_atts * { for: string } * string -> tag
       
    89 
       
    90   val reset_button: common_atts -> tag
       
    91   val submit_button: common_atts -> tag
       
    92 
       
    93   datatype event =
       
    94     (* global *)
       
    95       OnClick
       
    96     | OnDblClick
       
    97     | OnMouseDown
       
    98     | OnMouseUp
       
    99     | OnMouseOver
       
   100     | OnMouseMove
       
   101     | OnMouseOut
       
   102     | OnKeyPress
       
   103     | OnKeyDown
       
   104     | OnKeyUp
       
   105       (* anchor/label/input/select/textarea/button/area *)
       
   106     | OnFocus
       
   107     | OnBlur
       
   108       (* form *)
       
   109     | OnSubmit
       
   110     | OnReset
       
   111       (* input/textarea *)
       
   112     | OnSelect
       
   113       (* input/select/textarea *)
       
   114     | OnChange
       
   115       (* body *)
       
   116     | OnLoad
       
   117     | OnUnload;
       
   118 
       
   119   val script: common_atts * { script_type: string, src: string } -> tag
       
   120   val add_script: event * string -> tag -> tag
       
   121 end;
       
   122 
       
   123 structure Xhtml : XHTML =
       
   124 struct
       
   125 
       
   126 type attribute = string * string;
       
   127 type common_atts = {
       
   128     id : string option,
       
   129     class : string option
       
   130   };
       
   131 val noid = { id = NONE, class = NONE };
       
   132 fun id s = { id = SOME s, class = NONE };
       
   133 fun class s = { id = NONE, class = SOME s };
       
   134 
       
   135 fun from_common { id = NONE,   class = NONE } = []
       
   136   | from_common { id = SOME i, class = NONE } = [("id", i)]
       
   137   | from_common { id = NONE,   class = SOME c } = [("class", c)]
       
   138   | from_common { id = SOME i, class = SOME c } = [("id", i), ("class", c)];
       
   139 
       
   140 val update_atts =
       
   141   AList.join (op = : string * string -> bool) (fn _ => snd);
       
   142 
       
   143 datatype tag = Tag of (string * attribute list * tag list)
       
   144              | Text of string
       
   145              | RawText of string;
       
   146 
       
   147 fun is_text (Tag _) = false
       
   148   | is_text (Text _) = true
       
   149   | is_text (RawText _) = true;
       
   150 
       
   151 fun is_tag (Tag _) = true
       
   152   | is_tag (Text _) = false
       
   153   | is_tag (RawText _) = false;
       
   154 
       
   155 val att = pair;
       
   156 
       
   157 fun bool_att (nm, true) = [(nm, nm)]
       
   158   | bool_att (nm, false) = [];
       
   159 
       
   160 fun tag name atts inner = Tag (name, atts, inner);
       
   161 fun tag' name common_atts inner = Tag (name, from_common common_atts, inner);
       
   162 fun text t = Text t;
       
   163 fun raw_text t = RawText t;
       
   164 
       
   165 fun add_attributes atts' (Tag (nm, atts, inner)) =
       
   166       Tag (nm, update_atts (atts, atts'), inner)
       
   167   | add_attributes _ t = t;
       
   168 
       
   169 fun append (Tag (nm, atts, inner)) inner' = Tag (nm, atts, inner @ inner')
       
   170   | append _ _ = raise Fail "cannot append to a text element";
       
   171 
       
   172 fun show_att (n, v) = implode [" ", n, "=\"", XML.text v, "\""];
       
   173 
       
   174 fun show_text (Text t) = XML.text t
       
   175   | show_text (RawText t) = t
       
   176   | show_text _ = raise Fail "Bad call to show_text.";
       
   177 
       
   178 fun show (Text t) = [XML.text t]
       
   179   | show (RawText t) = [t]
       
   180   | show (Tag (nm, atts, inner)) =
       
   181   (["<", nm] @ map show_att atts
       
   182    @
       
   183    (if length inner = 0
       
   184     then ["/>"]
       
   185     else flat (
       
   186       [[">"]]
       
   187       @
       
   188       map show inner
       
   189       @
       
   190       [["</", nm, ">"]]
       
   191   )));
       
   192 
       
   193 fun write pr =
       
   194   let
       
   195     fun f (Text t) = (pr o XML.text) t
       
   196       | f (RawText t) = pr t
       
   197       | f (Tag (nm, atts, inner)) = (
       
   198           pr "<";
       
   199           pr nm;
       
   200           app (pr o show_att) atts;
       
   201           if length inner = 0
       
   202           then pr "/>"
       
   203           else (
       
   204             pr ">";
       
   205             app f inner;
       
   206             pr ("</" ^ nm ^ ">")
       
   207           ))
       
   208   in f end;
       
   209 
       
   210 (* Print all opening tags down into the tree until a branch of degree > 1 is
       
   211    found, in which case print everything before the last tag, which is then
       
   212    opened. *)
       
   213 fun write_open pr =
       
   214   let
       
   215     fun f (Text t) = (pr o XML.text) t
       
   216       | f (RawText t) = pr t
       
   217       | f (Tag (nm, atts, [])) =
       
   218           (pr "<"; pr nm; app (pr o show_att) atts; pr ">")
       
   219       | f (Tag (nm, atts, xs)) =
       
   220            (pr "<"; pr nm; app (pr o show_att) atts; pr ">";
       
   221             (case take_suffix is_text xs of
       
   222                ([], _) => ()
       
   223              | (b, _) =>
       
   224                  let val (xs, x) = split_last b;
       
   225                  in app (write pr) xs; f x end));
       
   226   in f end;
       
   227 
       
   228 (* Print matching closing tags for write_open. *)
       
   229 fun write_close pr =
       
   230   let
       
   231     fun close nm = pr ("</" ^ nm ^ ">");
       
   232     val pr_text = app (pr o show_text);
       
   233 
       
   234     fun f (Text t) = ()
       
   235       | f (RawText t) = ()
       
   236       | f (Tag (nm, _, [])) = close nm
       
   237       | f (Tag (nm, _, xs)) =
       
   238            (case take_suffix is_text xs of
       
   239               ([], text) => pr_text text
       
   240             | (b, text) =>
       
   241                 let val (xs, x) = split_last b;
       
   242                 in f x; close nm; pr_text text end);
       
   243   in f end;
       
   244 
       
   245 fun write_enclosed pr template content =
       
   246   (write_open pr template; content pr; write_close pr template)
       
   247 
       
   248 fun html { lang } tags = Tag ("html",
       
   249                               [("xmlns", "http://www.w3.org/1999/xhtml"),
       
   250                                ("xml:lang", lang)],
       
   251                               tags);
       
   252 
       
   253 fun head { title, stylesheet_href } inner = let
       
   254     val link =
       
   255       Tag ("link",
       
   256         [("rel", "stylesheet"),
       
   257          ("type", "text/css"),
       
   258          ("href", stylesheet_href)], []);
       
   259     val title = Tag ("title", [], [Text title]);
       
   260     val charset = Tag ("meta",
       
   261         [("http-equiv", "Content-type"),
       
   262          ("content", "text/html; charset=UTF-8")], []);
       
   263   in Tag ("head", [], link::title::charset::inner) end;
       
   264 
       
   265 fun body common_atts tags = Tag ("body", from_common common_atts, tags);
       
   266 
       
   267 fun divele common_atts tags = Tag ("div", from_common common_atts, tags);
       
   268 fun span (common_atts, t) = Tag ("span", from_common common_atts, [Text t]);
       
   269 fun span' common_atts tags = Tag ("span", from_common common_atts, tags);
       
   270 
       
   271 fun pre common_atts rt = Tag ("pre", from_common common_atts, [RawText rt]);
       
   272 
       
   273 fun ostr_att (nm, NONE) = []
       
   274   | ostr_att (nm, SOME s) = [(nm, s)];
       
   275 val oint_att = ostr_att o apsnd (Option.map string_of_int);
       
   276 
       
   277 val table = tag' "table";
       
   278 val thead = tag' "thead";
       
   279 val tbody = tag' "tbody";
       
   280 val tr = tag "tr" [];
       
   281 fun th (common_atts, t) = Tag ("th", from_common common_atts, [Text t]);
       
   282 fun th' common_atts tags = Tag ("th", from_common common_atts, tags);
       
   283 fun td (common_atts, t) = Tag ("td", from_common common_atts, [Text t]);
       
   284 fun td' common_atts tags = Tag ("td", from_common common_atts, tags);
       
   285 fun td'' (common_atts, { colspan, rowspan }) tags =
       
   286   Tag ("td",
       
   287     from_common common_atts
       
   288     @ oint_att ("colspan", colspan)
       
   289     @ oint_att ("rowspan", rowspan),
       
   290     tags);
       
   291 
       
   292 fun p (common_atts, t) = Tag ("p", from_common common_atts, [Text t]);
       
   293 fun p' (common_atts, tags) = Tag ("p", from_common common_atts, tags);
       
   294 
       
   295 fun h (common_atts, i, text) =
       
   296   Tag ("h" ^ string_of_int i, from_common common_atts, [Text text]);
       
   297 
       
   298 fun strong t = Tag ("strong", [], [Text t]);
       
   299 fun em t = Tag ("em", [], [Text t]);
       
   300 fun a { href, text } = Tag ("a", [("href", href)], [Text text]);
       
   301 
       
   302 fun to_li tag = Tag ("li", [], [tag]);
       
   303 fun ul (common_atts, lis) = Tag ("ul", from_common common_atts, map to_li lis);
       
   304 fun ol (common_atts, lis) = Tag ("ol", from_common common_atts, map to_li lis);
       
   305 
       
   306 fun to_dtdd (nm, tag) = [Tag ("dt", [], [Text nm]),
       
   307                          Tag ("dd", [], [tag])];
       
   308 fun dl (common_atts, dtdds) =
       
   309   Tag ("dl", from_common common_atts, maps to_dtdd dtdds);
       
   310             
       
   311 fun alternate_class { class0, class1 } rows = let
       
   312     fun f ((true, xs), x) = (false, add_attributes [("class", class0)] x :: xs)
       
   313       | f ((false, xs), x) = (true, add_attributes [("class", class1)] x :: xs);
       
   314   in Library.foldl f ((true, []), rows) |> snd |> rev end;
       
   315 
       
   316 fun form (common_atts as { id, ... }, { method, action }) tags =
       
   317   Tag ("form",
       
   318     [("method", method),
       
   319      ("action", action)]
       
   320     @ from_common common_atts, tags);
       
   321 
       
   322 datatype input_type =
       
   323     TextInput of { value: string option, maxlength: int option }
       
   324   | Password of int option
       
   325   | Checkbox of { checked : bool, value : string option }
       
   326   | Radio of { checked : bool, value : string option }
       
   327   | Submit
       
   328   | Reset
       
   329   | Hidden
       
   330   | Image of { src : string, alt : string }
       
   331   | File of { accept : string }
       
   332   | Button;
       
   333 
       
   334 fun from_checked { checked = false, value = NONE }   = []
       
   335   | from_checked { checked = true,  value = NONE }   = [("checked", "checked")]
       
   336   | from_checked { checked = false, value = SOME v } = [("value", v)]
       
   337   | from_checked { checked = true,  value = SOME v } =
       
   338       [("checked", "checked"), ("value", v)];
       
   339 
       
   340 fun input_atts (TextInput { value, maxlength }) =
       
   341       ("type", "text")
       
   342        :: ostr_att ("value", value)
       
   343         @ oint_att ("maxlength", maxlength)
       
   344   | input_atts (Password NONE) = [("type", "password")]
       
   345   | input_atts (Password (SOME i)) =
       
   346       [("type", "password"), ("maxlength", string_of_int i)]
       
   347   | input_atts (Checkbox checked) =
       
   348       ("type", "checkbox") :: from_checked checked
       
   349   | input_atts (Radio checked) = ("type", "radio") :: from_checked checked
       
   350   | input_atts Submit = [("type", "submit")]
       
   351   | input_atts Reset = [("type", "reset")]
       
   352   | input_atts Hidden = [("type", "hidden")]
       
   353   | input_atts (Image { src, alt }) =
       
   354       [("type", "image"), ("src", src), ("alt", alt)]
       
   355   | input_atts (File { accept }) = [("type", "file"), ("accept", accept)]
       
   356   | input_atts Button = [("type", "button")];
       
   357 
       
   358 fun input (common_atts, { name, itype }) =
       
   359   Tag ("input",
       
   360        input_atts itype @ [("name", name)] @ from_common common_atts,
       
   361        []);
       
   362 
       
   363 fun reset_button common_atts =
       
   364   Tag ("input", input_atts Reset @ from_common common_atts, []);
       
   365 
       
   366 fun submit_button common_atts =
       
   367   Tag ("input", input_atts Submit @ from_common common_atts, []);
       
   368 
       
   369 
       
   370 fun select (common_atts, { name, value }) options =
       
   371   let
       
   372     fun is_selected t =
       
   373       (case value of
       
   374          NONE => []
       
   375        | SOME s => if t = s then bool_att ("selected", true) else []);
       
   376     fun to_option t = Tag ("option", is_selected t, [Text t]);
       
   377   in
       
   378     Tag ("select",
       
   379       ("name", name) :: from_common common_atts,
       
   380       map to_option options)
       
   381   end;
       
   382 
       
   383 fun label (common_atts, { for }, text) =
       
   384   Tag ("label", ("for", for) :: from_common common_atts, [Text text]);
       
   385 
       
   386 datatype event =
       
   387     OnClick
       
   388   | OnDblClick
       
   389   | OnMouseDown
       
   390   | OnMouseUp
       
   391   | OnMouseOver
       
   392   | OnMouseMove
       
   393   | OnMouseOut
       
   394   | OnKeyPress
       
   395   | OnKeyDown
       
   396   | OnKeyUp
       
   397   | OnFocus
       
   398   | OnBlur
       
   399   | OnSubmit
       
   400   | OnReset
       
   401   | OnSelect
       
   402   | OnChange
       
   403   | OnLoad
       
   404   | OnUnload;
       
   405 
       
   406 fun event_to_str OnClick = "onclick"
       
   407   | event_to_str OnDblClick = "ondblclick"
       
   408   | event_to_str OnMouseDown = "onmousedown"
       
   409   | event_to_str OnMouseUp = "onmouseup"
       
   410   | event_to_str OnMouseOver = "onmouseover"
       
   411   | event_to_str OnMouseMove = "onmousemove"
       
   412   | event_to_str OnMouseOut = "onmouseout"
       
   413   | event_to_str OnKeyPress = "onkeypress"
       
   414   | event_to_str OnKeyDown = "onkeydown"
       
   415   | event_to_str OnKeyUp = "onkeyup"
       
   416   | event_to_str OnFocus = "onfocus"
       
   417   | event_to_str OnBlur = "onblur"
       
   418   | event_to_str OnSubmit = "onsubmit"
       
   419   | event_to_str OnReset = "onreset"
       
   420   | event_to_str OnSelect = "onselect"
       
   421   | event_to_str OnChange = "onchange"
       
   422   | event_to_str OnLoad = "onload"
       
   423   | event_to_str OnUnload = "onunload";
       
   424 
       
   425 fun script (common_atts, {script_type, src}) =
       
   426   Tag ("script",
       
   427     ("type", script_type)
       
   428     :: ("src", src)
       
   429     :: from_common common_atts, [text ""]);
       
   430 
       
   431 fun add_script (evty, script) (Tag (name, atts, inner))
       
   432       = Tag (name, AList.update (op =) (event_to_str evty, script) atts, inner)
       
   433   | add_script _ t = t;
       
   434 
       
   435 
       
   436 val doctype_xhtml1_0_strict =
       
   437   "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\" \
       
   438   \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
       
   439 
       
   440 end;
       
   441