r8620@thot: notin | 2006-03-08 11:44:16 +0100

 Modifications diverses de Coqdoc:
   - modification du comportement par défaut de l'option --latex
   - ajout d'une option --stdout
   - réaménagement dans les sources (création de global.ml)
   - modification du parser de coqdoc pour regler les problèmes liés à 
     la syntaxe V8.
   - Correction du bug #1052 sur les commentaires en fin de ligne
 


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

8 files changed, 400 insertions, 364 deletions

diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
new file mode 100644
index 0000000000..b5a4cb22cf
--- /dev/null
+++ b/tools/coqdoc/cdglobals.ml
@@ -0,0 +1,72 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+
+
+(*s Output options *)
+
+type target_language = LaTeX | HTML | TeXmacs
+
+let target_language = ref HTML
+
+type output_t =
+  | StdOut
+  | MultFiles
+  | File of string
+
+let output_dir = ref ""
+
+let out_to = ref MultFiles
+
+let out_channel = ref stdout
+
+let open_out_file f =
+  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
+    out_channel := open_out f
+
+let close_out_file () = close_out !out_channel
+
+
+let header_trailer = ref true
+let quiet = ref false
+let light = ref false
+let gallina = ref false
+let short = ref false
+let index = ref true
+let multi_index = ref false
+let toc = ref false
+let page_title = ref ""
+let title = ref ""
+let externals = ref true
+let coqlib = ref "http://coq.inria.fr/library/"
+let raw_comments = ref false
+
+let charset = ref "iso-8859-1"
+let inputenc = ref ""
+let latin1 = ref false
+let utf8 = ref false
+
+let set_latin1 () =
+  charset := "iso-8859-1";
+  inputenc := "latin1";
+  latin1 := true
+
+let set_utf8 () =
+  charset := "utf-8";
+  inputenc := "utf8";
+  utf8 := true
+
+(* Parsing options *)
+
+type coq_module = string
+
+type file =
+  | Vernac_file of string * coq_module
+  | Latex_file of string
+      
+
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 243a3750b9..1af3945708 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-type coq_module = string
+open Cdglobals
 
 type loc = int
 
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ae19433f93..091372de48 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -14,7 +14,7 @@ open Filename
 open Lexing 
 open Printf
 
-type coq_module = string
+open Cdglobals
 
 type loc = int
 
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 820ad8240d..d43df8d34e 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -18,6 +18,7 @@
  * It may be removed or abbreviated as far as I am concerned.
  *)
 
+open Cdglobals
 open Filename
 open Printf
 open Output
@@ -33,6 +34,7 @@ let usage () =
   prerr_endline "  --texmacs           produce a TeXmacs document";
   prerr_endline "  --dvi               output the DVI";
   prerr_endline "  --ps                output the PostScript";
+  prerr_endline "  --stdout            write output to stdout";
   prerr_endline "  -o <file>           write output in file <file>";
   prerr_endline "  -d <dir>            output files into directory <dir>";
   prerr_endline "  -g                  (gallina) skip proofs";
@@ -71,7 +73,12 @@ let banner () =
   eprintf "This is coqdoc version %s, compiled on %s\n"
     Coq_config.version Coq_config.compile_date;
   flush stderr
-    
+
+let target_full_name f = 
+  let basefile = chop_suffix f ".v" in
+    match !target_language with
+      | HTML -> basefile ^ ".html"
+      | _ -> basefile ^ ".tex"
 
 (*s \textbf{Separation of files.} Files given on the command line are
     separated according to their type, which is determined by their
@@ -232,8 +239,10 @@ let parse () =
 	multi_index := true; parse_rec rem
     | ("-toc" | "--toc" | "--table-of-contents") :: rem ->
 	toc := true; parse_rec rem
+    | ("-stdout" | "--stdout") :: rem ->
+	out_to := StdOut; parse_rec rem
     | ("-o" | "--output") :: f :: rem ->
-	output_file := f; parse_rec rem
+	out_to := File f; parse_rec rem
     | ("-o" | "--output") :: [] -> 
 	usage ()
     | ("-d" | "--directory") :: dir :: rem ->
@@ -251,30 +260,29 @@ let parse () =
     | ("-t" | "-title" | "--title") :: [] ->
 	usage ()
     | ("-latex" | "--latex") :: rem ->
-	Output.target_language := LaTeX; parse_rec rem
+	Cdglobals.target_language := LaTeX; parse_rec rem
     | ("-dvi" | "--dvi") :: rem ->
-	Output.target_language := LaTeX; dvi := true; parse_rec rem
+	Cdglobals.target_language := LaTeX; dvi := true; parse_rec rem
     | ("-ps" | "--ps") :: rem ->
-	Output.target_language := LaTeX; ps := true; parse_rec rem
+	Cdglobals.target_language := LaTeX; ps := true; parse_rec rem
     | ("-html" | "--html") :: rem ->
-	Output.target_language := HTML; parse_rec rem
+	Cdglobals.target_language := HTML; parse_rec rem
     | ("-texmacs" | "--texmacs") :: rem ->
-	Output.target_language := TeXmacs; parse_rec rem
-
+	Cdglobals.target_language := TeXmacs; parse_rec rem
     | ("-charset" | "--charset") :: s :: rem ->
-	Output.charset := s; parse_rec rem
+	Cdglobals.charset := s; parse_rec rem
     | ("-charset" | "--charset") :: [] ->
 	usage ()
     | ("-inputenc" | "--inputenc") :: s :: rem ->
-	Output.inputenc := s; parse_rec rem
+	Cdglobals.inputenc := s; parse_rec rem
     | ("-inputenc" | "--inputenc") :: [] ->
 	usage ()
     | ("-raw-comments" | "--raw-comments") :: rem ->
-	Output.raw_comments := true; parse_rec rem
+	Cdglobals.raw_comments := true; parse_rec rem
     | ("-latin1" | "--latin1") :: rem ->
-	Output.set_latin1 (); parse_rec rem
+	Cdglobals.set_latin1 (); parse_rec rem
     | ("-utf8" | "--utf8") :: rem ->
-	Output.set_utf8 (); parse_rec rem
+	Cdglobals.set_utf8 (); parse_rec rem
 
     | ("-q" | "-quiet" | "--quiet") :: rem ->
 	quiet := true; parse_rec rem
@@ -298,7 +306,6 @@ let parse () =
 	parse_rec rem
     | ("-files" | "--files") :: [] ->
 	usage ()
-
     | "-R" :: path :: log :: rem -> 
 	add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
@@ -308,12 +315,11 @@ let parse () =
     | ("-glob-from" | "--glob-from") :: [] ->
 	usage ()
     | ("--no-externals" | "-no-externals" | "-noexternals") :: rem ->
-	Output.externals := false; parse_rec rem
+	Cdglobals.externals := false; parse_rec rem
     | ("--coqlib" | "-coqlib") :: u :: rem ->
-	Output.coqlib := u; parse_rec rem
+	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
-
     | f :: rem -> 
 	add_file (what_file f); parse_rec rem
   in 
@@ -360,52 +366,114 @@ let copy src dst =
   with End_of_file ->
     close_in cin; close_out cout
 
+(*s Functions for generating output files *)
+
+let gen_one_file l =
+  let file = function
+    | Vernac_file (f,m) -> 
+	set_module m; coq_file f m
+    | Latex_file _ -> ()
+  in
+    header ();
+    if !toc then make_toc ();
+    List.iter file l;
+    if !index then make_index();
+    trailer ()
+      
+let gen_mult_files l =
+  let file = function
+    | Vernac_file (f,m) -> 
+	set_module m;
+	let hf = target_full_name f in
+	  open_out_file hf;
+	  header (); 
+	  if !toc then make_toc ();
+	  coq_file f m; 
+	  trailer ();
+	  close_out_file()
+    | Latex_file _ -> ()
+  in
+    List.iter file l;
+    if (!index && !target_language=HTML) then begin
+      open_out_file "index.html"; 
+      page_title := (if !title <> "" then !title else "Index");
+      header (); make_index (); trailer ();
+      close_out_file()
+    end;
+    if (!toc && !target_language=HTML) then begin
+      open_out_file "toc.html"; 
+      page_title := (if !title <> "" then !title else "Table of contents");
+      header ();
+      if !title <> "" then printf "<h1>%s</h1>\n" !title;
+      make_toc (); 
+      trailer ();
+      close_out_file()
+    end 
+      (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
+
+
+let index_module = function
+  | Vernac_file (_,m) -> Index.add_module m
+  | Latex_file _ -> ()
+
+let produce_document l =
+  List.iter index_module l;
+  match !out_to with
+    | StdOut -> 
+	Cdglobals.out_channel := stdout;
+	gen_one_file l
+    | File f ->
+	open_out_file f;
+	gen_one_file l;
+	close_out_file()
+    | MultFiles ->
+	gen_mult_files l
+
 let produce_output fl =
   if not (!dvi || !ps) then begin
-    if !output_file <> "" then set_out_file !output_file;
     produce_document fl
   end else begin
     let texfile = temp_file "coqdoc" ".tex" in
     let basefile = chop_suffix texfile ".tex" in
-    set_out_file texfile;
-    produce_document fl;
-    let command = 
-      let file = basename texfile in
-      let file = 
-	if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
-      in
-      sprintf "(latex %s && latex %s) 1>&2 %s" file file
-	(if !quiet then "> /dev/null" else "")
-    in
-    let res = locally (dirname texfile) Sys.command command in
-    if res <> 0 then begin
-      eprintf "Couldn't run LaTeX successfully\n"; 
-      clean_and_exit basefile res
-    end;
-    let dvifile = basefile ^ ".dvi" in
-    if !dvi then begin
-      if !output_file <> "" then 
-	(* we cannot use Sys.rename accross file systems *)
-	copy dvifile !output_file 
-      else 
-	cat dvifile
-    end;
-    if !ps then begin
-      let psfile = 
-	if !output_file <> "" then !output_file else basefile ^ ".ps" 
-      in
+      open_out_file texfile;
+      produce_document fl;
       let command = 
-	sprintf "dvips %s -o %s %s" dvifile psfile 
-	  (if !quiet then "> /dev/null 2>&1" else "")
+	let file = basename texfile in
+	let file = 
+	  if !quiet then sprintf "'\\nonstopmode\\input{%s}'" file else file 
+	in
+	  sprintf "(latex %s && latex %s) 1>&2 %s" file file
+	    (if !quiet then "> /dev/null" else "")
       in
-      let res = Sys.command command in
-      if res <> 0 then begin
-	eprintf "Couldn't run dvips successfully\n"; 
-	clean_and_exit basefile res
-      end;
-      if !output_file = "" then cat psfile
-    end;
-    clean_temp_files basefile
+      let res = locally (dirname texfile) Sys.command command in
+	if res <> 0 then begin
+	  eprintf "Couldn't run LaTeX successfully\n"; 
+	  clean_and_exit basefile res
+	end;
+	let dvifile = basefile ^ ".dvi" in
+	  if !dvi then begin
+	    if !output_file <> "" then 
+	      (* we cannot use Sys.rename accross file systems *)
+	      copy dvifile !output_file 
+	    else 
+	      cat dvifile
+	  end;
+	  if !ps then begin
+	    let psfile = 
+	      if !output_file <> "" then !output_file else basefile ^ ".ps" 
+	    in
+	    let command = 
+	      sprintf "dvips %s -o %s %s" dvifile psfile 
+		(if !quiet then "> /dev/null 2>&1" else "")
+	    in
+	    let res = Sys.command command in
+	      if res <> 0 then begin
+		eprintf "Couldn't run dvips successfully\n"; 
+		clean_and_exit basefile res
+	      end;
+	      if !output_file = "" then cat psfile
+	  end;
+	  clean_temp_files basefile
   end
 
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index c81bbf7a43..fcf83a391a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -8,28 +8,11 @@
 
 (*i $Id$ i*)
 
+open Cdglobals
 open Index
 
-(*s Target language *)
-
-type target_language = LaTeX | HTML | TeXmacs
-
-let target_language = ref HTML
-
 (*s Low level output *)
 
-let out_channel = ref stdout
-let output_is_file = ref false
-let output_dir = ref ""
-
-let set_out_file f = 
-  let f = if !output_dir <> "" then Filename.concat !output_dir f else f in
-  out_channel := open_out f;
-  output_is_file := true
-
-let close () =
-  if !output_is_file then close_out !out_channel
-
 let output_char c = Pervasives.output_char !out_channel c
 
 let output_string s = Pervasives.output_string !out_channel s
@@ -38,43 +21,6 @@ let printf s = Printf.fprintf !out_channel s
 
 let sprintf = Printf.sprintf
 
-let dump_file f =
-  let ch = open_in f in
-  try
-    while true do
-      Pervasives.output_char !out_channel (input_char ch)
-    done
-  with End_of_file -> close_in ch
-
-(*s Options *)
-
-let header_trailer = ref true
-let quiet = ref false
-let light = ref false
-let short = ref false
-let index = ref true
-let multi_index = ref false
-let toc = ref false
-let page_title = ref ""
-let title = ref ""
-let externals = ref true
-let coqlib = ref "http://coq.inria.fr/library/"
-let raw_comments = ref false
-
-let charset = ref "iso-8859-1"
-let inputenc = ref ""
-let latin1 = ref false
-let utf8 = ref false
-
-let set_latin1 () =
-  charset := "iso-8859-1";
-  inputenc := "latin1";
-  latin1 := true
-
-let set_utf8 () =
-  charset := "utf-8";
-  inputenc := "utf8";
-  utf8 := true
 
 (*s Coq keywords *)
 
@@ -85,9 +31,9 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "Add"; "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
+    [ "AddPath"; "Axiom"; "Chapter"; "CoFixpoint";
       "CoInductive"; "Defined"; "Definition"; 
-      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Hint";
+      "End"; "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
       "Immediate"; "Implicit"; "Import"; "Inductive"; 
       "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; 
@@ -508,14 +454,14 @@ module Html = struct
   let separate_index navig i =
     let idx = i.idx_name in
     let one_letter ((c,l) as cl) =
-      set_out_file (sprintf "index_%s_%c.html" idx c);
+      open_out_file (sprintf "index_%s_%c.html" idx c);
       header ();
       navig ();
       printf "<hr/>";
       letter_index true idx cl;
       if List.length l > 30 then begin printf "<hr/>"; navig () end;
       trailer ();
-      close ()
+      close_out_file ()
     in
     List.iter one_letter i.idx_entries
 
@@ -556,43 +502,26 @@ module Html = struct
     printf "</table>\n"
 
   let make_index () =
-    if !index then begin
-      let idxl = 
-	let glob,bt = Index.all_entries () in
+    let idxl = 
+      let glob,bt = Index.all_entries () in
 	format_global_index glob ::
-	List.map format_bytype_index bt 
-      in
-      let navig () = navig_index idxl in 
-      set_out_file "index.html";
+	  List.map format_bytype_index bt 
+    in
+    let navig () = navig_index idxl in 
       current_module := "Index";
-      page_title := (if !title <> "" then !title else "Index");
-      header ();
+      let one_index i =
+	if i.idx_size > 0 then begin
+	  printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
+	  all_letters i
+	end
+	in
       if !title <> "" then printf "<h1>%s</h1>\n" !title;
       navig ();
-      if !multi_index then begin
-	trailer (); 
-	close ();
-	List.iter (separate_index navig) idxl;
-      end else begin
-	let one_index i =
-	  if i.idx_size > 0 then begin
-	    printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
-	    all_letters i
-	  end
-	in
-	List.iter one_index idxl;
-	printf "<hr/>";
-	navig ();
-	trailer ();
-	close ()
-      end;
-    end
+      List.iter one_index idxl;
+      printf "<hr/>";
+      navig ()
 
   let make_toc () = 
-    set_out_file "toc.html";
-    page_title := (if !title <> "" then !title else "Table of contents");
-    header ();
-    if !title <> "" then printf "<h1>%s</h1>\n" !title;
     let make_toc_entry = function
       | Toc_library m -> 
 	  stop_item ();
@@ -603,9 +532,6 @@ module Html = struct
     in
     Queue.iter make_toc_entry toc_q;
     stop_item ();
-    if !index then printf "<a href=\"index.html\"><h2>Index</h2></a>";
-    trailer ();
-    close ()
 
 end
 
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index dd38dd68f5..f80dca3223 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -8,33 +8,9 @@
 
 (*i $Id$ i*)
 
+open Cdglobals
 open Index
 
-type target_language = LaTeX | HTML | TeXmacs
-
-val target_language : target_language ref
-
-val set_out_file : string -> unit
-val output_dir : string ref
-val close : unit -> unit
-
-val quiet : bool ref
-val short : bool ref
-val light : bool ref
-val header_trailer : bool ref
-val index : bool ref
-val multi_index : bool ref
-val toc : bool ref
-val title : string ref
-val externals : bool ref
-val coqlib : string ref
-val raw_comments : bool ref
-
-val charset : string ref
-val inputenc : string ref
-val set_latin1 : unit -> unit
-val set_utf8 : unit -> unit
-
 val add_printing_token : string -> string option * string option -> unit
 val remove_printing_token : string -> unit
 
@@ -45,8 +21,6 @@ val trailer : unit -> unit
 
 val push_in_preamble : string -> unit
 
-val dump_file : string -> unit
-
 val start_module : unit -> unit
 
 val start_doc : unit -> unit
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli
index e7314a1b53..f02a79be50 100644
--- a/tools/coqdoc/pretty.mli
+++ b/tools/coqdoc/pretty.mli
@@ -10,10 +10,4 @@
 
 open Index
 
-type file =
-  | Vernac_file of string * coq_module
-  | Latex_file of string
-
-val gallina : bool ref
-
-val produce_document : file list -> unit
+val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index 29119e3f86..9d695950cd 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -12,6 +12,7 @@
 
 {
 
+  open Cdglobals
   open Printf
   open Index
   open Lexing 
@@ -56,44 +57,8 @@
 
   let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
 
-  (* Gallina (skipping proofs). This is a three states automaton. *)   
-
-  let gallina = ref false
-
-  type gallina_state = Nothing | AfterDot | Proof
-
-  let gstate = ref AfterDot
-
-  let glet = ref false
-
-  let is_proof = 
-    let t = Hashtbl.create 13 in
-    List.iter (fun s -> Hashtbl.add t s true)
-      [ "Theorem"; "Lemma"; "Fact"; "Remark"; "Goal"; "Let";
-	"Correctness"; "Definition"; "Morphism" ];
-    fun s -> try Hashtbl.find t s with Not_found -> false
-
-  let gallina_id id = 
-    if !gstate = AfterDot then
-      if is_proof id then gstate := Proof else 
-	if id <> "Add" then gstate := Nothing
-
-  let gallina_symbol s = 
-    if !gstate = AfterDot then 
-      gstate := Nothing
-    else
-      if (!gstate = Proof && s = ":=") then 
-	if !glet then glet := false else gstate := Nothing
-
   let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
 
-  let gallina_char c = 
-    if c = '.' then
-      (let skip = !gstate = Proof in gstate := AfterDot; skip)
-    else
-      (if !gstate = AfterDot && not (is_space c) then gstate := Nothing;
-       false)
-
   (* saving/restoring the PP state *)
 
   type state = {
@@ -126,9 +91,7 @@
 
   let reset () =
     formatted := false;
-    brackets := 0;
-    gstate := AfterDot;
-    glet := false
+    brackets := 0
 
   (* erasing of Section/End *)
 
@@ -222,6 +185,100 @@ let symbolchar_no_brackets =
 let symbolchar = symbolchar_no_brackets | '[' | ']'
 let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
 
+
+let thm_token = 
+  "Theorem" 
+  | "Lemma" 
+  | "Fact" 
+  | "Remark" 
+  | "Corollary" 
+  | "Proposition" 
+  | "Property"
+  | "Goal"
+
+let def_token = 
+  "Definition" 
+  | "Let" 
+  | "SubClass" 
+  | "Example"
+  | "Local" 
+  | "Fixpoint" 
+  | "CoFixpoint" 
+  | "Record" 
+  | "Structure" 
+  | "Scheme"
+  | "Inductive"
+  | "CoInductive"
+
+let decl_token = 
+  "Hypothesis" 
+  | "Hypotheses" 
+  | "Parameter" 
+  | "Axiom" 's'? 
+  | "Conjecture"
+
+let gallina_ext =
+  "Module" 
+  | "Declare"
+  | "Transparent"
+  | "Opaque"
+  | "Canonical"
+  | "Coercion"
+  | "Identity"
+  | "Implicit"
+  | "Notation"
+  | "Infix"
+  | "Tactic" space+ "Notation"
+  | "Reserved" space+ "Notation"
+
+let commands = 
+  "Pwd"
+  | "Cd"
+  | "Drop"
+  | "ProtectedLoop"
+  | "Quit"
+  | "Load"
+  | "Add"
+  | "Remove" space+ "Loadpath"
+  | "Print"
+  | "Inspect"
+  | "About"
+  | "Search"
+  | "Eval"
+  | "Reset"
+  | "Check"
+  | "Type"
+
+let extraction = 
+  "Extraction"
+  | "Recursive" space+ "Extraction" 
+  | "Extract"
+
+let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
+
+let gallina_kw_to_hide =
+  "Implicit"
+  | "Ltac"
+  | "Require"
+  | "Import"
+  | "Export"
+  | "Load" 
+  | "Hint"
+  | "Open"
+  | "Close"
+  | "Delimit"
+  | "Transparent"
+  | "Opaque"
+  | ("Declare" space+ ("Morphism" | "Step") )
+  | "Section"
+  | "Chapter"
+  | "Variable" 's'?
+  | ("Hypothesis" | "Hypotheses")
+  | "End"
+  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | "Declare" space+ ("Left" | "Right") space+ "Step" 
+
+
 (* tokens with balanced brackets *)
 let token_brackets =
   ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* 
@@ -241,21 +298,7 @@ let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
 let end_verb = "(*" space* "end" space+ "verb" space* "*)"
 *)
 
-let coq_command_to_hide =
-  "Implicit" space |
-  "Ltac" space | 
-  "Require" space | 
-  "Load" space |
-  "Hint" space |
-  "Transparent" space |
-  "Opaque" space |
-  ("Declare" space+ ("Morphism" | "Step") space) |
-  "Section" space | 
-  "Variable" 's'? space | 
-  ("Hypothesis" | "Hypotheses") space | 
-  "End" space |
-  ("Set" | "Unset") space+ "Printing" space+ "Coercions" space |
-  "Declare" space+ ("Left" | "Right") space+ "Step" space
+
 
 (*s Scanning Coq, at beginning of line *)
 
@@ -265,8 +308,8 @@ rule coq_bol = parse
   | space* "(**" space_nl
       { end_coq (); start_doc (); 
 	let eol = doc_bol lexbuf in
-	end_doc (); start_coq (); 
-	if eol then coq_bol lexbuf else coq lexbuf }
+	  end_doc (); start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | space* "Comments" space_nl
       { end_coq (); start_doc (); comments lexbuf; end_doc (); 
 	start_coq (); coq lexbuf }
@@ -276,28 +319,35 @@ rule coq_bol = parse
       { begin_show (); coq_bol lexbuf }
   | space* end_show
       { end_show (); coq_bol lexbuf }
-  | space* coq_command_to_hide
+  | space* gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	if !light && section_or_end s then begin 
-	  skip_to_dot lexbuf; 
-	  coq_bol lexbuf 
-	end else begin
-	  indentation (count_spaces s); 
-	  backtrack lexbuf; 
-	  coq lexbuf 
-	end }
+	  if !light && section_or_end s then begin 
+	    skip_to_dot lexbuf; 
+	    coq_bol lexbuf 
+	  end else begin
+	    indentation (count_spaces s); 
+	    ident s (lexeme_start lexbuf); 
+	    let eol= body lexbuf in 
+	      if eol then coq_bol lexbuf else coq lexbuf
+	  end }
+  | space* gallina_kw
+      { let s = lexeme lexbuf in 
+	  indentation (count_spaces s);
+	  ident s (lexeme_start lexbuf); 
+	  let eol= body lexbuf in
+	    if eol then coq_bol lexbuf else coq lexbuf }
   | space* "(**" space+ "printing" space+ (identifier | token) space+
       { let tok = lexeme lexbuf in
 	let s = printing_token lexbuf in
-	add_printing_token tok s;
-	coq_bol lexbuf }
+	  add_printing_token tok s;
+	  coq_bol lexbuf }
   | space* "(**" space+ "printing" space+
       { eprintf "warning: bad 'printing' command at character %d\n" 
 	  (lexeme_start lexbuf); flush stderr;
 	ignore (comment lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+ 
-    (identifier | token) space* "*)"
+      (identifier | token) space* "*)"
       { remove_printing_token (lexeme lexbuf);
 	coq_bol lexbuf }
   | space* "(**" space+ "remove" space+ "printing" space+
@@ -307,24 +357,28 @@ rule coq_bol = parse
 	coq_bol lexbuf }
   | space* "(*"
       { let eol = comment lexbuf in
-	if eol then coq_bol lexbuf else coq lexbuf }
-  | space+
-      { indentation (count_spaces (lexeme lexbuf)); coq lexbuf }
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | eof 
       { () }
-  | _ 
-      { backtrack lexbuf; indentation 0; coq lexbuf }
+  | _
+      { let eol = 
+	  if not !gallina then 
+	    begin backtrack lexbuf; indentation 0; body_bol lexbuf end 
+	  else 
+	    skip_to_dot lexbuf 
+	in
+	  if eol then coq_bol lexbuf else coq lexbuf }
 
 (*s Scanning Coq elsewhere *)
 
 and coq = parse
   | "\n" 
-      { line_break (); coq_bol lexbuf }
+      { line_break(); coq_bol lexbuf }
   | "(**" space_nl
       { end_coq (); start_doc (); 
 	let eol = doc_bol lexbuf in
-	end_doc (); start_coq (); 
-	if eol then coq_bol lexbuf else coq lexbuf }
+	  end_doc (); start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
   | "(*"
       { let eol = comment lexbuf in
 	  if eol then begin line_break(); coq_bol lexbuf end 
@@ -334,45 +388,44 @@ and coq = parse
       { if not !formatted then begin symbol (lexeme lexbuf); coq lexbuf end }
   | eof 
       { () }
-  | "let" { let s = lexeme lexbuf in
-	      glet:=true; ident s (lexeme_start lexbuf); coq lexbuf }
-  | token
+  | gallina_kw_to_hide
       { let s = lexeme lexbuf in
-	if !gallina then gallina_symbol s;
-	symbol s;
-	coq lexbuf }
-  | "with" space+ "Module" | "Module" space+ "Type" | "Declare" space+ "Module"
-    (* hack to avoid making Type a keyword *)
-      { let s = lexeme lexbuf in
-	if !gallina then gallina_id s;
-        ident s (lexeme_start lexbuf); coq lexbuf }
-  | "(" space* identifier space* ":=" 
-      { let id = extract_ident (lexeme lexbuf) in
-	symbol "("; ident id (lexeme_start lexbuf); symbol ":="; coq lexbuf }
-  | (identifier '.')* identifier
-      { let id = lexeme lexbuf in
-	if !gallina then gallina_id id;
-	ident id (lexeme_start lexbuf); coq lexbuf }
-  | _ 
-      { let c = lexeme_char lexbuf 0 in 
-	char c;
-	if !gallina && gallina_char c then skip_proof lexbuf;
-	coq lexbuf }
-
+	  if !light && section_or_end s then begin 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf 
+	  end else begin
+	    ident s (lexeme_start lexbuf); 
+	    let eol=body lexbuf in 
+	      if eol then coq_bol lexbuf else coq lexbuf
+	  end }
+  | gallina_kw
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); 
+	  let eol = body lexbuf in
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space+ { char ' '; coq lexbuf }
+  | _ { let eol = 
+	  if not !gallina then 
+	    begin backtrack lexbuf; indentation 0; body_bol lexbuf end 
+	  else 
+	    skip_to_dot lexbuf 
+	in 
+	  if eol then coq_bol lexbuf else coq lexbuf}
+      
 (*s Scanning documentation, at beginning of line *)
-
+      
 and doc_bol = parse
   | space* "\n" '\n'*
       { paragraph (); doc_bol lexbuf }
   | space* section [^')'] ([^'\n' '*'] | '*' [^'\n'')'])*
-      { let lev, s = sec_title (lexeme lexbuf) in 
-	section lev (fun () -> ignore (doc (from_string s))); 
-	doc lexbuf }
-  | space* '-'+
-      { let n = count_dashes (lexeme lexbuf) in
-	if n >= 4 then rule () else item n;
-	doc lexbuf }
-  | "<<" space*
+{ let lev, s = sec_title (lexeme lexbuf) in 
+    section lev (fun () -> ignore (doc (from_string s))); 
+    doc lexbuf }
+| space* '-'+
+     { let n = count_dashes (lexeme lexbuf) in
+	 if n >= 4 then rule () else item n;
+	 doc lexbuf }
+| "<<" space*
       { start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
   | eof 
       { false }
@@ -491,23 +544,30 @@ and comment = parse
   | eof  { false }
   | _    { comment lexbuf }
 
-(*s Skip proofs *)
-
-and skip_proof = parse
-  | "(*" { ignore (comment lexbuf); skip_proof lexbuf }
-  | "Save" | "Qed" | "Defined"
-  | "Abort" | "Proof" | "Admitted" { skip_to_dot lexbuf }
-  | "Proof" space* '.' { skip_proof lexbuf }
-  | identifier { skip_proof lexbuf } (* to avoid keywords within idents *)
-  | eof { () }
-  | _ { skip_proof lexbuf }
-
 and skip_to_dot = parse
-  | eof | '.' space { if !gallina then gstate := AfterDot }
-  | ".\n" { if !gallina then gstate := AfterDot; line_break(); }
+  | '.' space* '\n' { true }
+  | eof | '.' space+ { false}
   | "(*" { ignore (comment lexbuf); skip_to_dot lexbuf }
   | _ { skip_to_dot lexbuf }
 
+and body_bol = parse
+  | space+
+      { indentation (count_spaces (lexeme lexbuf)); body lexbuf }
+  | _ { backtrack lexbuf; body lexbuf }
+
+and body = parse
+  | '\n' {line_break(); body_bol lexbuf}
+  | eof { false }
+  | '.' space* '\n' { char '.'; line_break(); true }      
+  | '.' space+ { char '.'; char ' '; false }
+  | "(*" { let eol = comment lexbuf in 
+	     if eol then body_bol lexbuf else body lexbuf }
+  | identifier 
+      { let s = lexeme lexbuf in 
+	  ident s (lexeme_start lexbuf); body lexbuf }
+  | _ { let c = lexeme_char lexbuf 0 in 
+	  char c; body lexbuf }
+
 and skip_hide = parse
   | eof | end_hide { () }
   | _ { skip_hide lexbuf }
@@ -526,10 +586,6 @@ and printing_token = parse
 
 {
 
-  type file =
-    | Vernac_file of string * coq_module
-    | Latex_file of string
-
   let coq_file f m =
     reset ();
     Index.scan_file f m;
@@ -539,59 +595,5 @@ and printing_token = parse
     start_coq (); coq_bol lb; end_coq ();
     close_in c
 
-  (* LaTeX document *)
-
-  let latex_document l = 
-    let file = function
-      | Vernac_file (f,m) -> set_module m; coq_file f m
-      | Latex_file f -> dump_file f
-    in
-    header ();
-    if !toc then make_toc ();
-    List.iter file l;
-    trailer ();
-    close ()
-
-  (* HTML document *)      
-
-  let html_document l =
-    let file = function
-      | Vernac_file (f,m) -> 
-	  set_module m;
-	  let hf = m ^ ".html" in
-	  set_out_file hf;
-	  header ();
-	  coq_file f m;
-	  trailer ();
-	  close ()
-      | Latex_file _ -> ()
-    in
-    List.iter file l;
-    make_index ();
-    if !toc then make_toc ()
-
-  (* TeXmacs document *)
-
-  let texmacs_document l = 
-    let file = function
-      | Vernac_file (f,m) -> set_module m; coq_file f m
-      | Latex_file f -> dump_file f
-    in
-    header ();
-    List.iter file l;
-    trailer ();
-    close ()
-
-  let index_module = function
-    | Vernac_file (_,m) -> Index.add_module m
-    | Latex_file _ -> ()
-
-  let produce_document l =
-    List.iter index_module l;
-    (match !target_language with
-       | LaTeX -> latex_document 
-       | HTML -> html_document
-       | TeXmacs -> texmacs_document) l
-
 }