diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/cpretty.mll | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 26 | ||||
| -rw-r--r-- | tools/coqdoc/tokens.ml | 6 | ||||
| -rw-r--r-- | tools/coqdoc/tokens.mli | 2 |
4 files changed, 18 insertions, 18 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index b700531739..56ee459ab9 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 0f36b775cd..1892a0c9c5 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 7de3ad80da..c2a47308d1 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 4e53108ac0..a85e75c472 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 *) |