From 700caaace0db146405f89a3700600f196c81c52c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 6 Jun 2018 12:22:45 +0200
Subject: [PATCH] test proofmode output for long lines, and fix it

---
 tests/proofmode.ref           | 40 +++++++++++++++++++++++++++++++++++
 tests/proofmode.v             | 33 +++++++++++++++++++++++++++++
 tests/proofmode_iris.ref      |  3 +--
 theories/proofmode/notation.v |  4 ++--
 4 files changed, 76 insertions(+), 4 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index bc5165837..f225a57a6 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -19,6 +19,46 @@
   --------------------------------------â–¡
   Q ∨ P
   
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  "HP" : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P)
+         ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  --------------------------------------∗
+  P
+  
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  _ : (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P)
+      ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  --------------------------------------∗
+  P
+  
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  "HP" : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | 
+         P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  --------------------------------------∗
+  P
+  
+1 subgoal
+  
+  PROP : sbi
+  P : PROP
+  ============================
+  _ : TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | 
+      P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  --------------------------------------∗
+  P
+  
 1 subgoal
   
   PROP : sbi
diff --git a/tests/proofmode.v b/tests/proofmode.v
index be7245aed..84d2c9229 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -37,6 +37,39 @@ Lemma demo_3 P1 P2 P3 :
   P1 ∗ P2 ∗ P3 -∗ P1 ∗ ▷ (P2 ∗ ∃ x, (P3 ∧ ⌜x = 0⌝) ∨ P3).
 Proof. iIntros "($ & $ & $)". iNext. by iExists 0. Qed.
 
+(* Test line breaking of long assumptions. *)
+Section linebreaks.
+Lemma print_long_line P :
+  (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P) ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  -∗ P.
+Proof.
+  iIntros "HP". Show.
+Abort.
+Lemma print_long_line_anon P :
+  (P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P) ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P
+  -∗ P.
+Proof.
+  iIntros "?". Show.
+Abort.
+
+(* This is specifically crafted such that not having the `hv` in
+   the proofmode notation breaks the output. *)
+Local Notation "'TESTNOTATION' '{{' P '|' Q '}' '}'" := (P ∧ Q)%I
+  (format "'TESTNOTATION'  '{{'  P  '|'  Q  '}' '}'") : bi_scope.
+Lemma print_long_line P :
+  TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  -∗ P.
+Proof.
+  iIntros "HP". Show.
+Abort.
+Lemma print_long_line_anon P :
+  TESTNOTATION {{ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P | P ∗ P ∗ P ∗ P ∗ P ∗ P ∗ P }}
+  -∗ P.
+Proof.
+  iIntros "?". Show.
+Abort.
+End linebreaks.
+
 Definition foo (P : PROP) := (P -∗ P)%I.
 Definition bar : PROP := (∀ P, foo P)%I.
 
diff --git a/tests/proofmode_iris.ref b/tests/proofmode_iris.ref
index 30f4ac3d4..735cba70f 100644
--- a/tests/proofmode_iris.ref
+++ b/tests/proofmode_iris.ref
@@ -103,8 +103,7 @@
   --------------------------------------â–¡
   "Hown1" : na_own t E1
   "Hown2" : na_own t (E2 ∖ ↑N)
-  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ 
-  id (na_own t E2)
+  "Hclose" : ▷ <pers> P ∗ na_own t (E2 ∖ ↑N) ={⊤}=∗ id (na_own t E2)
   --------------------------------------∗
   |={⊤}=> na_own t E1 ∗ na_own t E2 ∗ ▷ P
   
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 37bce07be..7f273eb8e 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -10,10 +10,10 @@ Arguments Esnoc {_} _%proof_scope _%string _%I.
 Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ (INamed H) P)
   (at level 1, P at level 200,
-   left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
+   left associativity, format "Γ H  :  '[hv' P ']' '//'", only printing) : proof_scope.
 Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P)
   (at level 1, P at level 200,
-   left associativity, format "Γ '_'  :  P '//'", only printing) : proof_scope.
+   left associativity, format "Γ '_'  :  '[hv' P ']' '//'", only printing) : proof_scope.
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Γ Δ _) Q%I)
-- 
GitLab