From e4282ea99c664d8d58067bee199cbbcf881b60d5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 4 Jul 2009 13:28:35 +0200 Subject: Imported Upstream version 8.2.pl1+dfsg --- tools/coq_makefile.ml4 | 20 +++---- tools/coqdoc/cdglobals.ml | 3 +- tools/coqdoc/coqdoc.css | 33 ++++++++++++ tools/coqdoc/coqdoc.sty | 3 ++ tools/coqdoc/main.ml | 7 ++- tools/coqdoc/output.ml | 55 +++++++++++++------ tools/coqdoc/output.mli | 5 +- tools/coqdoc/pretty.mll | 134 +++++++++++++++++++++++++++++++--------------- 8 files changed, 189 insertions(+), 71 deletions(-) (limited to 'tools') diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 98457261..eb3a19fa 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: coq_makefile.ml4 11883 2009-02-06 09:54:52Z herbelin $ *) +(* $Id: coq_makefile.ml4 12176 2009-06-09 09:44:40Z notin $ *) (* créer un Makefile pour un développement Coq automatiquement *) @@ -212,7 +212,7 @@ let clean sds sps = print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \ $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n"; if !some_mlfile then - print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n"; + print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d) $(MLFILES:.ml=.cmx) $(MLFILES:.ml=.o)\n"; if Coq_config.has_natdynlink && !some_mlfile then print "\trm -f $(CMXSFILES) $(CMXSFILES:.cmxs=.o)\n"; print "\t- rm -rf html\n"; @@ -243,14 +243,14 @@ let footer_includes () = let implicit () = let ml_rules () = print "%.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; - print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; - print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -c $(PP) $<\n\n"; - print "%.cmxs: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n"; + print "%.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print "%.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) $<\n\n"; + print "%.cmxs: %.ml\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) $<\n\n"; print "%.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "%.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; - print "%.cmxs: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n"; + print "%.cmxs: %.ml4\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $(PP) -impl $<\n\n"; print "%.ml.d: %.ml\n"; - print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(PP) \"$<\" > \"$@\"\n\n" + print "\t$(CAMLBIN)ocamldep -slash $(COQSRCLIBS) $(OCAMLLIBS) $(PP) \"$<\" > \"$@\"\n\n" and v_rule () = print "%.vo %.glob: %.v\n\t$(COQC) -dump-glob $*.glob $(COQDEBUG) $(COQFLAGS) $*\n\n"; print "%.vi: %.v\n\t$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*\n\n"; @@ -283,8 +283,8 @@ let variables defs = print "COQDOC:=$(COQBIN)coqdoc\n"; print "COQMKTOP:=$(COQBIN)coqmktop\n"; (* Caml executables and relative variables *) - printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; - printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; + printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc; + printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt; printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; print "GRAMMARS:=grammar.cma\n"; @@ -315,7 +315,7 @@ let include_dirs (inc_i,inc_r) = let str_i' = parse_includes inc_i' in let str_r = parse_rec_includes inc_r in section "Libraries definitions."; - print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n " str_i; print "\n"; + print "OCAMLLIBS:="; print_list "\\\n " str_i; print "\n"; print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\ -I $(COQLIB)/library -I $(COQLIB)/parsing \\ -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\ diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml index 5bcbed64..b3f0739d 100644 --- a/tools/coqdoc/cdglobals.ml +++ b/tools/coqdoc/cdglobals.ml @@ -54,9 +54,10 @@ let toc = ref false let page_title = ref "" let title = ref "" let externals = ref true -let coqlib = ref "http://coq.inria.fr/library/" +let coqlib = ref Coq_config.wwwstdlib let coqlib_path = ref Coq_config.coqlib let raw_comments = ref false +let parse_comments = ref false let interpolate = ref false let charset = ref "iso-8859-1" diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index a9a99706..762be5af 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -57,6 +57,11 @@ body { padding: 0px 0px; display: inline; font-family: monospace } +.comment { + display: inline; + font-family: monospace; + color: red; } + .code { display: block; font-family: monospace } @@ -80,18 +85,46 @@ body { padding: 0px 0px; color: rgb(40%,0%,40%); } +.id[type="variable"] { + color: rgb(40%,0%,40%); +} + .id[type="definition"] { color: rgb(0%,40%,0%); } +.id[type="abbreviation"] { + color: rgb(0%,40%,0%); +} + .id[type="lemma"] { color: rgb(0%,40%,0%); } +.id[type="instance"] { + color: rgb(0%,40%,0%); +} + +.id[type="projection"] { + color: rgb(0%,40%,0%); +} + +.id[type="method"] { + color: rgb(0%,40%,0%); +} + .id[type="inductive"] { color: rgb(0%,0%,80%); } +.id[type="record"] { + color: rgb(0%,0%,80%); +} + +.id[type="class"] { + color: rgb(0%,0%,80%); +} + .id[type="keyword"] { color : #cf1d1d; /* color: black; */ diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty index ef4f4119..fca9a1d7 100644 --- a/tools/coqdoc/coqdoc.sty +++ b/tools/coqdoc/coqdoc.sty @@ -70,6 +70,9 @@ % !!! CAUTION: This environment may have empty contents \newenvironment{coqdoccode}{}{} +% Environment for comments +\newenvironment{coqdoccomment}{\tt(*}{*)} + % newline and indentation %BEGIN LATEX % Base indentation length diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 2e97618b..2ee9ac96 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: main.ml 11828 2009-01-22 06:44:11Z notin $ i*) +(*i $Id: main.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) (* Modified by Lionel Elie Mamane on 9 & 10 Mar 2004: * - handling of absolute filenames (function coq_module) @@ -56,7 +56,7 @@ let usage () = prerr_endline " --verbose verbose mode"; prerr_endline " --no-externals no links to Coq standard library"; prerr_endline " --coqlib set URL for Coq standard library"; - prerr_endline " (default is http://coq.inria.fr/library/)"; + prerr_endline (" (default is " ^ Coq_config.wwwstdlib ^ ")"); prerr_endline " --boot run in boot mode"; prerr_endline " --coqlib_path set the path where Coq files are installed"; prerr_endline " -R map physical dir to Coq dir"; @@ -65,6 +65,7 @@ let usage () = prerr_endline " --charset set HTML charset"; prerr_endline " --inputenc set LaTeX input encoding"; prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module"; + prerr_endline " --parse-comments parse regular comments"; prerr_endline ""; exit 1 @@ -273,6 +274,8 @@ let parse () = usage () | ("-raw-comments" | "--raw-comments") :: rem -> Cdglobals.raw_comments := true; parse_rec rem + | ("-parse-comments" | "--parse-comments") :: rem -> + Cdglobals.parse_comments := true; parse_rec rem | ("-interpolate" | "--interpolate") :: rem -> Cdglobals.interpolate := true; parse_rec rem diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index c146150c..1ad8b14f 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.ml 11823 2009-01-21 15:32:37Z msozeau $ i*) +(*i $Id: output.ml 12187 2009-06-13 19:36:59Z msozeau $ i*) open Cdglobals open Index @@ -292,13 +292,13 @@ module Latex = struct let ident s l = if !in_title then ( - printf "\\texorpdfstring{"; + printf "\\texorpdfstring{\\protect"; with_latex_printing (fun s -> ident s l) s; printf "}{"; raw_ident s; printf "}") else with_latex_printing (fun s -> ident s l) s - let symbol = with_latex_printing raw_ident + let symbol s = with_latex_printing raw_ident s let rec reach_item_level n = if !item_level < n then begin @@ -320,6 +320,12 @@ module Latex = struct let end_doc () = in_doc := false; stop_item () + let comment c = char c + + let start_comment () = printf "\\begin{coqdoccomment}\n" + + let end_comment () = printf "\\end{coqdoccomment}\n" + let start_coq () = printf "\\begin{coqdoccode}\n" let end_coq () = printf "\\end{coqdoccode}\n" @@ -389,8 +395,6 @@ module Html = struct printf "
\n\n" end - let self = "http://coq.inria.fr" - let trailer () = if !index && !current_module <> "Index" then printf "
\n\n
\n
Index"; @@ -406,7 +410,7 @@ module Html = struct else begin printf "
This page has been generated by "; - printf "coqdoc\n" self; + printf "coqdoc\n" Coq_config.wwwcoq; printf "
\n\n\n\n\n" end @@ -456,14 +460,15 @@ module Html = struct let ident_ref m fid typ s = match find_module m with | Local -> + printf "" m fid; printf "" typ; - printf "" m fid; raw_ident s; - printf "" + raw_ident s; + printf "" | Coqlib when !externals -> let m = Filename.concat !coqlib m in - printf "" typ; printf "" m fid; - raw_ident s; printf "" + printf "" typ; + raw_ident s; printf "" | Coqlib | Unknown -> printf "" typ; raw_ident s; printf "" @@ -477,8 +482,9 @@ module Html = struct try (match Index.find !current_module loc with | Def (fullid,ty) -> + printf "" fullid; printf "" (type_name ty); - printf "" fullid; raw_ident s; printf "" + raw_ident s; printf "" | Mod (m,s') when s = s' -> module_ref m s | Ref (m,fullid,ty) -> @@ -500,9 +506,11 @@ module Html = struct with Not_found -> f tok - let ident s l = with_html_printing (fun s -> ident s l) s + let ident s l = + with_html_printing (fun s -> ident s l) s - let symbol = with_html_printing raw_ident + let symbol s = + with_html_printing raw_ident s let rec reach_item_level n = if !item_level < n then begin @@ -532,6 +540,10 @@ module Html = struct stop_item (); if not !raw_comments then printf "\n\n" + let start_comment () = printf "(*" + + let end_comment () = printf "*)" + let start_code () = end_doc (); start_coq () let end_code () = end_coq (); start_doc () @@ -540,7 +552,11 @@ module Html = struct let end_inline_coq () = printf "" - let paragraph () = stop_item (); printf "\n

\n" + let paragraph () = + let i = !item_level in + stop_item (); + if i > 0 then printf "\n" + else printf "\n

\n" let section lev f = let lab = new_label () in @@ -770,6 +786,9 @@ module TeXmacs = struct let end_coq () = () + let start_comment () = () + let end_comment () = () + let start_code () = in_doc := true; printf "<\\code>\n" let end_code () = in_doc := false; printf "\n" @@ -849,7 +868,7 @@ module Raw = struct let ident s loc = raw_ident s - let symbol = raw_ident + let symbol s = raw_ident s let item n = printf "- " @@ -858,6 +877,9 @@ module Raw = struct let start_doc () = printf "(** " let end_doc () = printf " *)\n" + let start_comment () = () + let end_comment () = () + let start_coq () = () let end_coq () = () @@ -911,6 +933,9 @@ let start_module = let start_doc = select Latex.start_doc Html.start_doc TeXmacs.start_doc Raw.start_doc let end_doc = select Latex.end_doc Html.end_doc TeXmacs.end_doc Raw.end_doc +let start_comment = select Latex.start_comment Html.start_comment TeXmacs.start_comment Raw.start_comment +let end_comment = select Latex.end_comment Html.end_comment TeXmacs.end_comment Raw.end_comment + let start_coq = select Latex.start_coq Html.start_coq TeXmacs.start_coq Raw.start_coq let end_coq = select Latex.end_coq Html.end_coq TeXmacs.end_coq Raw.end_coq diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 3da80335..75c7ccf8 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id: output.mli 12187 2009-06-13 19:36:59Z msozeau $ i*) open Cdglobals open Index @@ -28,6 +28,9 @@ val start_module : unit -> unit val start_doc : unit -> unit val end_doc : unit -> unit +val start_comment : unit -> unit +val end_comment : unit -> unit + val start_coq : unit -> unit val end_coq : unit -> unit diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll index 3ae5cbed..c4a1a76f 100644 --- a/tools/coqdoc/pretty.mll +++ b/tools/coqdoc/pretty.mll @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pretty.mll 11823 2009-01-21 15:32:37Z msozeau $ i*) +(*i $Id: pretty.mll 12187 2009-06-13 19:36:59Z msozeau $ i*) (*s Utility functions for the scanners *) @@ -57,7 +57,7 @@ let formatted = ref false let brackets = ref 0 let comment_level = ref 0 - let in_proof = ref false + let in_proof = ref None let backtrack lexbuf = lexbuf.lex_curr_pos <- lexbuf.lex_start_pos @@ -162,6 +162,8 @@ else String.sub s 1 (String.length s - 3) + let symbol lexbuf s = Output.symbol s + } (*s Regular expressions *) @@ -217,7 +219,10 @@ let thm_token = | "Proposition" | "Property" | "Goal" - | "Next" space+ "Obligation" + +let prf_token = + "Next" space+ "Obligation" + | "Proof" (space* "." | space+ "with") let def_token = "Definition" @@ -290,7 +295,7 @@ let commands = | ("Hypothesis" | "Hypotheses") | "End" -let end_kw = "Proof" | "Qed" | "Defined" | "Save" | "Admitted" | "Abort" +let end_kw = "Qed" | "Defined" | "Save" | "Admitted" | "Abort" let extraction = "Extraction" @@ -307,7 +312,6 @@ let prog_kw = let gallina_kw_to_hide = "Implicit" space+ "Arguments" - | "Next" "Obligation" | "Ltac" | "Require" | "Import" @@ -343,7 +347,7 @@ let end_verb = "(*" space* "end" space+ "verb" space* "*)" rule coq_bol = parse | space* nl+ - { if not (!in_proof && !Cdglobals.gallina) then Output.empty_line_of_code (); coq_bol lexbuf } + { 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 @@ -379,27 +383,29 @@ rule coq_bol = parse Output.indentation nbsp; Output.ident s (lexeme_start lexbuf + isp); let eol = body lexbuf in - in_proof := true; + in_proof := Some eol; if eol then coq_bol lexbuf else coq lexbuf } - | space* "Proof" (space* "." | space+ "with") - { in_proof := true; + | space* prf_token + { in_proof := Some true; let eol = - if not !Cdglobals.gallina then - begin backtrack lexbuf; body_bol lexbuf end - else true + 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 && !Cdglobals.gallina) then + if not (!in_proof <> None && !Cdglobals.gallina) then begin backtrack lexbuf; body_bol lexbuf end - else - skip_to_dot lexbuf + else skip_to_dot lexbuf in - in_proof := false; + in_proof := None; if eol then coq_bol lexbuf else coq lexbuf } | space* gallina_kw { - in_proof := false; + 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 @@ -409,7 +415,7 @@ rule coq_bol = parse if eol then coq_bol lexbuf else coq lexbuf } | space* prog_kw { - in_proof := false; + in_proof := None; let s = lexeme lexbuf in let nbsp,isp = count_spaces s in Output.indentation nbsp; @@ -441,6 +447,12 @@ rule coq_bol = parse 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 @@ -458,7 +470,7 @@ rule coq_bol = parse and coq = parse | nl - { if not (!in_proof && !Cdglobals.gallina) then Output.line_break(); coq_bol lexbuf } + { 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 @@ -466,12 +478,18 @@ and coq = parse 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 begin Output.line_break(); coq_bol lexbuf end + if eol then coq_bol lexbuf else coq lexbuf } | nl+ space* "]]" - { if not !formatted then begin Output.symbol (lexeme lexbuf); coq lexbuf end } + { if not !formatted then begin symbol lexbuf (lexeme lexbuf); coq lexbuf end } | eof { () } | gallina_kw_to_hide @@ -487,14 +505,29 @@ and coq = parse 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 (!in_proof && !Cdglobals.gallina) then + if not !Cdglobals.gallina then begin backtrack lexbuf; body lexbuf end - else - skip_to_dot lexbuf + else + let eol = skip_to_dot lexbuf in + if !in_proof <> Some true && eol then + Output.line_break (); + eol in - in_proof := false; + in_proof := None; if eol then coq_bol lexbuf else coq lexbuf } | gallina_kw { let s = lexeme lexbuf in @@ -513,8 +546,7 @@ and coq = parse if not !Cdglobals.gallina then begin backtrack lexbuf; body lexbuf end else - let eol = skip_to_dot lexbuf in - if eol then Output.line_break (); eol + skip_to_dot lexbuf in if eol then coq_bol lexbuf else coq lexbuf} @@ -616,8 +648,7 @@ and escaped_coq = parse { () } | token_brackets { let s = lexeme lexbuf in - Output.symbol s; - escaped_coq lexbuf } + symbol lexbuf s; escaped_coq lexbuf } | (identifier '.')* identifier { Output.ident (lexeme lexbuf) (lexeme_start lexbuf); escaped_coq lexbuf } | _ @@ -644,15 +675,30 @@ and comments = parse (*s Skip comments *) and comment = parse - | "(*" { incr comment_level; comment lexbuf } - | "*)" space* nl { decr comment_level; if !comment_level > 0 then comment lexbuf else true } - | "*)" { decr comment_level; if !comment_level > 0 then comment lexbuf else false } - | eof { false } - | _ { comment lexbuf } - + | "(*" { incr comment_level; + if !Cdglobals.parse_comments then Output.start_comment (); + 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 } + | "[" { + if !Cdglobals.parse_comments then ( + brackets := 1; + Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ()); + comment lexbuf } + | 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} + | eof | '.' space+ { false } | "(*" { comment_level := 1; ignore (comment lexbuf); skip_to_dot lexbuf } | _ { skip_to_dot lexbuf } @@ -664,15 +710,19 @@ and body_bol = parse and body = parse | nl {Output.line_break(); body_bol lexbuf} | nl+ space* "]]" - { if not !formatted then begin Output.symbol (lexeme lexbuf); body lexbuf end else true } + { 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 } + | '.' space* nl | '.' space* eof + { Output.char '.'; Output.line_break(); + if not !formatted then true else body_bol lexbuf } + | '.' space+ { Output.char '.'; Output.char ' '; + if not !formatted then false else body lexbuf } | '"' { Output.char '"'; ignore(notation lexbuf); body lexbuf } | "(*" { comment_level := 1; + if !Cdglobals.parse_comments then Output.start_comment (); let eol = comment lexbuf in if eol - then begin Output.line_break(); body_bol lexbuf end + then begin if not !Cdglobals.parse_comments then Output.line_break(); body_bol lexbuf end else body lexbuf } | identifier { let s = lexeme lexbuf in @@ -680,7 +730,7 @@ and body = parse body lexbuf } | token_no_brackets { let s = lexeme lexbuf in - Output.symbol s; body lexbuf } + symbol lexbuf s; body lexbuf } | _ { let c = lexeme_char lexbuf 0 in Output.char c; body lexbuf } @@ -695,7 +745,7 @@ and notation = parse | '"' { Output.char '"'} | token { let s = lexeme lexbuf in - Output.symbol s; notation lexbuf } + symbol lexbuf s; notation lexbuf } | _ { let c = lexeme_char lexbuf 0 in Output.char c; notation lexbuf } -- cgit v1.2.3