Module Wd_encoding

module Wd_encoding: sig .. end

This module contains the output encodings. The encodings are functions from string to string. They are usually entered into the application by default (see the method output_encoding of the Wd_types.application_type), and accessible by <ui:encoding> and other elements of the UI language.

The functions defined here assume that an ASCII-compatible character set is used.

val encode_as_html : string -> string

Encodes strings as HTML:

'<' becomes <
'>' becomes >
'"' becomes "
'&' becomes &

All other characters remain unchanged.

From <ui:encoding>, this function is accessible under the name html.

val encode_as_pre : string -> string

Does the following encoding:

' ' becomes  
'\n' becomes <br>
'\t' is expanded to a sequence of  , tab width is 8

All other characters remain unchanged.

From <ui:encoding>, this function is accessible under the name pre.

val encode_as_para : string -> string

Multiple linefeeds are replaced by <p>.

From <ui:encoding>, this function is accessible under the name para.

val encode_as_js_string : string -> string

Encodes strings such that they can be placed between quotes in Javascript.

'\' becomes backslash backslash
'"' becomes backslash double-quotes
''' becomes backslash single-quote
'<' becomes \x3c
'%' becomes \x25

The characters 0 to 31 and 127 become \xHH All other characters remain unchanged.

From <ui:encoding>, this function is accessible under the name js.

val encode_as_js_longstring : enc:Pxp_types.rep_encoding -> string -> string

Similar to encode_as_js_string, but an additional rules prevents that long lines result. (Javascript interpreters often cannot cope with long lines.) The string is split up into pieces p1,...,pN and these are connected by p1" + \n "p2" + \n ... + \n "pN

From <ui:encoding>, this function is accessible under the name jslong.

It is required to pass the character encoding of the strings as argument enc. In the case the encoding uses multi-byte character representations, it is avoided to break up these characters.

Note that you can combine the various encodings to get new effects. Reasonable combinations are:

encode_as_html then encode_as_pre
encode_as_html then encode_as_para
encode_as_html then encode_as_para then encode_as_pre
encode_as_html then encode_as_js_string
encode_as_html then encode_as_js_longstring

... and more