From be339d1d75f507d122d07813850f0c6936334f67 Mon Sep 17 00:00:00 2001
From: Nils Vreman <nils.vreman@gmail.com>
Date: Fri, 9 Nov 2018 12:37:30 +0100
Subject: [PATCH] Fixed offset error
---
gui/tasksetgui/TasksetDisplay.java | 17 ++++++++---------
1 file changed, 8 insertions(+), 9 deletions(-)
diff --git a/gui/tasksetgui/TasksetDisplay.java b/gui/tasksetgui/TasksetDisplay.java
index 7117e96..20663d7 100644
--- a/gui/tasksetgui/TasksetDisplay.java
+++ b/gui/tasksetgui/TasksetDisplay.java
@@ -59,9 +59,15 @@ public class TasksetDisplay extends BoxPanel implements Observer, UpdateListener
revalidate();
}
+ // Add empty if exists
+ if (empty.isPresent()) {
+ add(empty.get());
+ revalidate();
+ }
+
// This section fixes the offset from
// the lowest priority task to the Southern border.
- int taskOffset = priorities.size()*35;
+ int taskOffset = (empty.isPresent()) ? (priorities.size() + 1)*35 : priorities.size()*35;
if (offset - taskOffset > 0) {
setMaximumSize(new Dimension(300, 35 + taskOffset));
add(createVerticalStrut(offset - taskOffset));
@@ -70,12 +76,6 @@ public class TasksetDisplay extends BoxPanel implements Observer, UpdateListener
// Mark the previously marked one.
marked.ifPresent(taskGrid -> taskGrid.mark());
-
- // Add empty if exists
- if (empty.isPresent()) {
- add(empty.get());
- revalidate();
- }
}
/*
@@ -128,8 +128,7 @@ public class TasksetDisplay extends BoxPanel implements Observer, UpdateListener
emptyGrid.addEmptyListener(this);
empty = Optional.of(emptyGrid);
- add(emptyGrid);
- revalidate();
+ update(taskset, null);
}
}
--
GitLab