Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing

rules (bug report #2293).
Restored the sequential extension of the printing rules tables (that
commit #12905 replaced by a per-file modification of the printing
rules table). Note however that the table grows in the order of
compilation of files by coqdoc, which does not necessarily coincide
with the order of coqc compilation dependencies of the files.
Added documentation of coqdoc option "--external".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 18 insertions, 18 deletions

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index b70053173..56ee459ab 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -217,7 +217,7 @@
     Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
   let printing_token_re =
     Str.regexp
-      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
+      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\(&#\\|[^#]\\)*\\)#\\)?"
 
   let add_printing_token toks pps =
     try
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0f36b775c..1892a0c9c 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -115,7 +115,7 @@ let initialize_texmacs () =
       "|-", ensuremath "vdash"
     ] Tokens.empty_ttree
 
-let token_tree_texmacs = lazy (initialize_texmacs ())
+let token_tree_texmacs = ref (initialize_texmacs ())
 
 let initialize_tex_html () =
   let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in
@@ -144,18 +144,18 @@ let initialize_tex_html () =
 	(* "fun", "\\ensuremath{\\lambda}" ? *)
       ] (Tokens.empty_ttree,Tokens.empty_ttree)
 
-let token_tree_latex = lazy (fst (initialize_tex_html ()))
-let token_tree_html = lazy (snd (initialize_tex_html ()))
+let token_tree_latex = ref (fst (initialize_tex_html ()))
+let token_tree_html = ref (snd (initialize_tex_html ()))
 
 let add_printing_token s (t1,t2) =
-  match
-    (match !Cdglobals.target_language with LaTeX -> t1 | HTML -> t2 | _ -> None)
-  with
-  | None -> ()
-  | Some t -> Tokens.token_tree := Tokens.ttree_add !Tokens.token_tree s t
+  (match t1 with None -> () | Some t1 ->
+    token_tree_latex := Tokens.ttree_add !token_tree_latex s t1);
+  (match t2 with None -> () | Some t2 ->
+    token_tree_html := Tokens.ttree_add !token_tree_html s t2)
 
 let remove_printing_token s =
-  Tokens.token_tree := Tokens.ttree_remove !Tokens.token_tree s
+  token_tree_latex := Tokens.ttree_remove !token_tree_latex s;
+  token_tree_html := Tokens.ttree_remove !token_tree_html s
 
 (*s Table of contents *)
 
@@ -342,7 +342,7 @@ module Latex = struct
     Tokens.output_tagged_symbol_char tag c
 
   let initialize () =
-    Tokens.token_tree := Lazy.force token_tree_latex;
+    Tokens.token_tree := token_tree_latex;
     Tokens.outfun := output_sublexer_string
 
   (*s Interpreting ident with fallback on sublexer if unknown ident *)
@@ -602,7 +602,7 @@ module Html = struct
     Tokens.output_tagged_symbol_char tag c
 
   let initialize () =
-    Tokens.token_tree := Lazy.force token_tree_html;
+    Tokens.token_tree := token_tree_html;
     Tokens.outfun := output_sublexer_string
 
   let translate s =
@@ -885,7 +885,7 @@ module TeXmacs = struct
     if !in_doc then Tokens.output_tagged_symbol_char None c else char c
 
   let initialize () =
-    Tokens.token_tree := Lazy.force token_tree_texmacs;
+    Tokens.token_tree := token_tree_texmacs;
     Tokens.outfun := output_sublexer_string
 
   let proofbox () = printf "QED"
@@ -1002,7 +1002,7 @@ module Raw = struct
   let sublexer c l = char c
 
   let initialize () =
-    Tokens.token_tree := Tokens.empty_ttree;
+    Tokens.token_tree := ref Tokens.empty_ttree;
     Tokens.outfun := (fun _ _ _ _ -> failwith "Useless")
 
   let proofbox () = printf "[]"
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 7de3ad80d..c2a47308d 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -74,7 +74,7 @@ let ttree_find ttree str =
 
 type out_function = bool -> bool -> Index.index_entry option -> string -> unit
 
-let token_tree = ref empty_ttree
+let token_tree = ref (ref empty_ttree)
 let outfun = ref (fun _ _ _ _ -> failwith "outfun not initialized")
 
 (*s Translation automaton *)
@@ -142,7 +142,7 @@ let buffer_char is_symbolchar ctag c =
 	end
 
   and restart_buffering () =
-    let tt = try ttree_descend !token_tree c with Not_found -> empty_ttree in
+    let tt = try ttree_descend !(!token_tree) c with Not_found -> empty_ttree in
     Buffer.add_char buff c;
     Buffering (is_symbolchar,ctag,"",tt)
 
@@ -168,4 +168,4 @@ let flush_sublexer () =
 
 (* Translation not using the automaton *)
 let translate s =
-  try (ttree_find !token_tree s).node with Not_found -> None
+  try (ttree_find !(!token_tree) s).node with Not_found -> None
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index 4e53108ac..a85e75c47 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -65,7 +65,7 @@ type out_function =
   string -> unit
 
 (* This must be initialized before calling the sublexer *)
-val token_tree : ttree ref
+val token_tree : ttree ref ref
 val outfun : out_function ref
 
 (* Process an ident part that might be a symbol part *)