@@ -37,8 +37,8 @@ public HTMLWriter(StyledText styledText, int start, int length) {
3737 @ Override
3838 public void close () {
3939 if (!isClosed ()) {
40- write ("</div>\n " );
41- write ("</div>\n " );
40+ write ("</div>" );
41+ write ("</div>" );
4242 super .close ();
4343 }
4444 }
@@ -52,29 +52,27 @@ void writeHeader() {
5252 appendStyle (innerDivStyle , "color:" , styledText .getForeground (), ";" );
5353 appendStyle (innerDivStyle , "background-color:" , styledText .getBackground (), ";" );
5454
55- appendStyle (outerDivStyle , "padding-left:" , styledText .getLeftMargin (), "px;" );
56- appendStyle (outerDivStyle , "padding-top:" , styledText .getTopMargin (), "px;" );
57- appendStyle (outerDivStyle , "padding-right:" , styledText .getRightMargin (), "px;" );
58- appendStyle (outerDivStyle , "padding-bottom:" , styledText .getBottomMargin (), "px;" );
55+ appendStyle (outerDivStyle , "padding:"
56+ + styledText .getTopMargin () + "px "
57+ + styledText .getRightMargin () + "px "
58+ + styledText .getBottomMargin () + "px "
59+ + styledText .getLeftMargin () + "px;" );
5960
6061 String language = appendFont (innerDivStyle , styledText .getFont (), 0 );
6162
62- // Using wrapIndent like this messes up the line background (if set).
63- // int wrapIndent = styledText.getWrapIndent();
64- // if (wrapIndent != 0) {
65- // appendStyle(globalStyle, "padding-left:", wrapIndent, "px;");
66- // }
67- // int indent = styledText.getIndent() - wrapIndent;
6863 int indent = styledText .getIndent ();
6964 if (indent != 0 ) {
7065 appendStyle (innerDivStyle , "text-indent:" , indent , "px;" );
7166 }
7267
73- // TODO?
74- // int lineSpacing = styledText.getLineSpacing();
75-
76- if (!styledText .getWordWrap ()) {
77- appendStyle (innerDivStyle , "white-space:nowrap;" );
68+ if (styledText .getWordWrap ()) {
69+ // Sequences of white space are preserved.
70+ // Lines are broken at newline characters, at <br>, and as necessary to fill line boxes.
71+ appendStyle (innerDivStyle , "white-space:pre-wrap;" );
72+ } else {
73+ // Sequences of white space are preserved.
74+ // Lines are only broken at newline characters in the source and at <br> elements.
75+ appendStyle (innerDivStyle , "white-space:pre;" );
7876 }
7977
8078 appendAlignAndJustify (innerDivStyle , styledText .getAlignment (), styledText .getJustify ());
@@ -83,17 +81,11 @@ void writeHeader() {
8381 appendStyle (innerDivStyle , "direction:rtl;" );
8482 }
8583
86- // Do we have any use for these?
87- // Color selectionBackground = styledText.getSelectionBackground();
88- // Color selectionForeground = styledText.getSelectionForeground();
89- // int tabs = styledText.getTabs();
90- // boolean blockSelection = styledText.getBlockSelection();
91-
92- write ("<div style='" + outerDivStyle + "'>\n " );
84+ write ("<div style='" + outerDivStyle + "'>" );
9385 if (language == null || language .isEmpty ()) {
94- write ("<div style='" + innerDivStyle + "'>\n " );
86+ write ("<div style='" + innerDivStyle + "'>" );
9587 } else {
96- write ("<div lang='" + language + "' style='" + innerDivStyle + "'>\n " );
88+ write ("<div lang='" + language + "' style='" + innerDivStyle + "'>" );
9789 }
9890 }
9991
@@ -102,7 +94,7 @@ public void writeLineDelimiter(String lineDelimiter) {
10294 if (isClosed ()) {
10395 SWT .error (SWT .ERROR_IO );
10496 }
105- write ( lineDelimiter );
97+ // We don't write the newline, otherwise it would be rendered because of the `white-space:pre;`.
10698 }
10799
108100 @ Override
@@ -117,8 +109,11 @@ String writeLineStart(Color lineBackground, int indent, int verticalIndent, int
117109 appendStyle (paragraphStyle , "text-indent:" , indent , "px;" );
118110 }
119111
120- if (verticalIndent != 0 ) {
121- appendStyle (paragraphStyle , "margin-top:" , verticalIndent , "px;" );
112+ if (verticalIndent == 0 ) {
113+ appendStyle (paragraphStyle , "margin:0;" );
114+ } else {
115+ // Set the margin-top to verticalIndent, everything else zero.
116+ appendStyle (paragraphStyle , "margin:" , verticalIndent , " 0 0 0;" );
122117 }
123118
124119 if (paragraphStyle .length () == 0 ) {
@@ -131,6 +126,11 @@ String writeLineStart(Color lineBackground, int indent, int verticalIndent, int
131126 return "</p>" ;
132127 }
133128
129+ @ Override
130+ void writeEmptyLine () {
131+ write ("<br>" );
132+ }
133+
134134 @ Override
135135 String writeSpanStart (StyleRange style ) {
136136 StringBuilder spanStyle = new StringBuilder ();
0 commit comments