[isabelle] Redundant trace with jEdit



Hi all the people,

The title mention jEdit, while I'm not sure that's jEdit specific. Read: at least with jEdit.

If ever I create a redundant lemma, Isabelle warns me all the time, even when I feel it helps readability. But it seems it don't applies the same to it‑self: whenever I do “using [[simp_trace=true]]” and enable trace in the output pan, I often get redundant entries starting with

  “[1]Adding rewrite rule "??.unknown":”

For a concrete case I just had, there were multiple

  [1]Adding rewrite rule "??.unknown":
  r x y ≡ True

When repeated multiple times for multiple rewrite rules, this make the trace encumbered and less readable.

Is there a known way to filter it out automatically? If possible, I would like to have only one trace message for each added rewrite rule. A quick search using https://lists.cam.ac.uk/mailman/mmsearch/cl-isabelle-users returned nothing on that topic.


Have an happy time

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.