aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-04-06 07:26:19 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-04-06 07:26:19 +0000
commit2874c296bc0433ea0c1666b0a50231264b8489f6 (patch)
tree9d96acff91ad493404f1dfb621cefeb3f1ab668c /tools/coqdoc/output.ml
parenta473afc22bf69267c91f9806cb6587a879025105 (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/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml10
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 "&amp;"
| 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