Picking this and calculation in Isabelle/JEdit output

Question

This is a follow-up to

How to write a low-level proof in Isar?

Having

lemma por_qandr_imp_porq: assumes "p ∨ (q ∧ r)" shows "p ∨ q"
proof -
  note assms
  moreover
  have "p ⟹ p ∨ q"
    by (rule p_imp_porq)
  moreover
  have "q ∧ r ⟹ p ∨ q"
    by (rule qandr_imp_porq)
  ultimately
  show ?thesis
    by (rule disjE[of p "q∧r" "p∨q"])
qed

if I point the cursor after ultimately, Isabelle/JEdit's Output window shows

proof (chain)
picking this:
    p ∨ q ∧ r
    p ⟹ p ∨ q
    q ∧ r ⟹ p ∨ q 
calculation:
    p ∨ q ∧ r
    p ⟹ p ∨ q
    q ∧ r ⟹ p ∨ q

where calculation is in grey background. The contents of the picking this and the calculation parts are identical, but what is the difference between the two in their meaning?

Answer 1

At each step accumulating facts (i.e., each of moreover and the final ultimately), the proof state will show the fact calculation—which you can quote inside the proof, by the way.

AFAIK, this is redundant in the final step since both lists are the same. But the picking this message is useful since it indicates that those facts will be used (“chained”) for the next inference (which does not occur at moreover steps). If you actually want to use all of them amidst that block, you may invoke moreover from calculation.