aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/cpretty.mll
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-12 18:47:47 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-12 18:47:47 +0000
commit7216342d32fdc05b3fc37f7a76bb1031b89c7e02 (patch)
treeffc4e1c4a4fd904bbe6a87e6db7ecd3b4a4fa1be /tools/coqdoc/cpretty.mll
parenta67549d2ec769e48dacf4938209871a83cdc4f91 (diff)
Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les versions de OCaml antérieures à 3.11.0)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12512 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/cpretty.mll')
-rw-r--r--tools/coqdoc/cpretty.mll9
1 files changed, 8 insertions, 1 deletions
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index c20449bcd..4742a2e5d 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -15,6 +15,13 @@
open Printf
open Lexing
+ (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *)
+ let new_line lexbuf =
+ let pos = lexbuf.lex_curr_p in
+ lexbuf.lex_curr_p <- { pos with
+ pos_lnum = pos.pos_lnum + 1;
+ pos_bol = pos.pos_cnum }
+
(* A list function we need *)
let rec take n ls =
if n = 0 then [] else
@@ -989,7 +996,7 @@ and body_bol = parse
| _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
and body = parse
- | nl {Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
+ | nl {Output.line_break(); new_line lexbuf; body_bol lexbuf}
| nl+ space* "]]" space* nl
{ if not !formatted then
begin