diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 2 | ||||
| -rw-r--r-- | tools/coqdoc/coqdoc.css | 5 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 7 |
3 files changed, 10 insertions, 4 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 0202b3136b..745bbb7e55 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -66,7 +66,7 @@ VERBOSE ?= TIMED?= TIMECMD?= # Use command time on linux, gtime on Mac OS -TIMEFMT?="$* (real: %e, user: %U, sys: %S, mem: %M ko)" +TIMEFMT?="$@ (real: %e, user: %U, sys: %S, mem: %M ko)" ifneq (,$(TIMED)) ifeq (0,$(shell command time -f "" true >/dev/null 2>/dev/null; echo $$?)) STDTIME?=command time -f $(TIMEFMT) diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 2c2bd98541..48096e555a 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -331,3 +331,8 @@ ul.doclist { margin-top: 0em; margin-bottom: 0em; } + +.code :target { + border: 2px solid #D4D4D4; + background-color: #e5eecc; +} diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 04725aa26f..def1cbbcf8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -659,7 +659,8 @@ module Html = struct let reference s r = match r with | Def (fullid,ty) -> - printf "<a name=\"%s\">" (sanitize_name fullid); + let s' = sanitize_name fullid in + printf "<a id=\"%s\" class=\"idref\" href=\"#%s\">" s' s'; printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s @@ -820,7 +821,7 @@ module Html = struct | Some n -> if lev <= n then add_toc_entry (Toc_section (lev, f, r)) else ()); stop_item (); - printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev; + printf "<a id=\"%s\"></a><h%d class=\"section\">" lab lev; f (); printf "</h%d>\n" lev @@ -834,7 +835,7 @@ module Html = struct let letter_index category idx (c,l) = if l <> [] then begin let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in - printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; + printf "<a id=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat; List.iter (fun (id,(text,link,t)) -> let id' = prepare_entry id t in |