From 0dc4b008c753fa4e20ea95630edea9e3e32c68c0 Mon Sep 17 00:00:00 2001 From: Abhishek Anand (optiplex7010@home) Date: Thu, 20 Feb 2020 19:33:26 -0800 Subject: patched the print function --- printing/ppconstr.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c2d760ae08..65b4e238de 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -85,6 +85,7 @@ let tag_var = tag Tag.variable let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in + let parens = !Constrextern.print_coercions in (* Warning: The following function enforces a very precise order of evaluation of sub-components. @@ -95,7 +96,7 @@ let tag_var = tag Tag.variable | UnpMetaVar prec as unp :: l -> let c = pop env in let pp2 = aux l in - let pp1 = pr prec c in + let pp1 = pr (if parens then prec else LevelLe 0) c in return unp pp1 pp2 | UnpBinderMetaVar prec as unp :: l -> let c = pop bl in @@ -104,7 +105,7 @@ let tag_var = tag Tag.variable return unp pp1 pp2 | UnpListMetaVar (prec, sl) as unp :: l -> let cl = pop envlist in - let pp1 = prlist_with_sep (fun () -> aux sl) (pr prec) cl in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens then prec else LevelLe 0)) cl in let pp2 = aux l in return unp pp1 pp2 | UnpBinderListMetaVar (isopen, sl) as unp :: l -> -- cgit v1.2.3 From 38c47ac0626fed51d17bc7513d7dbbd63053016e Mon Sep 17 00:00:00 2001 From: Abhishek Anand (optiplex7010@home) Date: Thu, 20 Feb 2020 19:52:39 -0800 Subject: added the new option --- printing/ppconstr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 65b4e238de..ed54e046fd 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -85,7 +85,7 @@ let tag_var = tag Tag.variable let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in - let parens = !Constrextern.print_coercions in + let parens = !Constrextern.print_parens in (* Warning: The following function enforces a very precise order of evaluation of sub-components. -- cgit v1.2.3 From dd5a748cbec3abd9a11bbdd3ed4c14497b575fb9 Mon Sep 17 00:00:00 2001 From: Abhishek Anand (optiplex7010@home) Date: Thu, 20 Feb 2020 19:54:37 -0800 Subject: bugfix: switched then/else: parens option false (default)=> no parens --- printing/ppconstr.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ed54e046fd..6ede663883 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -96,7 +96,7 @@ let tag_var = tag Tag.variable | UnpMetaVar prec as unp :: l -> let c = pop env in let pp2 = aux l in - let pp1 = pr (if parens then prec else LevelLe 0) c in + let pp1 = pr (if parens then LevelLe 0 else prec) c in return unp pp1 pp2 | UnpBinderMetaVar prec as unp :: l -> let c = pop bl in @@ -105,7 +105,7 @@ let tag_var = tag Tag.variable return unp pp1 pp2 | UnpListMetaVar (prec, sl) as unp :: l -> let cl = pop envlist in - let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens then prec else LevelLe 0)) cl in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens then LevelLe 0 else prec)) cl in let pp2 = aux l in return unp pp1 pp2 | UnpBinderListMetaVar (isopen, sl) as unp :: l -> -- cgit v1.2.3 From 5820b274acda8be0372471758842b0ea2b950d41 Mon Sep 17 00:00:00 2001 From: Abhishek Anand (optiplex7010@home) Date: Sat, 22 Feb 2020 13:22:27 -0800 Subject: parens --> parentheses --- printing/ppconstr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 6ede663883..d96a528b76 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -85,7 +85,7 @@ let tag_var = tag Tag.variable let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in let pop r = let a = List.hd !r in r := List.tl !r; a in let return unp pp1 pp2 = (tag_unparsing unp pp1) ++ pp2 in - let parens = !Constrextern.print_parens in + let parens = !Constrextern.print_parentheses in (* Warning: The following function enforces a very precise order of evaluation of sub-components. -- cgit v1.2.3 From 858f8dba967713692662f23c79d8c33f2d362e91 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 23 Feb 2020 18:03:13 +0100 Subject: Cancelling precedences in Set Printing Parentheses only at border of notations. --- printing/ppconstr.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'printing/ppconstr.ml') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d96a528b76..59972f8bdb 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -93,19 +93,19 @@ let tag_var = tag Tag.variable let rec aux = function | [] -> mt () - | UnpMetaVar prec as unp :: l -> + | UnpMetaVar (prec, side) as unp :: l -> let c = pop env in let pp2 = aux l in - let pp1 = pr (if parens then LevelLe 0 else prec) c in + let pp1 = pr (if parens && side <> None then LevelLe 0 else prec) c in return unp pp1 pp2 | UnpBinderMetaVar prec as unp :: l -> let c = pop bl in let pp2 = aux l in let pp1 = pr_patt prec c in return unp pp1 pp2 - | UnpListMetaVar (prec, sl) as unp :: l -> + | UnpListMetaVar (prec, sl, side) as unp :: l -> let cl = pop envlist in - let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens then LevelLe 0 else prec)) cl in + let pp1 = prlist_with_sep (fun () -> aux sl) (pr (if parens && side <> None then LevelLe 0 else prec)) cl in let pp2 = aux l in return unp pp1 pp2 | UnpBinderListMetaVar (isopen, sl) as unp :: l -> -- cgit v1.2.3