It should be possible to include line feeds in labels

Currently a hack is used for introducing line feeds into labels: double spaces are replaced in JavaScript by the line feed character "\n". It should be possible to use a straight syntax for specifying line feeds in labels.