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