Re: [isabelle] Tab completion slow in Isabelle2014-RC2

On Fri, 8 Aug 2014, Joachim Breitner wrote:

But UI guided interaction will always be limited in expressiveness and efficiency, compared to a textual interface. There is a reason why we _write_ Isar, and do not use a “proof block panel” to click together the fixes and assumes, and elsewhere select the initial proof method

Both the writing and clicking that is sketched here is cumbersome, and conceptually not really different. A more high-level editing model of interactice proof documents is required, and apply scripts should be left behind altogether.

I've started working on more than 15 years ago, but even today people still think of the source text as a "script" that is somehow linear.


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