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

1 files changed, 3 insertions, 3 deletions

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