[MOD] GUI, layout: Preserve width/height of all panels

Author: ChristianGruen

basex-core/src/main/java/org/basex/gui/GUIOptions.java

@@ -64,7 +64,9 @@ public final class GUIOptions extends Options {
   public static final Comment C_WINDOWS = new Comment("Windows");
 
   /** GUI layout. */
-  public static final StringOption VIEWS = new StringOption("VIEWS", GUIConstants.VIEWS);
+  public static final StringOption LAYOUT = new StringOption("LAYOUT", GUIConstants.VIEWS);
+  /** Width of the project view (pixels). */
+  public static final NumberOption PROJECTSIZE = new NumberOption("PROJECTSIZE", 250);
 
   /** GUI height. */
   public static final NumbersOption GUISIZE = new NumbersOption("GUISIZE", 1004, 748);

basex-core/src/main/java/org/basex/gui/layout/BaseXSplit.java

@@ -1,6 +1,7 @@
 package org.basex.gui.layout;
 
 import java.awt.*;
+import java.util.function.*;
 
 /**
  * Project specific Split panel implementation.
@@ -22,6 +23,18 @@ public final class BaseXSplit extends BaseXBack implements LayoutManager {
   private double[] hiddenSize;
   /** Cached sizes (when panel is hidden). */
   private double[] cachedSize;
+  /** Resize listener. */
+  private Consumer<double[]> resized;
+
+  /** Index of the panel with a fixed pixel size ({@code -1}: proportional). */
+  private int anchor = -1;
+  /** Target pixel size of the anchored panel. */
+  private int anchorSize;
+  /** Minimum pixel size for the anchored panel and its neighbors. */
+  private int anchorMin;
+
+  /** Panels have actually been resized during the current drag. */
+  private boolean dragged;
 
   /**
    * Constructor.
@@ -56,6 +69,42 @@ public void init(final double[] vis, final double[] hidden) {
     hiddenSize = hidden;
   }
 
+  /**
+   * Sets the proportional panel sizes (sum must be 1.0).
+   * @param sizes proportional sizes
+   */
+  public void sizes(final double[] sizes) {
+    propSize = sizes;
+  }
+
+  /**
+   * Registers a listener.
+   * @param listener resize listener
+   */
+  public void resized(final Consumer<double[]> listener) {
+    resized = listener;
+  }
+
+  /**
+   * Anchors a panel to a fixed pixel size.
+   * @param index panel index to anchor
+   * @param size target pixel size
+   * @param min minimum pixel size
+   */
+  public void anchor(final int index, final int size, final int min) {
+    anchor = index;
+    anchorSize = size;
+    anchorMin = min;
+  }
+
+  /**
+   * Returns the current pixel size of the anchored panel.
+   * @return pixel size
+   */
+  public int anchorSize() {
+    return anchorSize;
+  }
+
   /**
    * Sets proportional panel sizes (sum must be 1.0).
    * @param show show/hide flag
@@ -84,6 +133,7 @@ public void visible(final boolean show) {
   void startDrag(final double p) {
     dragPos = p;
     dragSize = propSize.clone();
+    dragged = false;
   }
 
   /**
@@ -92,26 +142,68 @@ void startDrag(final double p) {
    * @param p current position
    */
   void drag(final BaseXSplitSep sep, final double p) {
-    if(dragSize == null) startDrag(p);
-
     final Component[] m = getComponents();
     final int r = propSize.length;
     int q = 0;
     for(int n = 0; n < r - 1; ++n) {
       if(m[(n << 1) + 1] == sep) q = n + 1;
     }
     final double v = (dragPos - p) / (horizontal ? getWidth() : getHeight());
+    final double min = anchor >= 0 ? (double) anchorMin / splitSize() : 0.0001;
     for(int i = 0; i < q; ++i) {
-      if(dragSize[i] - v / q < 0.0001) return;
+      if(dragSize[i] - v / q < min) return;
     }
     for(int i = q; i < r; ++i) {
-      if(dragSize[i] + v / (r - q) < 0.0001) return;
+      if(dragSize[i] + v / (r - q) < min) return;
     }
     for(int i = 0; i < q; ++i) propSize[i] = dragSize[i] - v / q;
     for(int i = q; i < r; ++i) propSize[i] = dragSize[i] + v / (r - q);
+    dragged = true;
     revalidate();
   }
 
+  /**
+   * Finishes a splitter drag: snapshots the anchored pixel size and notifies the listener once.
+   */
+  void endDrag() {
+    if(dragged) {
+      // remember the dragged pixel size of the anchored panel
+      if(anchor >= 0) {
+        anchorSize = (int) Math.round(propSize[anchor] * splitSize());
+      }
+      if(resized != null) resized.accept(propSize);
+    }
+    dragged = false;
+  }
+
+  /**
+   * Computes the proportional size of the anchored panel for the given available space.
+   * The panel keeps its target pixel size, but shrinks down to {@code min} pixels (and no
+   * further) when space runs short, always reserving {@code min} pixels for its neighbors.
+   * @param target target pixel size
+   * @param min minimum pixel size
+   * @param size available space in pixels
+   * @return proportional size (between 0 and 1)
+   */
+  static double anchorFraction(final int target, final int min, final int size) {
+    if(size <= 0) return 0;
+    int a = Math.min(target, size - min);
+    a = Math.max(a, Math.min(min, size));
+    return (double) a / size;
+  }
+
+  /**
+   * Returns the available space for the panels (total size minus the visible separators).
+   * @return size in pixels
+   */
+  private int splitSize() {
+    int seps = propSize.length - 1;
+    for(final double d : propSize) {
+      if(d == 0) --seps;
+    }
+    return (horizontal ? getWidth() : getHeight()) - seps * SEPARATOR_SIZE;
+  }
+
   @Override
   public void addLayoutComponent(final String name, final Component comp) { }
 
@@ -150,6 +242,21 @@ public void layoutContainer(final Container parent) {
 
     // set bounds of all components
     final int sz = (horizontal ? w : h) - c * SEPARATOR_SIZE;
+
+    // enforce a fixed pixel size for the anchored panel (skip while hidden or dragging)
+    if(anchor >= 0 && !dragged && propSize[anchor] != 0 && sz > 0) {
+      final double frac = anchorFraction(anchorSize, anchorMin, sz);
+      // distribute the remaining space among the other panels, keeping their relative sizes
+      double rest = 0;
+      for(int i = 0; i < propSize.length; i++) {
+        if(i != anchor) rest += propSize[i];
+      }
+      for(int i = 0; i < propSize.length; i++) {
+        propSize[i] = i == anchor ? frac :
+          rest > 0 ? propSize[i] / rest * (1 - frac) : (1 - frac) / (propSize.length - 1);
+      }
+    }
+
     double posD = 0;
     boolean invisible = false;
     for(c = 0; c < cl; c++) {

basex-core/src/main/java/org/basex/gui/layout/BaseXSplitSep.java

@@ -32,6 +32,10 @@ public void mousePressed(final MouseEvent e) {
       public void mouseDragged(final MouseEvent e) {
         ((BaseXSplit) getParent()).drag(BaseXSplitSep.this, pos(e));
       }
+      @Override
+      public void mouseReleased(final MouseEvent e) {
+        ((BaseXSplit) getParent()).endDrag();
+      }
 
       private double pos(final MouseEvent e) {
         final Point p = getLocationOnScreen();

basex-core/src/main/java/org/basex/gui/view/ViewComponent.java

@@ -9,6 +9,27 @@
  * @author Christian Gruen
  */
 interface ViewComponent {
+  /**
+   * Returns the proportional size (weight) of this component within its parent layout.
+   * @return weight
+   */
+  double weight();
+
+  /**
+   * Assigns the proportional size (weight) of this component within its parent layout.
+   * @param weight weight
+   */
+  void weight(double weight);
+
+  /**
+   * Formats a weight for the layout string (rounded to four decimal digits).
+   * @param weight weight
+   * @return string representation
+   */
+  static String format(final double weight) {
+    return Double.toString(Math.round(weight * 10_000) / 10_000.0);
+  }
+
   /**
    * Checks if the view layout is visible.
    * @return true if layout is visible

basex-core/src/main/java/org/basex/gui/view/ViewContainer.java

@@ -67,7 +67,7 @@ public ViewContainer(final GUI gui, final View... view) {
     for(int v = 0; v < vl; ++v) views[v] = new ViewPanel(view[v]);
 
     // build layout or use default if something goes wrong
-    if(!buildLayout(gui.gopts.get(GUIOptions.VIEWS)) && !buildLayout(VIEWS)) {
+    if(!buildLayout(gui.gopts.get(GUIOptions.LAYOUT)) && !buildLayout(VIEWS)) {
       Util.errln(Util.className(this) + ": could not build layout.");
     }
   }
@@ -84,16 +84,26 @@ public void updateViews() {
     if(ls.equals(layoutString)) return;
 
     // remember new layout
-    gui.gopts.set(GUIOptions.VIEWS, layout.layoutString(true));
+    persistLayout();
     layoutString = ls;
 
     // rebuild views
     removeAll();
+    layout.persister = this::persistLayout;
     layout.addTo(this);
     validate();
     repaint();
   }
 
+  /**
+   * Stores the current layout, including the proportional view sizes, in the GUI options.
+   * Invoked on structural changes and whenever the user drags a splitter (see
+   * {@link ViewLayout#persister}).
+   */
+  private void persistLayout() {
+    gui.gopts.set(GUIOptions.LAYOUT, layout.layoutString(true));
+  }
+
   @Override
   public void paintComponent(final Graphics g) {
     super.paintComponent(g);
@@ -120,6 +130,8 @@ void dropPanel() {
     if(source == null) return;
 
     if(location != null) {
+      // the model already holds the current sizes (kept in sync on every splitter drag),
+      // so the moved components carry their weights through the restructuring
       final ViewComponent comp = layout.delete(source);
       if(comp instanceof final ViewLayout vl) layout = vl;
 
@@ -315,24 +327,42 @@ private boolean buildLayout(final String string) {
       layout = null;
       int nv = 0;
       final Stack<ViewLayout> layouts = new Stack<>();
-      final StringTokenizer tokens = new StringTokenizer(string);
-      while(tokens.hasMoreTokens()) {
-        final String token = tokens.nextToken();
-        if(Strings.eq(token, "H", "V")) {
+      // collect all tokens (allows look-ahead for the optional weight tokens)
+      final ArrayList<String> tokens = new ArrayList<>();
+      final StringTokenizer st = new StringTokenizer(string);
+      while(st.hasMoreTokens()) tokens.add(st.nextToken());
+
+      final int ts = tokens.size();
+      for(int t = 0; t < ts; t++) {
+        final String token = tokens.get(t);
+        final ViewComponent comp;
+        if("-".equals(token)) {
+          layouts.pop();
+          continue;
+        } else if(Strings.eq(token, "H", "V")) {
           final ViewLayout view = new ViewLayout("H".equals(token));
           if(layouts.isEmpty()) {
             layout = view;
           } else {
             layouts.peek().add(view);
           }
           layouts.add(view);
-        } else if("-".equals(token)) {
-          layouts.pop();
+          comp = view;
         } else {
           final ViewPanel view = getView(token);
           if(view == null) return false;
           layouts.peek().add(view);
           ++nv;
+          comp = view;
+        }
+        // parse the optional proportional size that may follow a layout or view token
+        if(t + 1 < ts) {
+          final String next = tokens.get(t + 1);
+          final char ch = next.charAt(0);
+          if(ch >= '0' && ch <= '9' || ch == '.') {
+            comp.weight(Double.parseDouble(next));
+            ++t;
+          }
         }
       }
       return nv == views.length;