diff --git a/regression/goto-instrument/document-properties-basic/html.desc b/regression/goto-instrument/document-properties-basic/html.desc index b73e500ba57..8f8e013d792 100644 --- a/regression/goto-instrument/document-properties-basic/html.desc +++ b/regression/goto-instrument/document-properties-basic/html.desc @@ -3,7 +3,7 @@ main.c --document-properties-html ^EXIT=0$ ^SIGNAL=0$ -^ assert\(1 == 1\);<\/em>$ +^\s*\d+   assert\(1 == 1\);<\/em>$ -- ^warning: ignoring -- diff --git a/src/goto-instrument/document_properties.cpp b/src/goto-instrument/document_properties.cpp index 10ef4892c60..9c6aa50aff4 100644 --- a/src/goto-instrument/document_properties.cpp +++ b/src/goto-instrument/document_properties.cpp @@ -225,6 +225,11 @@ document_propertiest::get_code(const source_locationt &source_location) // build dest + std::size_t max_line_number_width = 0; + if(!lines.empty()) + { + max_line_number_width = std::to_string(lines.back().line_number).size(); + } for(std::list::iterator it=lines.begin(); it!=lines.end(); it++) { @@ -235,10 +240,10 @@ document_propertiest::get_code(const source_locationt &source_location) switch(format) { case LATEX: - while(line_no.size()<4) + while(line_no.size() < max_line_number_width) line_no=" "+line_no; - line_no+" "; + line_no += " "; tmp+=escape_latex(it->text, true); @@ -248,10 +253,10 @@ document_propertiest::get_code(const source_locationt &source_location) break; case HTML: - while(line_no.size()<4) + while(line_no.size() < max_line_number_width) line_no=" "+line_no; - line_no+"  "; + line_no += "  "; tmp+=escape_html(it->text); @@ -261,7 +266,7 @@ document_propertiest::get_code(const source_locationt &source_location) break; } - dest+=tmp+"\n"; + dest += line_no + tmp + "\n"; } return dest;