From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- tools/coqdoc/coqdoc.sty | 5 +---- tools/coqdoc/cpretty.mll | 13 ++++++++++--- tools/coqdoc/index.ml | 46 ++++++++++++++++++++++++++++++++++------------ tools/coqdoc/output.ml | 4 ++-- 4 files changed, 47 insertions(+), 21 deletions(-) (limited to 'tools') diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 4314d07d..9de9a38f 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -83,7 +83,7 @@ \newcommand{\coqdocnotation}[1]{\coqdockw{#1}} \newcommand{\coqdocsection}[1]{\coqdoccst{#1}} \newcommand{\coqdocaxiom}[1]{\coqdocax{#1}} -\newcommand{\coqdocmoduleid}[1]{\coqdocmod{#1}} +\newcommand{\coqdocmodule}[1]{\coqdocmod{#1}} % Environment encompassing code fragments % !!! CAUTION: This environment may have empty contents @@ -107,9 +107,6 @@ % Empty lines (in code only) \newcommand{\coqdocemptyline}{\vskip 0.4em plus 0.1em minus 0.1em} -% macro for typesetting the title of a module implementation -\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} -} \usepackage{ifpdf} \ifpdf \RequirePackage{hyperref} diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index a23a4f74..177058b3 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cpretty.mll 13440 2010-09-19 20:21:12Z herbelin $ i*) +(*i $Id: cpretty.mll 13692 2010-12-06 23:55:10Z herbelin $ i*) (*s Utility functions for the scanners *) @@ -272,7 +272,9 @@ let firstchar = (* superscript 1 *) '\194' '\185' | (* utf-8 latin 1 supplement *) - '\195' ['\128'-'\191'] | + '\195' ['\128'-'\150'] | + '\195' ['\152'-'\182'] | + '\195' ['\184'-'\191'] | (* utf-8 letterlike symbols *) (* '\206' ([ '\145' - '\183'] | '\187') | *) (* '\xCF' [ '\x00' - '\xCE' ] | *) @@ -315,7 +317,6 @@ let def_token = | "Class" | "SubClass" | "Example" - | "Local" | "Fixpoint" | "Boxed" | "CoFixpoint" @@ -450,6 +451,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 e8f30853..a28e1197 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: index.ml 13676 2010-12-04 10:34:21Z herbelin $ i*) open Filename open Lexing @@ -216,7 +216,7 @@ let type_name = function | Library -> let ln = !lib_name in if ln <> "" then String.lowercase ln else "library" - | Module -> "moduleid" + | Module -> "module" | Definition -> "definition" | Inductive -> "inductive" | Constructor -> "constructor" @@ -235,23 +235,45 @@ 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) *) + (* 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 begin + if (!j = l || s.[!j+1] <> '\'') then quoted := false + else (ntn.[!k] <- s.[!j]; incr k; incr j) + end 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 ^ ")" diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index cbebbd79..4f9dd169 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 13541 2010-10-13 19:53:29Z notin $ i*) +(*i $Id: output.ml 13676 2010-12-04 10:34:21Z herbelin $ i*) open Cdglobals open Index @@ -287,7 +287,7 @@ module Latex = struct printf "\\coqdocindent{%2.2fem}\n" space let module_ref m s = - printf "\\moduleid{%s}{%s}" m (escaped s) + printf "\\coqdocmodule{%s}{%s}" m (escaped s) let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in -- cgit v1.2.3