From b8194b22f93912079d07714c945a3f273347fad5 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 4 Dec 2010 10:34:07 +0000 Subject: Fixing several bugs with links to notation in coqdoc, including bug #2445: - single quotes in notations were breaking coqdoc, even raising an out-of-bound error when appearing in the last character of the notation; - letter "x" in notation tokens were inelegantly surrounded by single quotes, - rare, but allowed characters < 32 were lost in index pages. A new fully injective space-free-and-human-readable encoding algorithm is adopted which put single quotes around all terminal tokens, double existing single quotes, and replace invisible characters by ^X-like strings. Moreover, the keywords "Local"/"Global" were blocking the detection of keywords starting coq lines (e.g. "Local Notation" was not recognized as a notation). "Local" and "Global" are now uniformly treated as modifiers of vernac commands as they are in the Coq parser. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13673 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tools/coqdoc/cpretty.mll | 7 ++++++- tools/coqdoc/index.ml | 44 ++++++++++++++++++++++++++++++++++---------- 2 files changed, 40 insertions(+), 11 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 8fb705f2c..27e8f0b96 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -312,7 +312,6 @@ let def_token = | "Class" | "SubClass" | "Example" - | "Local" | "Fixpoint" | "Function" | "Boxed" @@ -448,6 +447,12 @@ rule coq_bol = parse { begin_show (); coq_bol lexbuf } | space* end_show { end_show (); coq_bol lexbuf } + | space* ("Local"|"Global") + { + in_proof := None; + let s = lexeme lexbuf in + output_indented_keyword s lexbuf; + coq_bol lexbuf } | space* gallina_kw_to_hide { let s = lexeme lexbuf in if !Cdglobals.light && section_or_end s then diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 089bb7f09..d9f5d9e1e 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -232,23 +232,47 @@ let type_name = function let prepare_entry s = function | Notation -> - (* Notations have conventially the form section.:sc:x_++_'x'_x *) + (* We decode the encoding done in Dumpglob.cook_notation of coqtop *) + (* Encoded notations have the form section:sc:x_'++'_x where: *) + (* - the section, if any, ends with a "." *) + (* - the scope can be empty *) + (* - tokens are separated with "_" *) + (* - non-terminal symbols are conventionally represented by "x" *) + (* - terminals are enclosed within simple quotes *) + (* - existing simple quotes (that necessarily are parts of *) + (* terminals) are doubled *) + (* (as a consequence, when a terminal contains "_" or "x", these *) + (* necessarily appear enclosed within non-doubled simple quotes) *) + (* - non-printable characters < 32 are left encoded so that they *) + (* are human-readable in index files *) + (* Example: "x ' %x _% y %'x %'_' z" is encoded as *) + (* "x_''''_'%x'_'_%'_x_'%''x'_'%''_'''_x" *) let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in let sc = String.sub s (h+1) (i-h-1) in - let ntn = String.make (String.length s) ' ' in + let ntn = String.make (String.length s - i) ' ' in let k = ref 0 in let j = ref (i+1) in let quoted = ref false in - while !j <> String.length s do - if s.[!j] = '_' && not !quoted then ntn.[!k] <- ' ' else - if s.[!j] = 'x' && not !quoted then ntn.[!k] <- '_' else - if s.[!j] = '\'' then - if s.[!j+1] = 'x' && s.[!j+1] = '\'' then (ntn.[!k] <- 'x'; j:=!j+2) - else (quoted := not !quoted; ntn.[!k] <- '\'') - else ntn.[!k] <- s.[!j]; - incr j; incr k + let l = String.length s - 1 in + while !j <= l do + if not !quoted then begin + (match s.[!j] with + | '_' -> ntn.[!k] <- ' '; incr k + | 'x' -> ntn.[!k] <- '_'; incr k + | '\'' -> quoted := true + | _ -> assert false) + end + else + if s.[!j] = '\'' then + if (!j = l || s.[!j+1] = '_') then quoted := false + else (incr j; ntn.[!k] <- s.[!j]; incr k) + else begin + ntn.[!k] <- s.[!j]; + incr k + end; + incr j done; let ntn = String.sub ntn 0 !k in if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" -- cgit v1.2.3