diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 20 | ||||
| -rw-r--r-- | tools/coqdoc/pretty.mll | 29 |
2 files changed, 25 insertions, 24 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 256515c51..cc3b60923 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -397,24 +397,18 @@ let rec process_cmd_line = function let banner () = print -"############################################################################## -## The Calculus of Inductive Constructions ## -## ## -## Projet Coq ## -## ## -## INRIA ENS-CNRS ## -## Rocquencourt Lyon ## -## ## -## Coq V7 ## -## ## -## ## -############################################################################## +"######################################################################### +## v # The Coq Proof Assistant ## +## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ## +## \\VV/ # ## +## // # Makefile automagically generated by coq_makefile V8.1 ## +########################################################################## " let warning () = print "# WARNING\n#\n"; - print "# This Makefile has been automagically generated by coq_makefile\n"; + print "# This Makefile has been automagically generated\n"; print "# Edit at your own risks !\n"; print "#\n# END OF WARNING\n\n" diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 57bdaf635..a095e9d13 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -52,6 +52,11 @@ 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 @@ -449,22 +454,24 @@ and coq = parse 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* + | space* section space+ ([^'\n' '*'] | '*'+ [^'\n' ')' '*'])* ('*'+ '\n')? + { let eol, lex = strip_eol (lexeme lexbuf) in + let lev, s = sec_title lex in +Printf.eprintf "%s %d" s (if eol then 1 else 2); + 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 rule () else item n; + doc lexbuf } + | "<<" space* { start_verbatim (); verbatim lexbuf; doc_bol lexbuf } | eof - { false } + { true } | _ { backtrack lexbuf; doc lexbuf } |