From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- tools/coqdep.ml | 22 ++++++++++++++-------- tools/coqdoc/coqdoc.sty | 2 +- tools/coqdoc/index.mll | 3 ++- tools/coqdoc/output.ml | 4 ++-- tools/coqdoc/pretty.mll | 25 ++++++++++++++----------- 5 files changed, 33 insertions(+), 23 deletions(-) (limited to 'tools') diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 6597c3f6..3647152a 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -6,18 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coqdep.ml 8923 2006-06-08 16:39:58Z herbelin $ *) +(* $Id: coqdep.ml 9276 2006-10-25 13:00:22Z barras $ *) open Printf open Coqdep_lexer open Unix -let (/) = Filename.concat - -let file_concat l = - if l=[] then "" else - List.fold_left (/) (List.hd l) (List.tl l) - let stderr = Pervasives.stderr let stdout = Pervasives.stdout @@ -28,12 +22,23 @@ let option_D = ref false let option_w = ref false let option_i = ref false let option_sort = ref false +let option_slash = ref false let suffixe = ref ".vo" let suffixe_spec = ref ".vi" type dir = string option +(* filename for printing *) +let (//) s1 s2 = + if !option_slash then s1^"/"^s2 else Filename.concat s1 s2 + +let (/) = Filename.concat + +let file_concat l = + if l=[] then "" else + List.fold_left (//) (List.hd l) (List.tl l) + (* Files specified on the command line *) let mlAccu = ref ([] : (string * string * dir) list) and mliAccu = ref ([] : (string * string * dir) list) @@ -148,7 +153,7 @@ let cut_prefix p s = if ls >= lp && String.sub s 0 lp = p then String.sub s lp (ls - lp) else s let canonize f = match Sys.os_type with - | "Win32" -> cut_prefix ".\\" f + | "Win32" when not !option_slash -> cut_prefix ".\\" f | _ -> cut_prefix "./" f let sort () = @@ -517,6 +522,7 @@ let coqdep () = | "-coqlib" :: [] -> usage () | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll | "-suffix" :: [] -> usage () + | "-slash" :: ll -> option_slash := true; parse ll | f :: ll -> treat None f; parse ll | [] -> () in diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index 597152f5..2c07b9fc 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -50,7 +50,7 @@ %HEVEA\newcommand{\coqdocindent}[1]{\hspace{#1}\hspace{#1}} % macro for typesetting the title of a module implementation -\newcommand{\coqdocmodule}[1]{\section*{Module #1}\markboth{Module #1}{} +\newcommand{\coqdocmodule}[1]{\chapter{Module #1}\markboth{Module #1}{} } %HEVEA\newcommand{\lnot}{\coqwkw{not}} diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 9b5716ff..5b281b8b 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mll 8863 2006-05-26 10:33:21Z notin $ i*) +(*i $Id: index.mll 9204 2006-10-04 13:05:58Z notin $ i*) { @@ -364,6 +364,7 @@ and end_ident = parse and module_ident = parse | space+ { module_ident lexbuf } + | '"' { string lexbuf; module_ident lexbuf } | ident space* ":=" { () } | ident diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index e6a0a72b..84e03d92 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 8863 2006-05-26 10:33:21Z notin $ i*) +(*i $Id: output.ml 9245 2006-10-17 12:53:34Z notin $ i*) open Cdglobals open Index @@ -118,7 +118,7 @@ module Latex = struct let header () = if !header_trailer then begin - printf "\\documentclass[12pt]{article}\n"; + printf "\\documentclass[12pt]{report}\n"; if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc; printf "\\usepackage[T1]{fontenc}\n"; printf "\\usepackage{fullpage}\n"; diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 5c6c7952..bdb58f86 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 8861 2006-05-24 15:52:15Z notin $ i*) +(*i $Id: pretty.mll 9204 2006-10-04 13:05:58Z notin $ i*) (*s Utility functions for the scanners *) @@ -398,19 +398,22 @@ and coq = parse { () } | gallina_kw_to_hide { let s = lexeme lexbuf in - 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 } + 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 } + let eol = body lexbuf in + if eol then coq_bol lexbuf else coq lexbuf } | space+ { char ' '; coq lexbuf } | eof { () } -- cgit v1.2.3