mirror of
https://github.com/dart-lang/sdk
synced 2024-09-16 00:29:48 +00:00
Pad line number appropriately when generating script insets.
This avoid jagged indentation when we jump from 9->10, 99->100, etc. BUG= R=johnmccutchan@google.com Review URL: https://codereview.chromium.org/1402193003 .
This commit is contained in:
parent
ecd7457bb3
commit
f5a07f6a9c
|
@ -824,6 +824,11 @@ class ScriptInsetElement extends ObservatoryElement {
|
|||
return table;
|
||||
}
|
||||
|
||||
var endLine = (endPos != null
|
||||
? script.tokenToLine(endPos)
|
||||
: script.lines.length + script.lineOffset);
|
||||
var lineNumPad = endLine.toString().length;
|
||||
|
||||
annotationsCursor = 0;
|
||||
|
||||
int blankLineCount = 0;
|
||||
|
@ -840,17 +845,17 @@ class ScriptInsetElement extends ObservatoryElement {
|
|||
if (blankLineCount < 4) {
|
||||
// Too few blank lines for an elipsis.
|
||||
for (int j = firstBlank; j <= lastBlank; j++) {
|
||||
table.append(lineElement(script.getLine(j)));
|
||||
table.append(lineElement(script.getLine(j), lineNumPad));
|
||||
}
|
||||
} else {
|
||||
// Add an elipsis for the skipped region.
|
||||
table.append(lineElement(script.getLine(firstBlank)));
|
||||
table.append(lineElement(null));
|
||||
table.append(lineElement(script.getLine(lastBlank)));
|
||||
table.append(lineElement(script.getLine(firstBlank), lineNumPad));
|
||||
table.append(lineElement(null, lineNumPad));
|
||||
table.append(lineElement(script.getLine(lastBlank), lineNumPad));
|
||||
}
|
||||
blankLineCount = 0;
|
||||
}
|
||||
table.append(lineElement(line));
|
||||
table.append(lineElement(line, lineNumPad));
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -876,11 +881,11 @@ class ScriptInsetElement extends ObservatoryElement {
|
|||
return annotation;
|
||||
}
|
||||
|
||||
Element lineElement(ScriptLine line) {
|
||||
Element lineElement(ScriptLine line, int lineNumPad) {
|
||||
var e = new DivElement();
|
||||
e.classes.add("sourceRow");
|
||||
e.append(lineBreakpointElement(line));
|
||||
e.append(lineNumberElement(line));
|
||||
e.append(lineNumberElement(line, lineNumPad));
|
||||
e.append(lineSourceElement(line));
|
||||
return e;
|
||||
}
|
||||
|
@ -952,9 +957,9 @@ class ScriptInsetElement extends ObservatoryElement {
|
|||
return e;
|
||||
}
|
||||
|
||||
Element lineNumberElement(ScriptLine line) {
|
||||
Element lineNumberElement(ScriptLine line, int lineNumPad) {
|
||||
var lineNumber = line == null ? "..." : line.line;
|
||||
var e = span("$nbsp$lineNumber$nbsp");
|
||||
var e = span("$nbsp${lineNumber.toString().padLeft(lineNumPad,nbsp)}$nbsp");
|
||||
e.classes.add('noCopy');
|
||||
|
||||
if (lineNumber == _currentLine) {
|
||||
|
|
Loading…
Reference in a new issue