Fix issue with line numbers introduced in 6534384.

There was a missing call to Lexing.new_line when lexing a line in a doc comment consisting of only ws + "*" + "\n". This caused line number information to get out of sync resulting in bad latex output and (presumably) other issues.
rems-project · Apr 27, 2024 · bb50f71 · bb50f71
1 parent 5719799
commit bb50f71
Showing 1 changed file with 4 additions and 6 deletions.
diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll
@@ -297,12 +297,10 @@ and doc_comment pos b depth lstart = parse
                                             doc_comment pos b (depth - 1) false lexbuf
 					  ) }
   | "\n"                                { Buffer.add_string b "\n"; Lexing.new_line lexbuf; doc_comment pos b depth true lexbuf }
-  | wsc+ "*\n" as prefix                { if lstart then (
-                                            Buffer.add_string b "\n";
-                                            doc_comment pos b depth true lexbuf
-                                          ) else (
-                                            Buffer.add_string b prefix; doc_comment pos b depth true lexbuf
-                                          ) }
+  | wsc+ "*\n" as prefix                { let s = if lstart then "\n" else prefix in
+                                          Buffer.add_string b s;
+                                          Lexing.new_line lexbuf;
+                                          doc_comment pos b depth true lexbuf }
   | wsc+ "*" wsc as prefix              { if lstart then (
                                             Buffer.add_string b (String.make (String.length prefix - 3) ' ');
                                             doc_comment pos b depth false lexbuf