From c435f4d2251bf9b96baad6e2f9b2bb911f1f2ff6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 6 Jun 2018 17:13:06 +0200
Subject: [PATCH] fix linebreak behavior for binary update modalities

---
 tests/proofmode.ref    | 22 ++++++++++++++++++++++
 tests/proofmode.v      | 11 +++++++++++
 theories/bi/notation.v | 11 ++++++-----
 3 files changed, 39 insertions(+), 5 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index ae1266ae4..7f236c6de 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -75,3 +75,25 @@
   --------------------------------------∗
   True
   
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  E : coPset.coPset
+  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
+  ============================
+  --------------------------------------∗
+  PPPPPPPPPPPPPPPPP ={E}=∗
+    QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+  
+1 subgoal
+  
+  PROP : sbi
+  BiFUpd0 : BiFUpd PROP
+  E1, E2 : coPset.coPset
+  PPPPPPPPPPPPPPPPP, QQQQQQQQQQQQQQQQQQ : PROP
+  ============================
+  --------------------------------------∗
+  PPPPPPPPPPPPPPPPP ={E1,E2}=∗
+    QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
+  
diff --git a/tests/proofmode.v b/tests/proofmode.v
index d5b83d55d..e45215ab4 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -517,6 +517,17 @@ 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_P_P_P_P :
 Proof.
   iIntros "?". Show.
 Abort.
+
+Lemma long_fupd E (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
+  PPPPPPPPPPPPPPPPP ={E}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
+Proof.
+  iStartProof. Show.
+Abort.
+Lemma long_fupd_maskchanging E1 E2 (PPPPPPPPPPPPPPPPP QQQQQQQQQQQQQQQQQQ : PROP) :
+  PPPPPPPPPPPPPPPPP ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ.
+Proof.
+  iStartProof. Show.
+Abort.
 End linebreaks.
 
 End printing_tests.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 5322e6d71..3a7ab4344 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -50,34 +50,35 @@ Reserved Notation "'<subj>' P" (at level 20, right associativity).
 
 (** Update modalities *)
 Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
-Reserved Notation "P ==∗ Q" (at level 99, Q at level 200, format "P  ==∗  Q").
+Reserved Notation "P ==∗ Q"
+  (at level 99, Q at level 200, format "'[hv  ' P  ==∗  '/' Q ']'").
 
 Reserved Notation "|={ E1 , E2 }=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }=>  Q").
 Reserved Notation "P ={ E1 , E2 }=∗ Q"
   (at level 99, E1,E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=∗  Q").
+   format "'[hv  ' P  ={ E1 , E2 }=∗  '/' Q ']'").
 
 Reserved Notation "|={ E }=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }=>  Q").
 Reserved Notation "P ={ E }=∗ Q"
   (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=∗  Q").
+   format "'[hv  ' P  ={ E }=∗  '/' Q ']'").
 
 Reserved Notation "|={ E1 , E2 }â–·=> Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
    format "|={ E1 , E2 }â–·=>  Q").
 Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
   (at level 99, E1, E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }▷=∗  Q").
+   format "'[hv  ' P  ={ E1 , E2 }▷=∗  '/' Q ']'").
 Reserved Notation "|={ E }â–·=> Q"
   (at level 99, E at level 50, Q at level 200,
    format "|={ E }â–·=>  Q").
 Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }▷=∗  Q").
+   format "'[hv  ' P  ={ E }▷=∗  '/' Q ']'").
 
 (** Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
-- 
GitLab