diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 20 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 9 |
2 files changed, 28 insertions, 1 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 779d10e99d..af8bac2c10 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -284,6 +284,11 @@ let pfx_id = (id '.')* let identifier = id | pfx_id id +let utf8_multibyte = + [ '\xC0'-'\xDF' ] _ + | [ '\xE0'-'\xEF' ] _ _ + | [ '\xF0'-'\xF7' ] _ _ _ + (* This misses unicode stuff, and it adds "[" and "]". It's only an approximation of idents - used for detecting whether an underscore is part of an identifier or meant to indicate emphasis *) @@ -1067,6 +1072,16 @@ and body = parse | ".." { Output.char '.'; Output.char '.'; body lexbuf } + | '"' + { Output.char '"'; + string lexbuf; + body lexbuf } + + | utf8_multibyte + { let c = lexeme lexbuf in + symbol lexbuf c; + body lexbuf } + | _ { let c = lexeme_char lexbuf 0 in Output.char c; body lexbuf } @@ -1093,6 +1108,11 @@ and notation_string = parse Output.char c; notation_string lexbuf } +and string = parse + | "\"\"" { Output.char '"'; Output.char '"'; string lexbuf } + | '"' { Output.char '"' } + | _ { let c = lexeme_char lexbuf 0 in Output.char c; string lexbuf } + and skip_hide = parse | eof | end_hide { () } | _ { skip_hide lexbuf } diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 434a8bf5b5..889e5d6ff9 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -314,10 +314,17 @@ let read_glob f = current_library := !cur_mod | 'R' -> (try + Scanf.sscanf s "R%d:%d %s %s %s %s" + (fun loc1 loc2 lib_dp sp id ty -> + for loc=loc1 to loc2 do + add_ref !cur_mod loc lib_dp sp id (type_of_string ty) + done) + with _ -> + try Scanf.sscanf s "R%d %s %s %s %s" (fun loc lib_dp sp id ty -> add_ref !cur_mod loc lib_dp sp id (type_of_string ty)) - with _ -> ()) + with _ -> ()) | _ -> try Scanf.sscanf s "%s %d %s %s" (fun ty loc sp id -> add_def loc (type_of_string ty) sp id) |