file: escape strings in HTML output