Exclude parentheses from the location of parenthesized operators.

This allows why3doc to generate anchors for operator definitions,
including "(*)".

src/parser/parser.mly

@@ -979,8 +979,12 @@ lident_rich:
 | lident_op_id  { $1 }
 
 lident_op_id:
-| LEFTPAR lident_op RIGHTPAR  { mk_id $2 $startpos $endpos }
-| LEFTPAR_STAR_RIGHTPAR       { mk_id (infix "*") $startpos $endpos }
+| LEFTPAR lident_op RIGHTPAR  { mk_id $2 $startpos($2) $endpos($2) }
+| LEFTPAR_STAR_RIGHTPAR
+    { (* parentheses are removed from the location *)
+      let s = let s = $startpos in { s with pos_cnum = s.pos_cnum + 1 } in
+      let e = let e = $endpos   in { e with pos_cnum = e.pos_cnum - 1 } in
+      mk_id (infix "*") s e }
 
 lident_op:
 | op_symbol               { infix $1 }

src/why3doc/doc_lexer.mll

@@ -51,15 +51,18 @@
 
   let current_file = ref ""
 
-  let print_ident fmt lexbuf s =
+  let print_ident ?(parentheses=false) fmt lexbuf s =
     if is_keyword1 s then
       fprintf fmt "<span class=\"keyword1\">%s</span>" s
     else if is_keyword2 s then
       fprintf fmt "<span class=\"keyword2\">%s</span>" s
     else begin
-      let (* f,l,c as *) loc = get_loc lexbuf in
-      (* Format.eprintf "  IDENT %s/%d/%d@." f l c; *)
-      (* is this a def point? *)
+      let loc =
+        let loc = get_loc lexbuf in
+        if parentheses then
+          let (f,l,s,e) = Loc.get loc in
+          Loc.user_position f l (s + 1) (e - 1)
+        else loc in
       try
         let id, def = Glob.find loc in
         match id.Ident.id_loc with
@@ -107,8 +110,9 @@ let ident = ['A'-'Z' 'a'-'z' '_'] ['A'-'Z' 'a'-'z' '0'-'9' '_']* | operator
 let special = ['\'' '"' '<' '>' '&']
 
 rule scan fmt empty = parse
-  | "(*)" as s
-          { pp_print_string fmt s;
+  | "(*)" { pp_print_char fmt '(';
+            print_ident ~parentheses:true fmt lexbuf "*";
+            pp_print_char fmt ')';
             scan fmt NotEmpty lexbuf }
   | space* "(***"
           { comment fmt false lexbuf;