div.report-size { width: 620 }
pre { background:#eeeeff; margin:2px; padding:4px; font-size:9pt }