Re: [isabelle] qed and done take long for large goal states



On 10/08/16 13:29, Lawrence Paulson wrote:
> That is a major gain and certainly worth keeping.
> 
> I am not terribly bothered by the presentation of abbreviations, but nevertheless, perhaps we can get the best of both? After all, no abbreviations are printed when you type qed.

The overall result is printed, and thus all abbreviations of the context
are potentially applied to some potentially large term.

This relative verbosity of the system goes back to the 1990s and TTY
mode / Proof General. In early PIDE versions, it was not done due to
confusion with the remaining Proof General setup. After that was
deleted, printing in the old way was mostly restored.


So maybe instead of tweaking low-level data structures, it is better to
change something in the general policies. E.g.

  * A context option like "show_results" to control printing of results.
  * Asynchronous printing of results.


	Makarius





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