") : "")
+}
+
+
+function html_begin_pre()
+{
+ In_PRE = 1
+ print_line("")
+}
+
+
+function html_begin_title()
+{
+ return ((HTML && (Url != "")) ? ("") : "")
+}
+
+
+function html_begin_toc()
+{
+ html_end_toc()
+ html_begin_pre()
+}
+
+
+function html_body( k)
+{
+ for (k = 1; k <= BodyLines; ++k)
+ print Body[k]
+}
+
+function html_breakpoint(title,maxlength, break_after,k)
+{
+ # Return the largest character position in title AFTER which we
+ # can break the title across lines, without exceeding maxlength
+ # visible characters.
+ if (html_length(title) > maxlength) # then need to split title across lines
+ {
+ # In the presence of HTML markup, the initialization of
+ # k here is complicated, because we need to advance it
+ # until html_length(title) is at least maxlength,
+ # without invoking the expensive html_length() function
+ # too frequently. The need to split the title makes the
+ # alternative of delayed insertion of HTML markup much
+ # more complicated.
+ break_after = 0
+ for (k = min(maxlength,length(title)); k < length(title); ++k)
+ {
+ if (substr(title,k+1,1) == " ")
+ { # could break after position k
+ if (html_length(substr(title,1,k)) <= maxlength)
+ break_after = k
+ else # advanced too far, retreat back to last break_after
+ break
+ }
+ }
+ if (break_after == 0) # no breakpoint found by forward scan
+ { # so switch to backward scan
+ for (k = min(maxlength,length(title)) - 1; \
+ (k > 0) && (substr(title,k+1,1) != " "); --k)
+ ; # find space at which to break title
+ if (k < 1) # no break point found
+ k = length(title) # so must print entire string
+ }
+ else
+ k = break_after
+ }
+ else # title fits on one line
+ k = length(title)
+ return (k)
+}
+
+
+
+function html_end_issue()
+{
+ print_line(prefix(3) "")
+ print_line(prefix(2) "