Print "n focused goals / x shelved / ID y" in 1 line

Suggested by cpitclaudel in #14998
coq · Oct 9, 2021 · ad1f688 · ad1f688
1 parent 2880bc7
commit ad1f688
Show file tree

Hide file tree

Showing 8 changed files with 125 additions and 149 deletions.
diff --git a/printing/printer.ml b/printing/printer.ml
@@ -771,8 +771,8 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
       let goals = print_multiple_goals g1 rest in
       let ngoals = List.length rest+1 in
       v 0 (
-        int ngoals ++ focused_if_needed ++ str(String.plural ngoals "goal")
-        ++ print_extra
+        hov 0 (int ngoals ++ focused_if_needed ++ str(String.plural ngoals "goal")
+               ++ print_extra)
         ++ str (if pr_first && (should_gname()) && ngoals > 1 then ", goal 1" else "")
         ++ (if pr_first && should_tag() then pr_goal_tag g1 else str"")
         ++ (if pr_first then pr_goal_name sigma g1 else mt()) ++ cut () ++ goals

diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
@@ -50,8 +50,7 @@ Coq < Coq < 1 goal
 (dependent evars: ; in current goal:)
 
 p14 < 
-p14 < 4 focused goals
-(shelved: 2)
+p14 < 4 focused goals (shelved: 2)
 
   P1, P2, P3, P4 : Prop
   p12 : P1 -> P2
@@ -69,8 +68,7 @@ goal 4 is:
 
 (dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
 
-p14 < 3 focused goals
-(shelved: 2)
+p14 < 3 focused goals (shelved: 2)
 
   P1, P2, P3, P4 : Prop
   p12 : P1 -> P2

diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
@@ -52,8 +52,7 @@ Coq < Coq < 1 goal
 p14 < 
 p14 < Second proof:
 
-p14 < 4 focused goals
-(shelved: 2)
+p14 < 4 focused goals (shelved: 2)
 
   P1, P2, P3, P4 : Prop
   p12 : P1 -> P2
@@ -71,8 +70,7 @@ goal 4 is:
 
 (dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
 
-p14 < 1 focused goal
-(shelved: 2)
+p14 < 1 focused goal (shelved: 2)
 
   P1, P2, P3, P4 : Prop
   p12 : P1 -> P2
@@ -86,8 +84,7 @@ p14 < 1 focused goal
 p14 < This subproof is complete, but there are some unfocused goals.
 Try unfocusing with "}".
 
-3 goals
-(shelved: 2)
+3 goals (shelved: 2)
 
 goal 1 is:
  ?P -> (?P0 -> P4) /\ ?P0
@@ -98,8 +95,7 @@ goal 3 is:
 
 (dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:)
 
-p14 < 3 focused goals
-(shelved: 2)
+p14 < 3 focused goals (shelved: 2)
 
   P1, P2, P3, P4 : Prop
   p12 : P1 -> P2

diff --git a/test-suite/output-coqtop/ShowGoal.out b/test-suite/output-coqtop/ShowGoal.out
@@ -1,73 +1,68 @@
-
-Coq < 1 goal
-
-  ============================
-  forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k
-
-x < 
-x < 1 focused goal
-(shelved: 1)
-
-  i : nat
-  ============================
-  exists k : nat, i = ?j /\ ?j = k /\ i = k
-
-x < 1 focused goal
-(shelved: 2)
-
-  i : nat
-  ============================
-  i = ?j /\ ?j = ?k /\ i = ?k
-
-x < 2 focused goals
-(shelved: 2)
-
-  i : nat
-  ============================
-  i = ?j
-
-goal 2 is:
- ?j = ?k /\ i = ?k
-
-x < 1 focused goal
-(shelved: 1)
-
-  i : nat
-  ============================
-  i = ?k /\ i = ?k
-
-x < 2 focused goals
-(shelved: 1)
-
-  i : nat
-  ============================
-  i = ?k
-
-goal 2 is:
- i = ?k
-
-x < 1 goal
-
-  i : nat
-  ============================
-  i = i
-
-x < goal ID 13 at state 5
-
-  i : nat
-  ============================
-  i = ?j /\ ?j = ?k /\ i = ?k
-
-x < goal ID 13 at state 7
-
-  i : nat
-  ============================
-  i = i /\ i = ?k /\ i = ?k
-
-x < goal ID 13 at state 9
-
-  i : nat
-  ============================
-  i = i /\ i = i /\ i = i
-
-x < 
+
+Coq < 1 goal
+
+  ============================
+  forall i : nat, exists j k : nat, i = j /\ j = k /\ i = k
+
+x < 
+x < 1 focused goal (shelved: 1)
+
+  i : nat
+  ============================
+  exists k : nat, i = ?j /\ ?j = k /\ i = k
+
+x < 1 focused goal (shelved: 2)
+
+  i : nat
+  ============================
+  i = ?j /\ ?j = ?k /\ i = ?k
+
+x < 2 focused goals (shelved: 2)
+
+  i : nat
+  ============================
+  i = ?j
+
+goal 2 is:
+ ?j = ?k /\ i = ?k
+
+x < 1 focused goal (shelved: 1)
+
+  i : nat
+  ============================
+  i = ?k /\ i = ?k
+
+x < 2 focused goals (shelved: 1)
+
+  i : nat
+  ============================
+  i = ?k
+
+goal 2 is:
+ i = ?k
+
+x < 1 goal
+
+  i : nat
+  ============================
+  i = i
+
+x < goal ID 13 at state 5
+
+  i : nat
+  ============================
+  i = ?j /\ ?j = ?k /\ i = ?k
+
+x < goal ID 13 at state 7
+
+  i : nat
+  ============================
+  i = i /\ i = ?k /\ i = ?k
+
+x < goal ID 13 at state 9
+
+  i : nat
+  ============================
+  i = i /\ i = i /\ i = i
+
+x < 
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out
@@ -1,42 +1,39 @@
-
-Coq < Coq < 1 goal
-
-  ============================
-  [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
-
-x < 
-x < 1 focused goal
-(shelved: 1)
-  [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
-  ============================
-  [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
-
-[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
- [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
-
-x < 1 focused goal
-(shelved: 2)
-  i : nat
-  ============================
-  [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
-
-[48;2;0;91;0m([1mfun[22m i : nat =>[49m
- [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
-   [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
-
-x < 2 focused goals
-(shelved: 2)
-  i : nat
-  ============================
-  [48;2;0;91;0mi[37m =[39m ?j[0m
-
-goal 2 is:
- [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
-
-[48;2;0;91;0m([1mfun[22m i : nat =>[49m
- [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
-   [48;2;0;91;0m?j[49m
-   [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
-      [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
-
-x < 
+
+Coq < Coq < 1 goal
+
+  ============================
+  [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x < 
+x < 1 focused goal (shelved: 1)
+  [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+  ============================
+  [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused goal (shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused goals (shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[0m
+
+goal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m?j[49m
+   [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+      [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x < 
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
@@ -3,8 +3,7 @@ In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
 while it is expected to have type "{x : nat | x = y}".
-1 focused goal
-(shelved: 1)
+1 focused goal (shelved: 1)
 
   H : ?n <= 3 -> 3 <= ?n -> ?n = 3
   ============================

diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out
@@ -1,5 +1,4 @@
-3 focused goals
-(shelved: 1)
+3 focused goals (shelved: 1)
 
   ============================
   ?Goal 0
@@ -13,8 +12,7 @@ unification constraint:
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
    veeryyyyyyyyyyyyloooooooooooooonggidentifier
-3 focused goals
-(shelved: 1)
+3 focused goals (shelved: 1)
 
   n, m : nat
   ============================
@@ -29,8 +27,7 @@ unification constraint:
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
    veeryyyyyyyyyyyyloooooooooooooonggidentifier
-3 focused goals
-(shelved: 1)
+3 focused goals (shelved: 1)
 
   m : nat
   ============================
@@ -46,8 +43,7 @@ unification constraint:
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
    veeryyyyyyyyyyyyloooooooooooooonggidentifier
-3 focused goals
-(shelved: 1)
+3 focused goals (shelved: 1)
 
   m : nat
   ============================

diff --git a/test-suite/output/unification.out b/test-suite/output/unification.out
@@ -9,32 +9,27 @@ Unable to unify "T" with "?X@{x0:=x; x:=C a}" (cannot instantiate
 The command has indeed failed with message:
 The term "id" has type "ID" while it is expected to have type 
 "Type -> ?T" (cannot instantiate "?T" because "A" is not in its scope).
-1 focused goal
-(shelved: 1)
+1 focused goal (shelved: 1)
 
   H : forall x : nat, S (S (S x)) = x
   ============================
   ?x = 0
-1 focused goal
-(shelved: 1)
+1 focused goal (shelved: 1)
 
   H : forall x : nat, S (S (S x)) = x
   ============================
   ?x = 0
-1 focused goal
-(shelved: 1)
+1 focused goal (shelved: 1)
 
   H : forall x : nat, S (S (S x)) = x
   ============================
   ?x = 0
-1 focused goal
-(shelved: 1)
+1 focused goal (shelved: 1)
 
   H : forall x : nat, S x = x
   ============================
   ?y = 0
-1 focused goal
-(shelved: 3)
+1 focused goal (shelved: 3)
 
   T : Prop
   H : forall Q R S : Prop, (Q /\ R) /\ S -> T