[isabelle-dev] NEWS: Dockable window "Find"

Holger Gast gast at informatik.uni-tuebingen.de
Wed Sep 25 09:44:04 CEST 2013

On 09/23/2013 01:25 PM, Makarius wrote:
> On Fri, 20 Sep 2013, Holger Gast wrote:
>> The layers 2+3 offer extensive means of customization.
>> To come back to the above example, one does, of course, not set
>> StyleRanges on the SWT widget oneself. One registers with the
>> JFace TextViewer's syntax highlighting mechanism and produces
>> them on demand -- for instance from the semantic markup offered
>> by Isabelle/Scala.
> Again: Why not make this practical, and tell Andrius Velykis about it? He has
> already Isabelle/Eclipse that is more than just a proof of concept or a small
> demo, so it deserves to catch up with the quality standards of Isabelle/jEdit.
I'm sure there is no need to explain such elementary facts as
the Eclipse/JFace/SWT layers and their respective responsibilities
to Andrius.

My motivation for outlining the Eclipse stack in some detail here
is quite simply that I wished to motivate people to consider writing
UIs for their own Isabelle applications. Wouldn't it be great
if we saw more C/Java/... verification tools integrated with the
Eclipse CDT/JDT/... environment? (One of my students has shown that it
can be done for C, Java should be even simpler; the basis was
the model layer of I3P.) Such integrations would foster the interest
of practitioners in theorem proving, which would certainly be desirable.

The prerequisite for such developments is, however, that people are not
scared away from UI programming by statements such as all existing
frameworks being "crap", their developers being "evil companies", and
that it is imperative to read through tons of sources to achieve
one's goals. Depending on the sources introduces tight coupling anyway,
which in turn leads to dependencies on specific versions of the JDK
and ensuing portability issues.

In reality, due to its long history and high practical relevance,
UI programming is one of the best understood areas in software
development. The available tool support (Netbeans' Matisse or
Eclipse's WindowBuilder) makes it very simple to get panels up
quickly. The editing frameworks of both Netbeans and Eclipse are
very mature. As long as one adheres conscientiously to the
contracts stated in the frameworks' documentation, there's
no need to understand the sources.

> Anyway, this thread is going in circles, back to the point where it started 5
> years ago.  The only difference is that Isabelle/jEdit has become real in the
> meantime
Well, there are other differences: I3P has (long since) become a reality
and has actually been used by others, in different environments,
and has even been built upon in Matej Urbas' Diabelli project [1].
Thanks to the well-designed and stable Netbeans infrastructure,
there have never been any portability problems.

I do agree, however, that there are certain circles in the
discussion due to fundamentally different approaches to UI
programming. I hope to have contributed, at least, a second
opinion on the topic as taken from the literature on Swing [2],
Netbeans [3], and Eclipse [4].



[1] Urbas and Jamnik: Diabelli: a heterogeneous proof system, IJCAR 2012.
[2] Eckstein et al. Java Swing, O'Reilly.
[3] Boudreau et al.: Rich Client Programming: Plugging into
    the Netbeans platform, Prentice Hall.
[4] McAffer et al.: Eclipse Rich Client Platform, Addison-Wesley

More information about the isabelle-dev mailing list