diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-06 07:26:19 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-04-06 07:26:19 +0000 |
commit | 2874c296bc0433ea0c1666b0a50231264b8489f6 (patch) | |
tree | 9d96acff91ad493404f1dfb621cefeb3f1ab668c /tools | |
parent | a473afc22bf69267c91f9806cb6587a879025105 (diff) |
echappement de <, > et & en HTML
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdoc/output.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index b6a4a063e..615d22486 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -358,11 +358,13 @@ module Html = struct | '&' -> printf "&" | c -> output_char c + let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done + let latex_char _ = () let latex_string _ = () - let html_char = output_char - let html_string = output_string + let html_char = char + let html_string = raw_ident let start_latex_math () = () let stop_latex_math () = () @@ -370,8 +372,6 @@ module Html = struct let start_verbatim () = printf "<pre>" let stop_verbatim () = printf "</pre>\n" - let raw_ident s = for i = 0 to String.length s - 1 do char s.[i] done - let module_ref m s = printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>" (*i @@ -805,7 +805,7 @@ let start_verbatim = let stop_verbatim = select Latex.stop_verbatim Html.stop_verbatim TeXmacs.stop_verbatim let verbatim_char = - select output_char output_char TeXmacs.char + select output_char Html.char TeXmacs.char let make_index = select Latex.make_index Html.make_index TeXmacs.make_index let make_toc = select Latex.make_toc Html.make_toc TeXmacs.make_toc |