Correction d'un bug de Coqdoc (indentation des lignes)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10583 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 23 insertions, 23 deletions

diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index 290c77fcb..47d7780cc 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -104,9 +104,9 @@ let make_fullid id =
 let split_sp s = 
   try
     let i = String.rindex s '.' in
-    String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
-  with Not_found -> 
-    "", s
+      String.sub s 0 i, String.sub s (i + 1) (String.length s - i - 1)
+  with 
+      Not_found -> "", s
 
 let modules = Hashtbl.create 97
 let local_modules = Hashtbl.create 97
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 5744f4d6e..2998e8c25 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -435,11 +435,11 @@ let produce_document l =
       copy src dst;
       List.iter read_glob l);
   (if !target_language=LaTeX then
-    let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
-    let dst = if !output_dir <> "" then 
-      Filename.concat !output_dir "coqdoc.sty" 
-    else "coqdoc.sty" in
-      copy src dst);
+      let src = (Filename.concat !Cdglobals.coqlib_path "/tools/coqdoc/coqdoc.sty") in
+      let dst = if !output_dir <> "" then 
+	  Filename.concat !output_dir "coqdoc.sty" 
+	else "coqdoc.sty" in
+	copy src dst);
   List.iter index_module l;
   match !out_to with
     | StdOut -> 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index e0d2a3c99..9a6bcd568 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -22,12 +22,12 @@
   let count_spaces s =
     let n = String.length s in
     let rec count c i = 
-      if i == n then c else match s.[i] with
+      if i == n then c,i else match s.[i] with
 	| '\t' -> count (c + (8 - (c mod 8))) (i + 1)
 	| ' ' -> count (c + 1) (i + 1)
-	| _ -> c
+	| _ -> c,i
     in
-    count 0 0
+      count 0 0
 
   let count_dashes s =
     let c = ref 0 in
@@ -350,27 +350,27 @@ rule coq_bol = parse
 	      if eol then (line_break (); coq_bol lexbuf) else coq lexbuf
 	  else 
 	    begin
-	      let nbsp = count_spaces s in
+	      let nbsp,isp = count_spaces s in
 		indentation nbsp; 
-		let s = String.sub s nbsp (String.length s - nbsp) in
-		  ident s (lexeme_start lexbuf + nbsp); 
+		let s = String.sub s isp (String.length s - isp) in
+		  ident s (lexeme_start lexbuf + isp); 
 		  let eol = body lexbuf in 
 		    if eol then coq_bol lexbuf else coq lexbuf
 	    end }
   | space* gallina_kw
       { let s = lexeme lexbuf in 
-	let nbsp = count_spaces s in
-	let s = String.sub s nbsp (String.length s - nbsp)  in
+	let nbsp,isp = count_spaces s in
+	let s = String.sub s isp (String.length s - isp)  in
 	  indentation nbsp;
-	  ident s (lexeme_start lexbuf + nbsp); 
+	  ident s (lexeme_start lexbuf + isp); 
 	  let eol= body lexbuf in
 	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* prog_kw
       { let s = lexeme lexbuf in 
-	let nbsp = count_spaces s in
+	let nbsp,isp = count_spaces s in
 	  indentation nbsp;
-	  let s = String.sub s nbsp (String.length s - nbsp)  in
-	    ident s (lexeme_start lexbuf + nbsp); 
+	  let s = String.sub s isp (String.length s - isp)  in
+	    ident s (lexeme_start lexbuf + isp); 
 	    let eol= body lexbuf in
 	      if eol then coq_bol lexbuf else coq lexbuf }
 
@@ -495,7 +495,7 @@ and doc = parse
 	doc lexbuf }
   | "[[" nl space*
       { formatted := true; line_break (); start_inline_coq ();
-	indentation (count_spaces (lexeme lexbuf)); 
+	indentation (fst (count_spaces (lexeme lexbuf))); 
 	let eol = body_bol lexbuf in 
 	  end_inline_coq (); formatted := false;
 	  if eol then doc_bol lexbuf else doc lexbuf}
@@ -604,7 +604,7 @@ and skip_to_dot = parse
 
 and body_bol = parse
   | space+
-      { indentation (count_spaces (lexeme lexbuf)); body lexbuf }
+      { indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
   | _ { backtrack lexbuf; body lexbuf }
 
 and body = parse
@@ -632,7 +632,7 @@ and body = parse
 
 and notation_bol = parse
   | space+
-      { indentation (count_spaces (lexeme lexbuf)); notation lexbuf }
+      { indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
   | _ { backtrack lexbuf; notation lexbuf }
 
 and notation = parse