Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update styling of SourceFilePage content #1609

Open
wants to merge 11 commits into
base: master
Choose a base branch
from
2 changes: 2 additions & 0 deletions .editorconfig
@@ -0,0 +1,2 @@
[*.java]
indent_style = tab
Expand Up @@ -60,8 +60,9 @@ public SourceFilePage(final ISourceNode sourceFileNode,

@Override
protected void content(final HTMLElement body) throws IOException {
final SourceHighlighter hl = new SourceHighlighter(context.getLocale());
hl.render(body, getNode(), sourceReader);
final SourceHighlighter highlighter;
highlighter = new SourceHighlighter(context.getLocale());
highlighter.render(body, getNode(), sourceReader);
sourceReader.close();
}

Expand All @@ -76,8 +77,9 @@ protected void head(final HTMLElement head) throws IOException {

@Override
protected String getOnload() {
return format("window['PR_TAB_WIDTH']=%d;prettyPrint()",
Integer.valueOf(tabWidth));
String setTabWidth = format("window['PR_TAB_WIDTH']=%d", tabWidth);
String invokePrettyPrint = "prettyPrint()";
return setTabWidth + ";" + invokePrettyPrint;
}

@Override
Expand Down
Expand Up @@ -77,9 +77,6 @@ public final class Styles {
/** Block of source code */
public static final String SOURCE = "source";

/** Line number before each source line */
public static final String NR = "nr";

/** Part of source code where instructions are not covered */
public static final String NOT_COVERED = "nc";

Expand Down
Expand Up @@ -80,6 +80,9 @@ h1 {
pre.source {
border:#d6d3ce 1px solid;
font-family:monospace;
background-color: #f3f3f3;
border-radius: 20px;
padding: 10px;
}

pre.source ol {
Expand All @@ -88,8 +91,8 @@ pre.source ol {
}

pre.source li {
border-left: 1px solid #D6D3CE;
color: #A0A0A0;
border-left: 0px;
color: black;
padding-left: 0px;
}

Expand Down