Reorganizing the printing of warnings; fixing line count.

The line count remains fragile though... Any idea to do it
automatically?

1 files changed, 67 insertions, 48 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 5d210b2e60..d056887591 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -278,8 +278,16 @@
           pos_lnum = lcp.pos_lnum + n;
           pos_bol = lcp.pos_cnum }
 
-  let print_position chan p =
-    Printf.fprintf chan "%s:%d:%d" p.pos_fname p.pos_lnum (p.pos_cnum - p.pos_bol)
+  let print_position_p chan p =
+    Printf.fprintf chan "%s%d, character %d"
+    (if p.pos_fname = "" then "Line " else "File \"" ^ p.pos_fname ^ "\", line ")
+    p.pos_lnum (p.pos_cnum - p.pos_bol)
+
+  let print_position chan {lex_start_p = p} = print_position_p chan p
+
+  let warn msg lexbuf =
+    eprintf "%a, warning: %s\n" print_position lexbuf msg;
+    flush stderr
 
   exception MismatchPreformatted of position
 
@@ -487,29 +495,29 @@ rule coq_bol = parse
         then Output.empty_line_of_code ();
         coq_bol lexbuf }
   | space* "(**" (space_nl as s)
-    { if is_nl s then Lexing.new_line lexbuf;
+    { if is_nl s then new_lines 1 lexbuf;
       Output.end_coq (); Output.start_doc ();
 	let eol = doc_bol lexbuf in
 	  Output.end_doc (); Output.start_coq ();
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | space* "Comments" (space_nl as s)
-      { if is_nl s then Lexing.new_line lexbuf;
+      { if is_nl s then new_lines 1 lexbuf;
         Output.end_coq (); Output.start_doc ();
         comments lexbuf;
         Output.end_doc (); Output.start_coq ();
         coq lexbuf }
   | space* begin_hide nl
-      { Lexing.new_line lexbuf; skip_hide lexbuf; coq_bol lexbuf }
+      { new_lines 1 lexbuf; skip_hide lexbuf; coq_bol lexbuf }
   | space* begin_show nl
-      { Lexing.new_line lexbuf; begin_show (); coq_bol lexbuf }
+      { new_lines 1 lexbuf; begin_show (); coq_bol lexbuf }
   | space* end_show nl
-      { Lexing.new_line lexbuf; end_show (); coq_bol lexbuf }
+      { new_lines 1 lexbuf; end_show (); coq_bol lexbuf }
   | space* begin_details (* At this point, the comment remains open,
                             and will be closed by [details_body] *)
       { let s = details_body lexbuf in
         Output.end_coq (); begin_details s; Output.start_coq (); coq_bol lexbuf }
   | space* end_details nl
-      { Lexing.new_line lexbuf;
+      { new_lines 1 lexbuf;
         Output.end_coq (); end_details (); Output.start_coq (); coq_bol lexbuf }
   | space* (("Local"|"Global") space+)? gallina_kw_to_hide
       { let s = lexeme lexbuf in
@@ -572,8 +580,7 @@ rule coq_bol = parse
 	  add_printing_token tok s;
 	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
-      { eprintf "warning: bad 'printing' command at character %d\n"
-	  (lexeme_start lexbuf); flush stderr;
+      { warn "bad 'printing' command" lexbuf;
 	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
@@ -582,8 +589,7 @@ rule coq_bol = parse
       { remove_printing_token (lexeme lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+
-      { eprintf "warning: bad 'remove printing' command at character %d\n"
-	  (lexeme_start lexbuf); flush stderr;
+      { warn "bad 'remove printing' command" lexbuf;
 	comment_level := 1;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
@@ -616,9 +622,9 @@ rule coq_bol = parse
 
 and coq = parse
   | nl
-    { Lexing.new_line lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf }
+    { new_lines 1 lexbuf; if not (only_gallina ()) then Output.line_break(); coq_bol lexbuf }
   | "(**" (space_nl as s)
-    { if is_nl s then Lexing.new_line lexbuf;
+    { if is_nl s then new_lines 1 lexbuf;
       Output.end_coq (); Output.start_doc ();
 	let eol = doc_bol lexbuf in
 	  Output.end_doc (); Output.start_coq ();
@@ -719,7 +725,7 @@ and coq = parse
 
 and doc_bol = parse
   | space* section space+ ([^'\n' '\r' '*'] | '*'+ [^'\n' '\r' ')' '*'])* ('*'+ (nl as s))?
-      { if not (is_none s) then Lexing.new_line lexbuf;
+      { if not (is_none s) then new_lines 1 lexbuf;
         let eol, lex = strip_eol (lexeme lexbuf) in
         let lev, s = sec_title lex in
           if (!Cdglobals.lib_subtitles) &&
@@ -731,7 +737,7 @@ and doc_bol = parse
   | ((space_nl* nl)? as s) (space* '-'+ as line)
       { let nl_count = count_newlines s in
         match check_start_list line with
-          | Neither -> backtrack_past_newline lexbuf; Lexing.new_line lexbuf; doc None lexbuf
+          | Neither -> backtrack_past_newline lexbuf; new_lines 1 lexbuf; doc None lexbuf
           | List n ->
               new_lines nl_count lexbuf;
               if nl_count > 0 then Output.paragraph ();
@@ -770,22 +776,24 @@ and doc_list_bol indents = parse
         verbatim 0 false lexbuf;
         doc_list_bol indents lexbuf }
   | "[[" nl
-      { formatted := Some lexbuf.lex_start_p;
+      { new_lines 1 lexbuf; formatted := Some lexbuf.lex_start_p;
         Output.start_inline_coq_block ();
         ignore(body_bol lexbuf);
         Output.end_inline_coq_block ();
         formatted := None;
         doc_list_bol indents lexbuf }
   | "[[[" nl
-      { inf_rules (Some indents) lexbuf }
+      { new_lines 1 lexbuf; inf_rules (Some indents) lexbuf }
   | space* nl space* '-'
       { (* Like in the doc_bol production, these two productions
            exist only to deal properly with whitespace *)
+        new_lines 1 lexbuf;
         Output.paragraph ();
         backtrack_past_newline lexbuf;
         doc_list_bol indents lexbuf }
   | space* nl space* _
-      { let buf' = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let buf' = lexeme lexbuf in
         let buf =
           let bufs = Str.split_delim (Str.regexp "['\n']") buf' in
             match bufs with
@@ -830,12 +838,14 @@ and doc_list_bol indents = parse
 (*s Scanning documentation elsewhere *)
 and doc indents = parse
   | nl
-      { Output.char '\n';
+      { new_lines 1 lexbuf;
+        Output.char '\n';
         match indents with
         | Some ls -> doc_list_bol ls lexbuf
         | None -> doc_bol lexbuf }
   | "[[" nl
-      { if !Cdglobals.plain_comments
+      { new_lines 1 lexbuf;
+        if !Cdglobals.plain_comments
         then (Output.char '['; Output.char '['; doc indents lexbuf)
         else (formatted := Some lexbuf.lex_start_p;
               Output.start_inline_coq_block ();
@@ -847,7 +857,7 @@ and doc indents = parse
 		  | None -> doc_bol lexbuf
 		else doc indents lexbuf)}
   | "[[[" nl
-      { inf_rules indents lexbuf }
+      { new_lines 1 lexbuf; inf_rules indents lexbuf }
   | "[]"
       { Output.proofbox (); doc indents lexbuf }
   | "{{" { url lexbuf; doc indents lexbuf }
@@ -877,7 +887,7 @@ and doc indents = parse
        doc_bol lexbuf
       }
   | '*'* "*)" space* nl
-      { true }
+      { new_lines 1 lexbuf; true }
   | '*'* "*)"
       { false }
   | "$"
@@ -952,8 +962,8 @@ and escaped_html = parse
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
 and verbatim depth inline = parse
-  | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
-  | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+  | nl ">>" space* nl { new_lines 2 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
+  | nl ">>" { new_lines 1 lexbuf; Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | ">>" { Output.stop_verbatim inline }
   | "(*" { Output.verbatim_char inline '(';
            Output.verbatim_char inline '*';
@@ -993,7 +1003,8 @@ and escaped_coq = parse
                 else skipped_comment lexbuf);
         escaped_coq lexbuf }
   | "*)"
-      { (* likely to be a syntax error: we escape *) backtrack lexbuf }
+      { (* likely to be a syntax error *)
+        warn "unterminated \"]\"" lexbuf; backtrack lexbuf }
   | eof
       { Tokens.flush_sublexer () }
   | identifier
@@ -1036,7 +1047,8 @@ and skipped_comment = parse
       { incr comment_level;
 	skipped_comment lexbuf }
   | "*)" space* nl
-      { decr comment_level;
+      { new_lines 1 lexbuf;
+        decr comment_level;
         if !comment_level > 0 then skipped_comment lexbuf else true }
   | "*)"
       { decr comment_level;
@@ -1050,7 +1062,8 @@ and comment = parse
         Output.start_comment ();
         comment lexbuf }
   | "*)" space* nl
-      { Output.end_comment ();
+      { new_lines 1 lexbuf;
+        Output.end_comment ();
         Output.line_break ();
         decr comment_level;
         if !comment_level > 0 then comment lexbuf else true }
@@ -1064,7 +1077,8 @@ and comment = parse
               escaped_coq lexbuf; Output.end_inline_coq ());
         comment lexbuf }
   | "[[" nl
-      { if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
+      { new_lines 1 lexbuf;
+        if !Cdglobals.plain_comments then (Output.char '['; Output.char '[')
         else (formatted := Some lexbuf.lex_start_p;
               Output.start_inline_coq_block ();
               let _ = body_bol lexbuf in
@@ -1099,13 +1113,14 @@ and comment = parse
       { Output.indentation (fst (count_spaces (lexeme lexbuf)));
         comment lexbuf }
   | nl
-      { Output.line_break ();
+      { new_lines 1 lexbuf;
+        Output.line_break ();
         comment lexbuf }
   | _ { Output.char (lexeme_char lexbuf 0);
         comment lexbuf }
 
 and skip_to_dot = parse
-  | '.' space* nl { true }
+  | '.' space* nl { new_lines 1 lexbuf; true }
   | eof | '.' space+ { false }
   | "(*"
       { comment_level := 1;
@@ -1114,14 +1129,14 @@ and skip_to_dot = parse
   | _ { skip_to_dot lexbuf }
 
 and skip_to_dot_or_brace = parse
-  | '.' space* nl { true }
+  | '.' space* nl { new_lines 1 lexbuf; true }
   | eof | '.' space+ { false }
   | "(*"
       { comment_level := 1;
         ignore (skipped_comment lexbuf);
         skip_to_dot_or_brace lexbuf }
   | "}" space* nl
-      { true }
+      { new_lines 1 lexbuf; true }
   | "}"
       { false }
   | space*
@@ -1134,7 +1149,7 @@ and body_bol = parse
   | "" { Output.indentation 0; body lexbuf }
 
 and body = parse
-  | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
+  | nl { Tokens.flush_sublexer(); Output.line_break(); new_lines 1 lexbuf; body_bol lexbuf}
   | (nl+ as s) space* "]]" space* nl
       { new_lines (count_newlines s + 1) lexbuf;
         Tokens.flush_sublexer();
@@ -1156,7 +1171,7 @@ and body = parse
           end }
   | "]]" space* nl
       { Tokens.flush_sublexer();
-        Lexing.new_line lexbuf;
+        new_lines 1 lexbuf;
         if is_none !formatted then
           begin
 	    let loc = lexeme_start lexbuf in
@@ -1265,31 +1280,31 @@ and string = parse
   | _      { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf }
 
 and skip_hide = parse
-  | eof | end_hide nl { Lexing.new_line lexbuf; () }
+  | eof | end_hide nl { new_lines 1 lexbuf; () }
   | _ { skip_hide lexbuf }
 
 (*s Reading token pretty-print *)
 
 and printing_token_body = parse
   | "*)" (nl as s)? | eof
-    { if not (is_none s) then Lexing.new_line lexbuf;
+    { if not (is_none s) then new_lines 1 lexbuf;
       let s = Buffer.contents token_buffer in
 	  Buffer.clear token_buffer;
 	  s }
   | (nl | _) as s
-    { if is_nl s then Lexing.new_line lexbuf;
+    { if is_nl s then new_lines 1 lexbuf;
       Buffer.add_string token_buffer (lexeme lexbuf);
 	  printing_token_body lexbuf }
 
 and details_body = parse
   | "*)" space* (nl as s)? | eof
-      { if not (is_none s) then Lexing.new_line lexbuf;
+      { if not (is_none s) then new_lines 1 lexbuf;
         None }
   | ":" space*  { details_body_rec lexbuf }
 
 and details_body_rec = parse
   | "*)" space* (nl as s)? | eof
-        { if not (is_none s) then Lexing.new_line lexbuf;
+        { if not (is_none s) then new_lines 1 lexbuf;
           let s = Buffer.contents token_buffer in
           Buffer.clear token_buffer;
           Some s }
@@ -1300,9 +1315,10 @@ and details_body_rec = parse
     enclosed in [[[  ]]] brackets *)
 and inf_rules indents = parse
   | space* nl     (* blank line, before or between definitions *)
-      { inf_rules indents lexbuf }
+      { new_lines 1 lexbuf; inf_rules indents lexbuf }
   | "]]]" nl      (* end of the inference rules block *)
-      { match indents with
+      { new_lines 1 lexbuf;
+        match indents with
         | Some ls -> doc_list_bol ls lexbuf
         | None -> doc_bol lexbuf }
   | _ 
@@ -1315,7 +1331,8 @@ and inf_rules indents = parse
 *)
 and inf_rules_assumptions indents assumptions = parse
   | space* "---" '-'* [^ '\n']* nl (* hit the horizontal line *)
-      { let line = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let line = lexeme lexbuf in
         let (spaces,_) = count_spaces line in
         let dashes_and_name = 
                cut_head_tail_spaces (String.sub line 0 (String.length line - 1))
@@ -1334,7 +1351,8 @@ and inf_rules_assumptions indents assumptions = parse
           inf_rules_conclusion indents (List.rev assumptions) 
                                (spaces, dashes, name) [] lexbuf }
   | [^ '\n']* nl (* if it's not the horizontal line, it's an assumption *)
-      { let line = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let line = lexeme lexbuf in
         let (spaces,_) = count_spaces line in
         let assumption = cut_head_tail_spaces 
                             (String.sub line 0 (String.length line - 1))
@@ -1348,11 +1366,12 @@ and inf_rules_assumptions indents assumptions = parse
     blank line or a ']]]'. *)
 and inf_rules_conclusion indents assumptions middle conclusions = parse
   | space* nl | space* "]]]" nl (* end of conclusions. *)
-      { backtrack lexbuf;
+      { new_lines 2 lexbuf; backtrack lexbuf;
         Output.inf_rule assumptions middle (List.rev conclusions);
         inf_rules indents lexbuf }
   | space* [^ '\n']+ nl (* this is a line in the conclusion *)
-      { let line = lexeme lexbuf in
+      { new_lines 1 lexbuf;
+        let line = lexeme lexbuf in
         let (spaces,_) = count_spaces line in
         let conc = cut_head_tail_spaces (String.sub line 0 
                                                     (String.length line - 1))
@@ -1395,16 +1414,16 @@ and st_subtitle = parse
 {
   (* coq_bol with error handling *)
   let coq_bol' f lb =
-    Lexing.new_line lb; (* Start numbering lines from 1 *)
     try coq_bol lb with
     | MismatchPreformatted p ->
-      Printf.eprintf "%a: mismatched \"[[\"\n" print_position { p with pos_fname = f };
+      Printf.eprintf "%a: mismatched \"[[\"\n" print_position_p p;
       exit 1
 
   let coq_file f m =
     reset ();
     let c = open_in f in
     let lb = from_channel c in
+    let lb = { lb with lex_start_p = { lb.lex_start_p with pos_fname = f } } in
       (Index.current_library := m;
        Output.initialize ();
        Output.start_module ();