diff options
author | 2009-01-21 12:53:33 +0000 | |
---|---|---|
committer | 2009-01-21 12:53:33 +0000 | |
commit | 0deeb743b6b90b7be64d150c142ed5ef77d77943 (patch) | |
tree | ac477c7f4209c5c216db039ffab19a7df7cbf194 /tools/coqdoc | |
parent | 27a7627fe5f9b3d3715abb133229ebc446dd983b (diff) |
- Better deal with commands inside section titles in latex output using
the support from hyperref.
- Rename n-ary 'exist' tactic to 'exists' in Program.Syntax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11821 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/coqdoc.sty | 5 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 28 | ||||
-rw-r--r-- | tools/coqdoc/pretty.mll | 7 |
3 files changed, 26 insertions, 14 deletions
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index fdf11cb9c..ef4f41195 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -101,11 +101,12 @@ \newcommand{\coqref}[2]{\hyperlink{coq:#1}{#2}} \newcommand{\identref}[2]{\hyperlink{coq:#1}{\textsf {#2}}} \newcommand{\coqlibrary}[2]{\cleardoublepage\phantomsection - \hypertarget{coq:#1}{\chapter{Library \coqdoccst{#2}}}} + \hypertarget{coq:#1}{\chapter{Library \texorpdfstring{\coqdoccst}{}{#2}}}} \else \newcommand{\coqdef}[3]{#3} \newcommand{\coqref}[2]{#2} - \newcommand{\identref}[2]{\textsf {#2}} + \newcommand{\texorpdfstring}[2]{#1} + \newcommand{\identref}[2]{\textsf{#2}} \newcommand{\coqlibrary}[2]{\cleardoublepage\chapter{Library \coqdoccst{#2}}} \fi \usepackage{xr} diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index b38cf7b9a..568fade17 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -32,7 +32,7 @@ let build_table l = let is_keyword = build_table - [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; + [ "AddPath"; "Axiom"; "Abort"; "Boxed"; "Chapter"; "Check"; "Coercion"; "CoFixpoint"; "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint"; "Hypothesis"; "Hypotheses"; @@ -139,6 +139,9 @@ let new_label = let r = ref 0 in fun () -> incr r; "lab" ^ string_of_int !r module Latex = struct + let in_title = ref false + let in_doc = ref false + (*s Latex preamble *) let (preamble : string Queue.t) = Queue.create () @@ -266,7 +269,7 @@ module Latex = struct ident_ref m fullid typ s | Mod _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" - + let ident s loc = if is_keyword s then begin printf "\\coqdockw{"; raw_ident s; printf "}" @@ -278,16 +281,23 @@ module Latex = struct if is_tactic s then begin printf "\\coqdoctac{"; raw_ident s; printf "}" end else begin - if !Cdglobals.interpolate then + if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) + then try reference s (Index.find_string !current_module s) - with _ -> printf "\\coqdocvar{"; raw_ident s; printf "}" + with _ -> (printf "\\coqdocvar{"; raw_ident s; printf "}") else (printf "\\coqdocvar{"; raw_ident s; printf "}") end end end - let ident s l = with_latex_printing (fun s -> ident s l) s - + let ident s l = + if !in_title then ( + printf "\\texorpdfstring{"; + with_latex_printing (fun s -> ident s l) s; + printf "}{"; raw_ident s; printf "}") + else + with_latex_printing (fun s -> ident s l) s + let symbol = with_latex_printing raw_ident let rec reach_item_level n = @@ -306,9 +316,9 @@ module Latex = struct let stop_item () = reach_item_level 0 - let start_doc () = () + let start_doc () = in_doc := true - let end_doc () = stop_item () + let end_doc () = in_doc := false; stop_item () let start_coq () = printf "\\begin{coqdoccode}\n" @@ -328,7 +338,7 @@ module Latex = struct let section lev f = stop_item (); output_string (section_kind lev); - f (); + in_title := true; f (); in_title := false; printf "}\n\n" let rule () = diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index dc07e8156..f460cfb12 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -217,7 +217,7 @@ let thm_token = | "Proposition" | "Property" | "Goal" - | "Next Obligation" + | "Next" space+ "Obligation" let def_token = "Definition" @@ -227,6 +227,7 @@ let def_token = | "Example" | "Local" | "Fixpoint" + | "Boxed" | "CoFixpoint" | "Record" | "Structure" @@ -235,7 +236,7 @@ let def_token = | "CoInductive" | "Equations" | "Instance" - | "Global Instance" + | "Global" space+ "Instance" let decl_token = "Hypothesis" @@ -289,7 +290,7 @@ let commands = | ("Hypothesis" | "Hypotheses") | "End" -let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" +let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort" let extraction = "Extraction" |