Re: [isabelle] Isabelle2015-RC0 available for testing



On Fri, 17 Apr 2015, Lars Hupel wrote:

I've toyed around with the various '_deps' commands a bit. I do like the
new graph viewer.

I have made more last-minute refinements of it in Isabelle2015-RC1, and subsequently I refer to that version.


* The new viewer is a jEdit panel, which means it always stays on top
  unless it's minimized (my environment: KDE 4.x). Could this be
  changed, possibly for all panels, so that it does not stay on top, or
  is this a jEdit limitation? Most desktop environments offer a shortkey
  to force such behaviour anyway, so I could just enable it on the spot
  if I wanted to.

This panel behaviour was newly introduced in Isabelle2014 -- I specifically patched the jEdit docking framework for that (most of that was accepted by the jEdit maintainers for a future release). The problem is that Java/AWT does not really know about window managers. There are three different classes doing similar things: JWindow, JFrame, JDialog -- they merely differ in accidental window manager hints.

Since Isabelle2014 we are using JDialog instead of JFrame, because these windows stay on top of the main editor frame. This might be occasionally odd, especially on Linux, but on Mac OS X and Windows it is essential to work properly. Otherwise, windows could end up in an unreachable position behind the main window, e.g. when working in the full-screen mode that is now very common on these platforms.

All this behaviour is somehow hardwired into JWindow, JFrame, JDialog, and cannot be changed. It is just a matter of choosing the smallest evil by default. Once on Stackoverflow in the "java" and "swing" areas, I asked critical questions about these three classes, but I got quickly removed by some guys with a lot of points, although someone else had marked this as "favourite question".


* 'thy_deps' offers no possibility to fold heaps. Was that a deliberate
  decision? In my current development I have about 3-4 layered images
  and would like to fold them.

Both thy_deps and class_deps have ways to specify intervals of the hierarchy to be visualized. It would be better to have that in the GUI, but that is more work and experimental tinkering, instead of a bit of filtering output in Isabelle/ML.

For Isabelle2015, the priority was to have the new graphview (new since Sep-2012) in a usable state. So I spent about 2-3 weeks on it, and the TODO list was longer afterwards than before. Nonetheless, it should be usable now, and actually do the same graph layout than the old browser from 1996.


* Most applications offer zooming by scrolling while pressing Ctrl. In
  the viewer, I can't do that.

The new Graphview did have some Google-Maps-style zooming before I started working on it, but it did not quite work, so I removed it (like many other unfinished things). The present version is meant to approximate the old browser from the bottom, although many add-on features have again crept into it.

I would also like to see better zooming, but instead of C-mouse-wheel, I find myself looking for zoom-width or zoom-height buttons like good old Evince on Linux, before it got changed into unusablity about 1-2 years ago.

I would also like to see all zoom facilities moving uniformly in Isabelle/jEdit, e.g. the zoom for the Output panel and others. But that is avantgarde, and for a later release.


	Makarius




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