aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/genprint.ml10
-rw-r--r--printing/genprint.mli10
-rw-r--r--printing/ppconstr.ml21
-rw-r--r--printing/ppconstr.mli10
-rw-r--r--printing/pputils.ml26
-rw-r--r--printing/pputils.mli16
-rw-r--r--printing/ppvernac.ml10
-rw-r--r--printing/ppvernac.mli10
-rw-r--r--printing/prettyp.ml10
-rw-r--r--printing/prettyp.mli10
-rw-r--r--printing/printer.ml10
-rw-r--r--printing/printer.mli10
-rw-r--r--printing/printmod.ml10
-rw-r--r--printing/printmod.mli10
14 files changed, 111 insertions, 62 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 37a94fe219..1bb7838a45 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
diff --git a/printing/genprint.mli b/printing/genprint.mli
index baa60fcb2e..fd5dd7259e 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Entry point for generic printers *)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 3c7095505a..8854ff8981 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(*i*)
@@ -149,7 +151,7 @@ let tag_var = tag Tag.variable
str "`" ++ str hd ++ c ++ str tl
let pr_com_at n =
- if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
+ if !Flags.beautify && not (Int.equal n 0) then comment (Pputils.extract_comments n)
else mt()
let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp)
@@ -701,13 +703,16 @@ let tag_var = tag Tag.variable
| { CAst.v = CAppExpl ((None,f,us),[]) } -> str "@" ++ pr_cref f us
| c -> pr prec c
- let transf env c =
+ let transf env sigma c =
if !Flags.beautify_file then
- let r = Constrintern.for_grammar (Constrintern.intern_constr env) c in
+ let r = Constrintern.for_grammar (Constrintern.intern_constr env sigma) c in
Constrextern.extern_glob_constr (Termops.vars_of_env env) r
else c
- let pr_expr prec c = pr prec (transf (Global.env()) c)
+ let pr_expr prec c =
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ pr prec (transf env sigma c)
let pr_simpleconstr = pr_expr lsimpleconstr
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index cedeed5f34..1f1308b0df 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** This module implements pretty-printers for constr_expr syntactic
diff --git a/printing/pputils.ml b/printing/pputils.ml
index e779fc5fc0..010b92f3e6 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
@@ -13,14 +15,26 @@ open Misctypes
open Locus
open Genredexpr
+let beautify_comments = ref []
+
+let rec split_comments comacc acc pos = function
+ | [] -> beautify_comments := List.rev acc; comacc
+ | ((b,e),c as com)::coms ->
+ (* Take all comments that terminates before pos, or begin exactly
+ at pos (used to print comments attached after an expression) *)
+ if e<=pos || pos=b then split_comments (c::comacc) acc pos coms
+ else split_comments comacc (com::acc) pos coms
+
+let extract_comments pos = split_comments [] [] pos !beautify_comments
+
let pr_located pr (loc, x) =
match loc with
| Some loc when !Flags.beautify ->
let (b, e) = Loc.unloc loc in
(* Side-effect: order matters *)
- let before = Pp.comment (CLexer.extract_comments b) in
+ let before = Pp.comment (extract_comments b) in
let x = pr x in
- let after = Pp.comment (CLexer.extract_comments e) in
+ let after = Pp.comment (extract_comments e) in
before ++ x ++ after
| _ -> pr x
diff --git a/printing/pputils.mli b/printing/pputils.mli
index ec5c32fc46..6039168f88 100644
--- a/printing/pputils.mli
+++ b/printing/pputils.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Genarg
@@ -37,3 +39,9 @@ val pr_red_expr_env : Environ.env -> Evd.evar_map ->
val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t
val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t
+
+(* The comments interface is imperative due to the printer not
+ threading it, this could be solved using a better data
+ structure. *)
+val beautify_comments : ((int * int) * string) list ref
+val extract_comments : int -> string list
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 83cac7ddda..8551d040dd 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 603be63083..4aa24bf5db 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** This module implements pretty-printers for vernac_expr syntactic
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 114a071eee..3682b7c25b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Changed by (and thus parts copyright ©) by Lionel Elie Mamane <lionel@mamane.lu>
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index c1d8f1d37a..213f0aeeb6 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/printing/printer.ml b/printing/printer.ml
index d720bc2f8c..917ee2021a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
diff --git a/printing/printer.mli b/printing/printer.mli
index a3427920af..e32cb0921e 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 2cdb9be3f0..43796ec618 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Util
diff --git a/printing/printmod.mli b/printing/printmod.mli
index 4f15dd3936..b0b0b0a35e 100644
--- a/printing/printmod.mli
+++ b/printing/printmod.mli
@@ -1,9 +1,11 @@
(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 06:23:21 +0000