From e0bd95f7c3e0304506d62a900ae26c58ec3d4f38 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 24 Mar 2009 17:46:31 +0000
Subject: pretty.mll of coqdoc becomes cpretty.mll (avoid clash with a camlp5
 file)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12011 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.common          |   2 +-
 tools/coqdoc/cpretty.mli |  13 +
 tools/coqdoc/cpretty.mll | 773 +++++++++++++++++++++++++++++++++++++++++++++++
 tools/coqdoc/main.ml     |   4 +-
 tools/coqdoc/pretty.mli  |  13 -
 tools/coqdoc/pretty.mll  | 773 -----------------------------------------------
 6 files changed, 789 insertions(+), 789 deletions(-)
 create mode 100644 tools/coqdoc/cpretty.mli
 create mode 100644 tools/coqdoc/cpretty.mll
 delete mode 100644 tools/coqdoc/pretty.mli
 delete mode 100644 tools/coqdoc/pretty.mll

diff --git a/Makefile.common b/Makefile.common
index 461c1c78f6..8a258fb8cc 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -263,7 +263,7 @@ GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
 GALLINACMX:=$(GALLINACMO:.cmo=.cmx)
 
 COQDOCCMO:=$(CONFIG) $(addprefix tools/coqdoc/, \
-  cdglobals.cmo alpha.cmo index.cmo output.cmo pretty.cmo main.cmo )
+  cdglobals.cmo alpha.cmo index.cmo output.cmo cpretty.cmo main.cmo )
 COQDOCCMX:=$(COQDOCCMO:.cmo=.cmx)
 
 # grammar modules with camlp4
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
new file mode 100644
index 0000000000..f02a79be50
--- /dev/null
+++ b/tools/coqdoc/cpretty.mli
@@ -0,0 +1,13 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Index
+
+val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
new file mode 100644
index 0000000000..1420c9a924
--- /dev/null
+++ b/tools/coqdoc/cpretty.mll
@@ -0,0 +1,773 @@
+(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+(*s Utility functions for the scanners *)
+
+{
+  open Printf
+  open Lexing 
+
+  (* count the number of spaces at the beginning of a string *)
+  let count_spaces s =
+    let n = String.length s in
+    let rec count c i = 
+      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,i
+    in
+      count 0 0
+
+  let count_dashes s =
+    let c = ref 0 in
+    for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
+    !c
+
+  let cut_head_tail_spaces s =
+    let n = String.length s in
+    let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
+    let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
+    let l = look_up 0 in
+    let r = look_dn (n-1) in
+    if l <= r then String.sub s l (r-l+1) else s
+
+  let sec_title s =
+    let rec count lev i = 
+      if s.[i] = '*' then 
+	count (succ lev) (succ i) 
+      else 
+	let t = String.sub s i (String.length s - i) in
+	lev, cut_head_tail_spaces t
+    in
+    count 0 (String.index s '*')
+
+  let strip_eol s =
+    let eol = s.[String.length s - 1] = '\n' in
+    (eol, if eol then String.sub s 1 (String.length s - 1) else s)
+
+
+  let formatted = ref false
+  let brackets = ref 0
+  let comment_level = ref 0
+  let in_proof = ref None
+
+  let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
+
+  let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
+
+  (* saving/restoring the PP state *)
+
+  type state = {
+    st_gallina : bool;
+    st_light : bool
+  }
+
+  let state_stack = Stack.create ()
+
+  let save_state () = 
+    Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
+
+  let restore_state () =
+    let s = Stack.pop state_stack in
+    Cdglobals.gallina := s.st_gallina;
+    Cdglobals.light := s.st_light
+      
+  let without_ref r f x = save_state (); r := false; f x; restore_state ()
+
+  let without_gallina = without_ref Cdglobals.gallina
+
+  let without_light = without_ref Cdglobals.light
+
+  let show_all f = without_gallina (without_light f)
+
+  let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
+  let end_show () = restore_state ()
+
+  (* Reset the globals *)
+
+  let reset () =
+    formatted := false;
+    brackets := 0;
+    comment_level := 0
+
+  (* erasing of Section/End *)
+
+  let section_re = Str.regexp "[ \t]*Section"
+  let end_re = Str.regexp "[ \t]*End"
+  let is_section s = Str.string_match section_re s 0
+  let is_end s = Str.string_match end_re s 0
+
+  let sections_to_close = ref 0
+
+  let section_or_end s =
+    if is_section s then begin
+      incr sections_to_close; true
+    end else if is_end s then begin
+      if !sections_to_close > 0 then begin 
+	decr sections_to_close; true 
+      end else 
+	false
+    end else
+      true
+
+  (* tokens pretty-print *)
+
+  let token_buffer = Buffer.create 1024
+
+  let token_re = 
+    Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
+  let printing_token_re =
+    Str.regexp
+      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
+
+  let add_printing_token toks pps =
+    try
+      if Str.string_match token_re toks 0 then
+	let tok = Str.matched_group 1 toks in
+	if Str.string_match printing_token_re pps 0 then
+	  let pp = 
+	    (try Some (Str.matched_group 3 pps) with _ -> 
+             try Some (Str.matched_group 4 pps) with _ -> None),
+	    (try Some (Str.matched_group 6 pps) with _ -> None)
+	  in
+	  Output.add_printing_token tok pp
+    with _ ->
+      ()
+
+  let remove_token_re = 
+    Str.regexp 
+      "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
+
+  let remove_printing_token toks =
+    try
+      if Str.string_match remove_token_re toks 0 then
+	let tok = Str.matched_group 1 toks in
+	Output.remove_printing_token tok
+    with _ ->
+      ()
+
+  let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
+  let extract_ident s =
+    assert (String.length s >= 3);
+    if Str.string_match extract_ident_re s 0 then
+      Str.matched_group 1 s
+    else
+      String.sub s 1 (String.length s - 3)
+
+  let symbol lexbuf s = Output.symbol s 
+
+}
+
+(*s Regular expressions *)
+
+let space = [' ' '\t']
+let space_nl = [' ' '\t' '\n' '\r']
+let nl = "\r\n" | '\n'
+
+let firstchar = 
+  ['A'-'Z' 'a'-'z' '_' 
+  (* iso 8859-1 accents *) 
+  '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  (* *)
+  '\194' '\185' |
+  (* utf-8 latin 1 supplement *) 
+  '\195' ['\128'-'\191'] |
+  (* utf-8 letterlike symbols *) 
+  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
+  '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
+    | '\129' [ '\176'-'\187' ] (* superscripts *)
+    | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
+let identchar = 
+  firstchar | ['\'' '0'-'9' '@' ]
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let identifier = 
+  id | pfx_id id
+
+let symbolchar_symbol_no_brackets =
+  ['!' '$' '%' '&' '*' '+' ',' '^' '#'
+      '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
+  (* utf-8 symbols *) 
+  '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
+let symbolchar_no_brackets = symbolchar_symbol_no_brackets | 
+    [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
+let symbolchar = symbolchar_no_brackets | '[' | ']'
+let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
+let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
+let printing_token = (token | id)+
+
+(* tokens with balanced brackets *)
+let token_brackets =
+  ( token_no_brackets ('[' token_no_brackets? ']')* 
+  | token_no_brackets? ('[' token_no_brackets? ']')+ )
+  token_no_brackets?
+
+let thm_token = 
+  "Theorem" 
+  | "Lemma" 
+  | "Fact" 
+  | "Remark" 
+  | "Corollary" 
+  | "Proposition" 
+  | "Property"
+  | "Goal"
+
+let prf_token =
+  "Next" space+ "Obligation"
+  | "Proof" (space* "." | space+ "with")
+
+let def_token = 
+  "Definition" 
+  | "Let" 
+  | "Class"
+  | "SubClass"
+  | "Example"
+  | "Local" 
+  | "Fixpoint" 
+  | "Boxed" 
+  | "CoFixpoint" 
+  | "Record" 
+  | "Structure" 
+  | "Scheme"
+  | "Inductive"
+  | "CoInductive"
+  | "Equations"
+  | "Instance"
+  | "Global" space+ "Instance"
+
+let decl_token = 
+  "Hypothesis" 
+  | "Hypotheses" 
+  | "Parameter" 
+  | "Axiom" 's'? 
+  | "Conjecture"
+
+let gallina_ext =
+  "Module" 
+  | "Include" space+ "Type"
+  | "Include"
+  | "Declare" space+ "Module"
+  | "Transparent"
+  | "Opaque"
+  | "Canonical"
+  | "Coercion"
+  | "Identity"
+  | "Implicit"
+  | "Notation"
+  | "Infix"
+  | "Tactic" space+ "Notation"
+  | "Reserved" space+ "Notation"
+  | "Section"
+  | "Context"
+  | "Variable" 's'?
+  | ("Hypothesis" | "Hypotheses")
+  | "End"
+
+let commands = 
+  "Pwd"
+  | "Cd"
+  | "Drop"
+  | "ProtectedLoop"
+  | "Quit"
+  | "Load"
+  | "Add"
+  | "Remove" space+ "Loadpath"
+  | "Print"
+  | "Inspect"
+  | "About"
+  | "Search"
+  | "Eval"
+  | "Reset"
+  | "Check"
+  | "Type"
+
+  | "Section"
+  | "Chapter"
+  | "Variable" 's'?
+  | ("Hypothesis" | "Hypotheses")
+  | "End"
+
+let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
+
+let extraction = 
+  "Extraction"
+  | "Recursive" space+ "Extraction" 
+  | "Extract"
+
+let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
+
+let prog_kw =
+  "Program" space+ gallina_kw
+  | "Obligation"
+  | "Obligations"
+  | "Solve"
+
+let gallina_kw_to_hide =
+    "Implicit" space+ "Arguments"
+  | "Ltac"
+  | "Require"
+  | "Import"
+  | "Export"
+  | "Load" 
+  | "Hint"
+  | "Open"
+  | "Close"
+  | "Delimit"
+  | "Transparent"
+  | "Opaque"
+  | ("Declare" space+ ("Morphism" | "Step") )
+  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
+  | "Declare" space+ ("Left" | "Right") space+ "Step" 
+
+
+let section = "*" | "**" | "***" | "****"
+
+let item_space = "    "
+
+let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
+let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
+let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
+let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
+(*
+let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
+let end_verb = "(*" space* "end" space+ "verb" space* "*)"
+*)
+
+
+
+(*s Scanning Coq, at beginning of line *)
+
+rule coq_bol = parse
+  | space* nl+
+      { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
+  | space* "(**" space_nl
+      { Output.end_coq (); Output.start_doc (); 
+	let eol = doc_bol lexbuf in
+	  Output.end_doc (); Output.start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
+  | space* "Comments" space_nl
+      { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); 
+	Output.start_coq (); coq lexbuf }
+  | space* begin_hide
+      { skip_hide lexbuf; coq_bol lexbuf }
+  | space* begin_show
+      { begin_show (); coq_bol lexbuf }
+  | space* end_show
+      { end_show (); coq_bol lexbuf }
+  | space* gallina_kw_to_hide
+      { let s = lexeme lexbuf in
+	  if !Cdglobals.light && section_or_end s then 
+	    let eol = skip_to_dot lexbuf in
+	      if eol then (coq_bol lexbuf) else coq lexbuf
+	  else 
+	    begin
+	      let nbsp,isp = count_spaces s in
+		Output.indentation nbsp; 
+		let s = String.sub s isp (String.length s - isp) in
+		  Output.ident s (lexeme_start lexbuf + isp); 
+		  let eol = body lexbuf in 
+		    if eol then coq_bol lexbuf else coq lexbuf
+	    end }
+  | space* thm_token
+      { let s = lexeme lexbuf in 
+	let nbsp,isp = count_spaces s in
+	let s = String.sub s isp (String.length s - isp)  in
+	  Output.indentation nbsp;
+	  Output.ident s (lexeme_start lexbuf + isp); 
+	  let eol = body lexbuf in
+	    in_proof := Some eol;
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space* prf_token
+      { in_proof := Some true;
+	let eol = 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; body_bol lexbuf end 
+	  else 
+	    let s = lexeme lexbuf in
+	      if s.[String.length s - 1] = '.' then false
+	      else skip_to_dot lexbuf
+	in if eol then coq_bol lexbuf else coq lexbuf }
+  | space* end_kw { 
+      let eol = 
+	if not (!in_proof <> None && !Cdglobals.gallina) then 
+	  begin backtrack lexbuf; body_bol lexbuf end 
+	else skip_to_dot lexbuf
+      in
+	in_proof := None;
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | space* gallina_kw
+      { 
+	in_proof := None;
+	let s = lexeme lexbuf in 
+	let nbsp,isp = count_spaces s in
+	let s = String.sub s isp (String.length s - isp)  in
+	  Output.indentation nbsp;
+	  Output.ident s (lexeme_start lexbuf + isp); 
+	  let eol= body lexbuf in
+	    if eol then coq_bol lexbuf else coq lexbuf }
+  | space* prog_kw
+      { 
+	in_proof := None;
+	let s = lexeme lexbuf in 
+	let nbsp,isp = count_spaces s in
+	  Output.indentation nbsp;
+	  let s = String.sub s isp (String.length s - isp)  in
+	    Output.ident s (lexeme_start lexbuf + isp); 
+	    let eol= body lexbuf in
+	      if eol then coq_bol lexbuf else coq lexbuf }
+
+  | space* "(**" space+ "printing" space+ printing_token space+
+      { let tok = lexeme lexbuf in
+	let s = printing_token_body lexbuf in
+	  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;
+	comment_level := 1;
+	ignore (comment lexbuf);
+	coq_bol lexbuf }
+  | space* "(**" space+ "remove" space+ "printing" space+ 
+      (identifier | token) space* "*)"
+      { remove_printing_token (lexeme lexbuf);
+	coq_bol lexbuf }
+  | space* "(**" space+ "remove" space+ "printing" space+
+      { eprintf "warning: bad 'remove printing' command at character %d\n" 
+	  (lexeme_start lexbuf); flush stderr;
+	comment_level := 1;
+	ignore (comment lexbuf);
+	coq_bol lexbuf }
+  | space* "(*"
+      { comment_level := 1; 
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
+	let eol = comment lexbuf in
+	  if eol then coq_bol lexbuf else coq lexbuf }
+  | eof 
+      { () }
+  | _
+      { let eol = 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; 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
+  | nl 
+      { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
+  | "(**" space_nl
+      { Output.end_coq (); Output.start_doc (); 
+	let eol = doc_bol lexbuf in
+	  Output.end_doc (); Output.start_coq (); 
+	  if eol then coq_bol lexbuf else coq lexbuf }
+  | "(*"
+      { comment_level := 1;
+	if !Cdglobals.parse_comments then begin
+	  let s = lexeme lexbuf in 
+	  let nbsp,isp = count_spaces s in
+	    Output.indentation nbsp;
+	    Output.start_comment ();
+	end;
+	let eol = comment lexbuf in
+	  if eol then coq_bol lexbuf
+          else coq lexbuf
+      }
+  | nl+ space* "]]"
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
+  | eof 
+      { () }
+  | gallina_kw_to_hide
+      { let s = lexeme lexbuf in
+	  if !Cdglobals.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
+	      Output.ident s (lexeme_start lexbuf); 
+	      let eol=body lexbuf in 
+		if eol then coq_bol lexbuf else coq lexbuf
+	    end }
+  | prf_token
+      { let eol = 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; body_bol lexbuf end 
+	  else 
+	    let s = lexeme lexbuf in
+	    let eol = 
+	      if s.[String.length s - 1] = '.' then false
+	      else skip_to_dot lexbuf
+	    in
+	      eol
+	in if eol then coq_bol lexbuf else coq lexbuf }
+  | end_kw { 
+      let eol = 
+	if not !Cdglobals.gallina then 
+	  begin backtrack lexbuf; body lexbuf end 
+	else 
+	  let eol = skip_to_dot lexbuf in
+	    if !in_proof <> Some true && eol then 
+	      Output.line_break ();
+	    eol
+      in
+	in_proof := None;
+	if eol then coq_bol lexbuf else coq lexbuf }
+  | gallina_kw
+      { let s = lexeme lexbuf in 
+	  Output.ident s (lexeme_start lexbuf); 
+	let eol = body lexbuf in
+	  if eol then coq_bol lexbuf else coq lexbuf }
+  | prog_kw
+      { let s = lexeme lexbuf in 
+	  Output.ident s (lexeme_start lexbuf); 
+	let eol = body lexbuf in
+	  if eol then coq_bol lexbuf else coq lexbuf }
+  | space+ { Output.char ' '; coq lexbuf }
+  | eof 
+      { () }
+  | _ {	let eol = 
+	  if not !Cdglobals.gallina then 
+	    begin backtrack lexbuf; body 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* nl+
+      { Output.paragraph (); doc_bol lexbuf }
+  | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
+      { let eol, lex = strip_eol (lexeme lexbuf) in
+        let lev, s = sec_title lex in
+          Output.section lev (fun () -> ignore (doc (from_string s)));
+	  if eol then doc_bol lexbuf else doc lexbuf }
+  | space* '-'+
+      { let n = count_dashes (lexeme lexbuf) in
+	if n >= 4 then Output.rule () else Output.item n;
+        doc lexbuf }
+  | "<<" space*
+      { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
+  | eof 
+      { true }
+  | _ 
+      { backtrack lexbuf; doc lexbuf }
+
+(*s Scanning documentation elsewhere *)
+
+and doc = parse
+  | nl
+      { Output.char '\n'; doc_bol lexbuf }
+  | "[[" nl
+      { formatted := true; Output.line_break (); Output.start_inline_coq ();
+	let eol = body_bol lexbuf in 
+	  Output.end_inline_coq (); formatted := false;
+	  if eol then doc_bol lexbuf else doc lexbuf}
+  | "["
+      { brackets := 1; 
+	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
+	doc lexbuf }
+  | '*'* "*)" space* nl
+      { true }
+  | '*'* "*)"
+      { false }
+  | "$"
+      { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
+  | "$$"
+      { Output.char '$'; doc lexbuf }
+  | "%"
+      { escaped_latex lexbuf; doc lexbuf }
+  | "%%"
+      { Output.char '%'; doc lexbuf }
+  | "#"
+      { escaped_html lexbuf; doc lexbuf }
+  | "##"
+      { Output.char '#'; doc lexbuf }
+  | eof 
+      { false }
+  | _ 
+      { Output.char (lexeme_char lexbuf 0); doc lexbuf }
+
+(*s Various escapings *)
+
+and escaped_math_latex = parse
+  | "$" { Output.stop_latex_math () }
+  | eof { Output.stop_latex_math () }
+  | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
+
+and escaped_latex = parse
+  | "%" { () }
+  | eof { () }
+  | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
+
+and escaped_html = parse
+  | "#" { () }
+  | "&#"
+        { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
+  | "##"
+        { Output.html_char '#'; escaped_html lexbuf }
+  | eof { () }
+  | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
+
+and verbatim = parse
+  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
+  | eof { Output.stop_verbatim () }
+  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
+
+(*s Coq, inside quotations *)
+
+and escaped_coq = parse
+  | "]"
+      { decr brackets; 
+	if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
+  | "["
+      { incr brackets; Output.char '['; escaped_coq lexbuf }
+  | "(*"
+      { comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
+  | "*)"
+      { (* likely to be a syntax error: we escape *) backtrack lexbuf }
+  | eof
+      { () }
+  | token_brackets
+      { let s = lexeme lexbuf in
+	  symbol lexbuf s; escaped_coq lexbuf }
+  | (identifier '.')* identifier
+      { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
+  | _ 
+      { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
+
+(*s Coq "Comments" command. *)
+
+and comments = parse
+  | space_nl+ 
+      { Output.char ' '; comments lexbuf }
+  | '"' [^ '"']* '"' 
+      { let s = lexeme lexbuf in
+	let s = String.sub s 1 (String.length s - 2) in
+	ignore (doc (from_string s)); comments lexbuf }
+  | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
+      { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
+  | "." (space_nl | eof)
+      { () }
+  | eof 
+      { () }
+  | _   
+      { Output.char (lexeme_char lexbuf 0); comments lexbuf }
+
+(*s Skip comments *)
+
+and comment = parse
+  | "(*" { incr comment_level; comment lexbuf }
+  | "*)" space* nl { 
+      if !Cdglobals.parse_comments then
+	(Output.end_comment (); Output.line_break ());
+      decr comment_level; if !comment_level > 0 then comment lexbuf else true }
+  | "*)" { 
+      if !Cdglobals.parse_comments then (Output.end_comment ());
+      decr comment_level; if !comment_level > 0 then comment lexbuf else false }
+  | eof  { false }
+  | space+ { if !Cdglobals.parse_comments then 
+	Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
+  | nl   { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
+  | _    { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
+  comment lexbuf }
+      
+and skip_to_dot = parse
+  | '.' space* nl { true }
+  | eof | '.' space+ { false}
+  | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
+  | _ { skip_to_dot lexbuf }
+
+and body_bol = parse
+  | space+
+      { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
+  | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
+
+and body = parse
+  | nl {Output.line_break(); body_bol lexbuf}
+  | nl+ space* "]]"
+      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
+  | eof { false }
+  | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
+  | '.' space+ { Output.char '.'; Output.char ' '; false }
+  | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
+  | "(*" { comment_level := 1; 
+	   if !Cdglobals.parse_comments then Output.start_comment ();
+	   let eol = comment lexbuf in 
+	     if !Cdglobals.parse_comments then Output.end_comment ();
+	     if eol 
+	     then begin Output.line_break(); body_bol lexbuf end
+	     else body lexbuf }
+  | identifier 
+      { let s = lexeme lexbuf in 
+	  Output.ident s (lexeme_start lexbuf); 
+	  body lexbuf }
+  | token_no_brackets
+      { let s = lexeme lexbuf in
+	  symbol lexbuf s; body lexbuf }
+  | _ { let c = lexeme_char lexbuf 0 in 
+	  Output.char c; 
+          body lexbuf }
+
+and notation_bol = parse
+  | space+
+      { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
+  | _ { backtrack lexbuf; notation lexbuf }
+
+and notation = parse
+  | nl { Output.line_break(); notation_bol lexbuf }
+  | '"' { Output.char '"'}
+  | token
+      { let s = lexeme lexbuf in
+	  symbol lexbuf s; notation lexbuf }
+  | _ { let c = lexeme_char lexbuf 0 in 
+	  Output.char c; 
+          notation lexbuf }
+
+and skip_hide = parse
+  | eof | end_hide { () }
+  | _ { skip_hide lexbuf }
+
+(*s Reading token pretty-print *)
+
+and printing_token_body = parse
+  | "*)" nl? | eof 
+	{ let s = Buffer.contents token_buffer in 
+	  Buffer.clear token_buffer;
+	  s }
+  | _   { Buffer.add_string token_buffer (lexeme lexbuf); 
+	  printing_token_body lexbuf }
+
+(*s Applying the scanners to files *)
+
+{
+
+  let coq_file f m =
+    reset ();
+    Index.current_library := m;
+    Output.start_module ();
+    let c = open_in f in
+    let lb = from_channel c in
+    Output.start_coq (); coq_bol lb; Output.end_coq ();
+    close_in c
+
+}
+
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 24538360a2..bbfd93fd44 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -383,7 +383,7 @@ let copy src dst =
 let gen_one_file l =
   let file = function
     | Vernac_file (f,m) -> 
-	Output.set_module m; Pretty.coq_file f m
+	Output.set_module m; Cpretty.coq_file f m
     | Latex_file _ -> ()
   in
     if (!header_trailer) then Output.header ();
@@ -399,7 +399,7 @@ let gen_mult_files l =
 	let hf = target_full_name m in
 	  open_out_file hf;
 	  if (!header_trailer) then Output.header (); 
-	  Pretty.coq_file f m; 
+	  Cpretty.coq_file f m; 
 	  if (!header_trailer) then Output.trailer ();
 	  close_out_file()
     | Latex_file _ -> ()
diff --git a/tools/coqdoc/pretty.mli b/tools/coqdoc/pretty.mli
deleted file mode 100644
index f02a79be50..0000000000
--- a/tools/coqdoc/pretty.mli
+++ /dev/null
@@ -1,13 +0,0 @@
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-open Index
-
-val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
deleted file mode 100644
index 1420c9a924..0000000000
--- a/tools/coqdoc/pretty.mll
+++ /dev/null
@@ -1,773 +0,0 @@
-(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
-(************************************************************************)
-(*  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        *)
-(************************************************************************)
-
-(*i $Id$ i*)
-
-(*s Utility functions for the scanners *)
-
-{
-  open Printf
-  open Lexing 
-
-  (* count the number of spaces at the beginning of a string *)
-  let count_spaces s =
-    let n = String.length s in
-    let rec count c i = 
-      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,i
-    in
-      count 0 0
-
-  let count_dashes s =
-    let c = ref 0 in
-    for i = 0 to String.length s - 1 do if s.[i] = '-' then incr c done;
-    !c
-
-  let cut_head_tail_spaces s =
-    let n = String.length s in
-    let rec look_up i = if i == n || s.[i] <> ' ' then i else look_up (i+1) in
-    let rec look_dn i = if i == -1 || s.[i] <> ' ' then i else look_dn (i-1) in
-    let l = look_up 0 in
-    let r = look_dn (n-1) in
-    if l <= r then String.sub s l (r-l+1) else s
-
-  let sec_title s =
-    let rec count lev i = 
-      if s.[i] = '*' then 
-	count (succ lev) (succ i) 
-      else 
-	let t = String.sub s i (String.length s - i) in
-	lev, cut_head_tail_spaces t
-    in
-    count 0 (String.index s '*')
-
-  let strip_eol s =
-    let eol = s.[String.length s - 1] = '\n' in
-    (eol, if eol then String.sub s 1 (String.length s - 1) else s)
-
-
-  let formatted = ref false
-  let brackets = ref 0
-  let comment_level = ref 0
-  let in_proof = ref None
-
-  let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos
-
-  let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
-
-  (* saving/restoring the PP state *)
-
-  type state = {
-    st_gallina : bool;
-    st_light : bool
-  }
-
-  let state_stack = Stack.create ()
-
-  let save_state () = 
-    Stack.push { st_gallina = !Cdglobals.gallina; st_light = !Cdglobals.light } state_stack
-
-  let restore_state () =
-    let s = Stack.pop state_stack in
-    Cdglobals.gallina := s.st_gallina;
-    Cdglobals.light := s.st_light
-      
-  let without_ref r f x = save_state (); r := false; f x; restore_state ()
-
-  let without_gallina = without_ref Cdglobals.gallina
-
-  let without_light = without_ref Cdglobals.light
-
-  let show_all f = without_gallina (without_light f)
-
-  let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
-  let end_show () = restore_state ()
-
-  (* Reset the globals *)
-
-  let reset () =
-    formatted := false;
-    brackets := 0;
-    comment_level := 0
-
-  (* erasing of Section/End *)
-
-  let section_re = Str.regexp "[ \t]*Section"
-  let end_re = Str.regexp "[ \t]*End"
-  let is_section s = Str.string_match section_re s 0
-  let is_end s = Str.string_match end_re s 0
-
-  let sections_to_close = ref 0
-
-  let section_or_end s =
-    if is_section s then begin
-      incr sections_to_close; true
-    end else if is_end s then begin
-      if !sections_to_close > 0 then begin 
-	decr sections_to_close; true 
-      end else 
-	false
-    end else
-      true
-
-  (* tokens pretty-print *)
-
-  let token_buffer = Buffer.create 1024
-
-  let token_re = 
-    Str.regexp "[ \t]*(\\*\\*[ \t]+printing[ \t]+\\([^ \t]+\\)"
-  let printing_token_re =
-    Str.regexp
-      "[ \t]*\\(\\(%\\([^%]*\\)%\\)\\|\\(\\$[^$]*\\$\\)\\)?[ \t]*\\(#\\(\\([^#]\\|&#\\)*\\)#\\)?"
-
-  let add_printing_token toks pps =
-    try
-      if Str.string_match token_re toks 0 then
-	let tok = Str.matched_group 1 toks in
-	if Str.string_match printing_token_re pps 0 then
-	  let pp = 
-	    (try Some (Str.matched_group 3 pps) with _ -> 
-             try Some (Str.matched_group 4 pps) with _ -> None),
-	    (try Some (Str.matched_group 6 pps) with _ -> None)
-	  in
-	  Output.add_printing_token tok pp
-    with _ ->
-      ()
-
-  let remove_token_re = 
-    Str.regexp 
-      "[ \t]*(\\*\\*[ \t]+remove[ \t]+printing[ \t]+\\([^ \t]+\\)[ \t]*\\*)"
-
-  let remove_printing_token toks =
-    try
-      if Str.string_match remove_token_re toks 0 then
-	let tok = Str.matched_group 1 toks in
-	Output.remove_printing_token tok
-    with _ ->
-      ()
-
-  let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
-  let extract_ident s =
-    assert (String.length s >= 3);
-    if Str.string_match extract_ident_re s 0 then
-      Str.matched_group 1 s
-    else
-      String.sub s 1 (String.length s - 3)
-
-  let symbol lexbuf s = Output.symbol s 
-
-}
-
-(*s Regular expressions *)
-
-let space = [' ' '\t']
-let space_nl = [' ' '\t' '\n' '\r']
-let nl = "\r\n" | '\n'
-
-let firstchar = 
-  ['A'-'Z' 'a'-'z' '_' 
-  (* iso 8859-1 accents *) 
-  '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
-  (* *)
-  '\194' '\185' |
-  (* utf-8 latin 1 supplement *) 
-  '\195' ['\128'-'\191'] |
-  (* utf-8 letterlike symbols *) 
-  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
-  '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
-    | '\129' [ '\176'-'\187' ] (* superscripts *)
-    | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
-let identchar = 
-  firstchar | ['\'' '0'-'9' '@' ]
-let id = firstchar identchar*
-let pfx_id = (id '.')*
-let identifier = 
-  id | pfx_id id
-
-let symbolchar_symbol_no_brackets =
-  ['!' '$' '%' '&' '*' '+' ',' '^' '#'
-      '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
-  (* utf-8 symbols *) 
-  '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
-let symbolchar_no_brackets = symbolchar_symbol_no_brackets | 
-    [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
-let symbolchar = symbolchar_no_brackets | '[' | ']'
-let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
-let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
-let printing_token = (token | id)+
-
-(* tokens with balanced brackets *)
-let token_brackets =
-  ( token_no_brackets ('[' token_no_brackets? ']')* 
-  | token_no_brackets? ('[' token_no_brackets? ']')+ )
-  token_no_brackets?
-
-let thm_token = 
-  "Theorem" 
-  | "Lemma" 
-  | "Fact" 
-  | "Remark" 
-  | "Corollary" 
-  | "Proposition" 
-  | "Property"
-  | "Goal"
-
-let prf_token =
-  "Next" space+ "Obligation"
-  | "Proof" (space* "." | space+ "with")
-
-let def_token = 
-  "Definition" 
-  | "Let" 
-  | "Class"
-  | "SubClass"
-  | "Example"
-  | "Local" 
-  | "Fixpoint" 
-  | "Boxed" 
-  | "CoFixpoint" 
-  | "Record" 
-  | "Structure" 
-  | "Scheme"
-  | "Inductive"
-  | "CoInductive"
-  | "Equations"
-  | "Instance"
-  | "Global" space+ "Instance"
-
-let decl_token = 
-  "Hypothesis" 
-  | "Hypotheses" 
-  | "Parameter" 
-  | "Axiom" 's'? 
-  | "Conjecture"
-
-let gallina_ext =
-  "Module" 
-  | "Include" space+ "Type"
-  | "Include"
-  | "Declare" space+ "Module"
-  | "Transparent"
-  | "Opaque"
-  | "Canonical"
-  | "Coercion"
-  | "Identity"
-  | "Implicit"
-  | "Notation"
-  | "Infix"
-  | "Tactic" space+ "Notation"
-  | "Reserved" space+ "Notation"
-  | "Section"
-  | "Context"
-  | "Variable" 's'?
-  | ("Hypothesis" | "Hypotheses")
-  | "End"
-
-let commands = 
-  "Pwd"
-  | "Cd"
-  | "Drop"
-  | "ProtectedLoop"
-  | "Quit"
-  | "Load"
-  | "Add"
-  | "Remove" space+ "Loadpath"
-  | "Print"
-  | "Inspect"
-  | "About"
-  | "Search"
-  | "Eval"
-  | "Reset"
-  | "Check"
-  | "Type"
-
-  | "Section"
-  | "Chapter"
-  | "Variable" 's'?
-  | ("Hypothesis" | "Hypotheses")
-  | "End"
-
-let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort"
-
-let extraction = 
-  "Extraction"
-  | "Recursive" space+ "Extraction" 
-  | "Extract"
-
-let gallina_kw = thm_token | def_token | decl_token | gallina_ext | commands | extraction
-
-let prog_kw =
-  "Program" space+ gallina_kw
-  | "Obligation"
-  | "Obligations"
-  | "Solve"
-
-let gallina_kw_to_hide =
-    "Implicit" space+ "Arguments"
-  | "Ltac"
-  | "Require"
-  | "Import"
-  | "Export"
-  | "Load" 
-  | "Hint"
-  | "Open"
-  | "Close"
-  | "Delimit"
-  | "Transparent"
-  | "Opaque"
-  | ("Declare" space+ ("Morphism" | "Step") )
-  | ("Set" | "Unset") space+ "Printing" space+ "Coercions"
-  | "Declare" space+ ("Left" | "Right") space+ "Step" 
-
-
-let section = "*" | "**" | "***" | "****"
-
-let item_space = "    "
-
-let begin_hide = "(*" space* "begin" space+ "hide" space* "*)" space* nl
-let end_hide = "(*" space* "end" space+ "hide" space* "*)" space* nl
-let begin_show = "(*" space* "begin" space+ "show" space* "*)" space* nl
-let end_show = "(*" space* "end" space+ "show" space* "*)" space* nl
-(*
-let begin_verb = "(*" space* "begin" space+ "verb" space* "*)"
-let end_verb = "(*" space* "end" space+ "verb" space* "*)"
-*)
-
-
-
-(*s Scanning Coq, at beginning of line *)
-
-rule coq_bol = parse
-  | space* nl+
-      { if not (!in_proof <> None && (!Cdglobals.gallina || !Cdglobals.light)) then Output.empty_line_of_code (); coq_bol lexbuf }
-  | space* "(**" space_nl
-      { Output.end_coq (); Output.start_doc (); 
-	let eol = doc_bol lexbuf in
-	  Output.end_doc (); Output.start_coq (); 
-	  if eol then coq_bol lexbuf else coq lexbuf }
-  | space* "Comments" space_nl
-      { Output.end_coq (); Output.start_doc (); comments lexbuf; Output.end_doc (); 
-	Output.start_coq (); coq lexbuf }
-  | space* begin_hide
-      { skip_hide lexbuf; coq_bol lexbuf }
-  | space* begin_show
-      { begin_show (); coq_bol lexbuf }
-  | space* end_show
-      { end_show (); coq_bol lexbuf }
-  | space* gallina_kw_to_hide
-      { let s = lexeme lexbuf in
-	  if !Cdglobals.light && section_or_end s then 
-	    let eol = skip_to_dot lexbuf in
-	      if eol then (coq_bol lexbuf) else coq lexbuf
-	  else 
-	    begin
-	      let nbsp,isp = count_spaces s in
-		Output.indentation nbsp; 
-		let s = String.sub s isp (String.length s - isp) in
-		  Output.ident s (lexeme_start lexbuf + isp); 
-		  let eol = body lexbuf in 
-		    if eol then coq_bol lexbuf else coq lexbuf
-	    end }
-  | space* thm_token
-      { let s = lexeme lexbuf in 
-	let nbsp,isp = count_spaces s in
-	let s = String.sub s isp (String.length s - isp)  in
-	  Output.indentation nbsp;
-	  Output.ident s (lexeme_start lexbuf + isp); 
-	  let eol = body lexbuf in
-	    in_proof := Some eol;
-	    if eol then coq_bol lexbuf else coq lexbuf }
-  | space* prf_token
-      { in_proof := Some true;
-	let eol = 
-	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; body_bol lexbuf end 
-	  else 
-	    let s = lexeme lexbuf in
-	      if s.[String.length s - 1] = '.' then false
-	      else skip_to_dot lexbuf
-	in if eol then coq_bol lexbuf else coq lexbuf }
-  | space* end_kw { 
-      let eol = 
-	if not (!in_proof <> None && !Cdglobals.gallina) then 
-	  begin backtrack lexbuf; body_bol lexbuf end 
-	else skip_to_dot lexbuf
-      in
-	in_proof := None;
-	if eol then coq_bol lexbuf else coq lexbuf }
-  | space* gallina_kw
-      { 
-	in_proof := None;
-	let s = lexeme lexbuf in 
-	let nbsp,isp = count_spaces s in
-	let s = String.sub s isp (String.length s - isp)  in
-	  Output.indentation nbsp;
-	  Output.ident s (lexeme_start lexbuf + isp); 
-	  let eol= body lexbuf in
-	    if eol then coq_bol lexbuf else coq lexbuf }
-  | space* prog_kw
-      { 
-	in_proof := None;
-	let s = lexeme lexbuf in 
-	let nbsp,isp = count_spaces s in
-	  Output.indentation nbsp;
-	  let s = String.sub s isp (String.length s - isp)  in
-	    Output.ident s (lexeme_start lexbuf + isp); 
-	    let eol= body lexbuf in
-	      if eol then coq_bol lexbuf else coq lexbuf }
-
-  | space* "(**" space+ "printing" space+ printing_token space+
-      { let tok = lexeme lexbuf in
-	let s = printing_token_body lexbuf in
-	  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;
-	comment_level := 1;
-	ignore (comment lexbuf);
-	coq_bol lexbuf }
-  | space* "(**" space+ "remove" space+ "printing" space+ 
-      (identifier | token) space* "*)"
-      { remove_printing_token (lexeme lexbuf);
-	coq_bol lexbuf }
-  | space* "(**" space+ "remove" space+ "printing" space+
-      { eprintf "warning: bad 'remove printing' command at character %d\n" 
-	  (lexeme_start lexbuf); flush stderr;
-	comment_level := 1;
-	ignore (comment lexbuf);
-	coq_bol lexbuf }
-  | space* "(*"
-      { comment_level := 1; 
-	if !Cdglobals.parse_comments then begin
-	  let s = lexeme lexbuf in 
-	  let nbsp,isp = count_spaces s in
-	    Output.indentation nbsp;
-	    Output.start_comment ();
-	end;
-	let eol = comment lexbuf in
-	  if eol then coq_bol lexbuf else coq lexbuf }
-  | eof 
-      { () }
-  | _
-      { let eol = 
-	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; 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
-  | nl 
-      { if not (!in_proof <> None && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf }
-  | "(**" space_nl
-      { Output.end_coq (); Output.start_doc (); 
-	let eol = doc_bol lexbuf in
-	  Output.end_doc (); Output.start_coq (); 
-	  if eol then coq_bol lexbuf else coq lexbuf }
-  | "(*"
-      { comment_level := 1;
-	if !Cdglobals.parse_comments then begin
-	  let s = lexeme lexbuf in 
-	  let nbsp,isp = count_spaces s in
-	    Output.indentation nbsp;
-	    Output.start_comment ();
-	end;
-	let eol = comment lexbuf in
-	  if eol then coq_bol lexbuf
-          else coq lexbuf
-      }
-  | nl+ space* "]]"
-      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end }
-  | eof 
-      { () }
-  | gallina_kw_to_hide
-      { let s = lexeme lexbuf in
-	  if !Cdglobals.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
-	      Output.ident s (lexeme_start lexbuf); 
-	      let eol=body lexbuf in 
-		if eol then coq_bol lexbuf else coq lexbuf
-	    end }
-  | prf_token
-      { let eol = 
-	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; body_bol lexbuf end 
-	  else 
-	    let s = lexeme lexbuf in
-	    let eol = 
-	      if s.[String.length s - 1] = '.' then false
-	      else skip_to_dot lexbuf
-	    in
-	      eol
-	in if eol then coq_bol lexbuf else coq lexbuf }
-  | end_kw { 
-      let eol = 
-	if not !Cdglobals.gallina then 
-	  begin backtrack lexbuf; body lexbuf end 
-	else 
-	  let eol = skip_to_dot lexbuf in
-	    if !in_proof <> Some true && eol then 
-	      Output.line_break ();
-	    eol
-      in
-	in_proof := None;
-	if eol then coq_bol lexbuf else coq lexbuf }
-  | gallina_kw
-      { let s = lexeme lexbuf in 
-	  Output.ident s (lexeme_start lexbuf); 
-	let eol = body lexbuf in
-	  if eol then coq_bol lexbuf else coq lexbuf }
-  | prog_kw
-      { let s = lexeme lexbuf in 
-	  Output.ident s (lexeme_start lexbuf); 
-	let eol = body lexbuf in
-	  if eol then coq_bol lexbuf else coq lexbuf }
-  | space+ { Output.char ' '; coq lexbuf }
-  | eof 
-      { () }
-  | _ {	let eol = 
-	  if not !Cdglobals.gallina then 
-	    begin backtrack lexbuf; body 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* nl+
-      { Output.paragraph (); doc_bol lexbuf }
-  | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')?
-      { let eol, lex = strip_eol (lexeme lexbuf) in
-        let lev, s = sec_title lex in
-          Output.section lev (fun () -> ignore (doc (from_string s)));
-	  if eol then doc_bol lexbuf else doc lexbuf }
-  | space* '-'+
-      { let n = count_dashes (lexeme lexbuf) in
-	if n >= 4 then Output.rule () else Output.item n;
-        doc lexbuf }
-  | "<<" space*
-      { Output.start_verbatim (); verbatim lexbuf; doc_bol lexbuf }
-  | eof 
-      { true }
-  | _ 
-      { backtrack lexbuf; doc lexbuf }
-
-(*s Scanning documentation elsewhere *)
-
-and doc = parse
-  | nl
-      { Output.char '\n'; doc_bol lexbuf }
-  | "[[" nl
-      { formatted := true; Output.line_break (); Output.start_inline_coq ();
-	let eol = body_bol lexbuf in 
-	  Output.end_inline_coq (); formatted := false;
-	  if eol then doc_bol lexbuf else doc lexbuf}
-  | "["
-      { brackets := 1; 
-	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
-	doc lexbuf }
-  | '*'* "*)" space* nl
-      { true }
-  | '*'* "*)"
-      { false }
-  | "$"
-      { Output.start_latex_math (); escaped_math_latex lexbuf; doc lexbuf }
-  | "$$"
-      { Output.char '$'; doc lexbuf }
-  | "%"
-      { escaped_latex lexbuf; doc lexbuf }
-  | "%%"
-      { Output.char '%'; doc lexbuf }
-  | "#"
-      { escaped_html lexbuf; doc lexbuf }
-  | "##"
-      { Output.char '#'; doc lexbuf }
-  | eof 
-      { false }
-  | _ 
-      { Output.char (lexeme_char lexbuf 0); doc lexbuf }
-
-(*s Various escapings *)
-
-and escaped_math_latex = parse
-  | "$" { Output.stop_latex_math () }
-  | eof { Output.stop_latex_math () }
-  | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
-
-and escaped_latex = parse
-  | "%" { () }
-  | eof { () }
-  | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
-
-and escaped_html = parse
-  | "#" { () }
-  | "&#"
-        { Output.html_char '&'; Output.html_char '#'; escaped_html lexbuf }
-  | "##"
-        { Output.html_char '#'; escaped_html lexbuf }
-  | eof { () }
-  | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
-
-and verbatim = parse
-  | nl ">>" { Output.verbatim_char '\n'; Output.stop_verbatim () }
-  | eof { Output.stop_verbatim () }
-  | _ { Output.verbatim_char (lexeme_char lexbuf 0); verbatim lexbuf }
-
-(*s Coq, inside quotations *)
-
-and escaped_coq = parse
-  | "]"
-      { decr brackets; 
-	if !brackets > 0 then begin Output.char ']'; escaped_coq lexbuf end }
-  | "["
-      { incr brackets; Output.char '['; escaped_coq lexbuf }
-  | "(*"
-      { comment_level := 1; ignore (comment lexbuf); escaped_coq lexbuf }
-  | "*)"
-      { (* likely to be a syntax error: we escape *) backtrack lexbuf }
-  | eof
-      { () }
-  | token_brackets
-      { let s = lexeme lexbuf in
-	  symbol lexbuf s; escaped_coq lexbuf }
-  | (identifier '.')* identifier
-      { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf }
-  | _ 
-      { Output.char (lexeme_char lexbuf 0); escaped_coq lexbuf }
-
-(*s Coq "Comments" command. *)
-
-and comments = parse
-  | space_nl+ 
-      { Output.char ' '; comments lexbuf }
-  | '"' [^ '"']* '"' 
-      { let s = lexeme lexbuf in
-	let s = String.sub s 1 (String.length s - 2) in
-	ignore (doc (from_string s)); comments lexbuf }
-  | ([^ '.' '"'] | '.' [^ ' ' '\t' '\n'])+
-      { escaped_coq (from_string (lexeme lexbuf)); comments lexbuf }
-  | "." (space_nl | eof)
-      { () }
-  | eof 
-      { () }
-  | _   
-      { Output.char (lexeme_char lexbuf 0); comments lexbuf }
-
-(*s Skip comments *)
-
-and comment = parse
-  | "(*" { incr comment_level; comment lexbuf }
-  | "*)" space* nl { 
-      if !Cdglobals.parse_comments then
-	(Output.end_comment (); Output.line_break ());
-      decr comment_level; if !comment_level > 0 then comment lexbuf else true }
-  | "*)" { 
-      if !Cdglobals.parse_comments then (Output.end_comment ());
-      decr comment_level; if !comment_level > 0 then comment lexbuf else false }
-  | eof  { false }
-  | space+ { if !Cdglobals.parse_comments then 
-	Output.indentation (fst (count_spaces (lexeme lexbuf))); comment lexbuf }
-  | nl   { if !Cdglobals.parse_comments then Output.line_break (); comment lexbuf }
-  | _    { if !Cdglobals.parse_comments then Output.char (lexeme_char lexbuf 0);
-  comment lexbuf }
-      
-and skip_to_dot = parse
-  | '.' space* nl { true }
-  | eof | '.' space+ { false}
-  | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf }
-  | _ { skip_to_dot lexbuf }
-
-and body_bol = parse
-  | space+
-      { Output.indentation (fst (count_spaces (lexeme lexbuf))); body lexbuf }
-  | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
-
-and body = parse
-  | nl {Output.line_break(); body_bol lexbuf}
-  | nl+ space* "]]"
-      { if not !formatted then begin symbol lexbuf (lexeme lexbuf); body lexbuf end else true }
-  | eof { false }
-  | '.' space* nl | '.' space* eof { Output.char '.'; Output.line_break(); true }      
-  | '.' space+ { Output.char '.'; Output.char ' '; false }
-  | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf }
-  | "(*" { comment_level := 1; 
-	   if !Cdglobals.parse_comments then Output.start_comment ();
-	   let eol = comment lexbuf in 
-	     if !Cdglobals.parse_comments then Output.end_comment ();
-	     if eol 
-	     then begin Output.line_break(); body_bol lexbuf end
-	     else body lexbuf }
-  | identifier 
-      { let s = lexeme lexbuf in 
-	  Output.ident s (lexeme_start lexbuf); 
-	  body lexbuf }
-  | token_no_brackets
-      { let s = lexeme lexbuf in
-	  symbol lexbuf s; body lexbuf }
-  | _ { let c = lexeme_char lexbuf 0 in 
-	  Output.char c; 
-          body lexbuf }
-
-and notation_bol = parse
-  | space+
-      { Output.indentation (fst (count_spaces (lexeme lexbuf))); notation lexbuf }
-  | _ { backtrack lexbuf; notation lexbuf }
-
-and notation = parse
-  | nl { Output.line_break(); notation_bol lexbuf }
-  | '"' { Output.char '"'}
-  | token
-      { let s = lexeme lexbuf in
-	  symbol lexbuf s; notation lexbuf }
-  | _ { let c = lexeme_char lexbuf 0 in 
-	  Output.char c; 
-          notation lexbuf }
-
-and skip_hide = parse
-  | eof | end_hide { () }
-  | _ { skip_hide lexbuf }
-
-(*s Reading token pretty-print *)
-
-and printing_token_body = parse
-  | "*)" nl? | eof 
-	{ let s = Buffer.contents token_buffer in 
-	  Buffer.clear token_buffer;
-	  s }
-  | _   { Buffer.add_string token_buffer (lexeme lexbuf); 
-	  printing_token_body lexbuf }
-
-(*s Applying the scanners to files *)
-
-{
-
-  let coq_file f m =
-    reset ();
-    Index.current_library := m;
-    Output.start_module ();
-    let c = open_in f in
-    let lb = from_channel c in
-    Output.start_coq (); coq_bol lb; Output.end_coq ();
-    close_in c
-
-}
-
-- 
cgit v1.2.3