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


Am Freitag, den 08.08.2014, 12:41 +0200 schrieb bnord:
> Also I'd like some marker in the text 
> showing me "here is some sledgehammer instance running click me to get 
> to the results".

I’d like to support that suggestion. The complete lack of feedback in
the editor pane about sledgehammer is one of the reasons why I continue
to invoke sledgehammer by typing.

(Of course there is more to it. In the editor, I can change "by (metis
foo bar baz)" relatively easily to "sledgehammer (add: foo bar baz)". I
don’t know how I would do a similar thing with the panel. Maybe with
more interaction in the panel (such as “update this failing metis call
by using its lemmas in the sledgehammer panel”).

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 (not to
speak of the “apply script assembly panel”).

        who dreams of a document model based ITP that requires nothing
        but interacting with the model

Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

Attachment: signature.asc
Description: This is a digitally signed message part

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