From 225d9cb1462cbabae32d34f8fb40830daf2334f4 Mon Sep 17 00:00:00 2001
From: Letitia Li <leli@enst.fr>
Date: Fri, 2 Oct 2015 10:13:29 +0000
Subject: [PATCH] Fixed some Pragma bugs
---
src/ui/avatarbd/AvatarBDPragma.java | 4 +++-
src/ui/window/JDialogPragma.java | 11 +++++++----
2 files changed, 10 insertions(+), 5 deletions(-)
diff --git a/src/ui/avatarbd/AvatarBDPragma.java b/src/ui/avatarbd/AvatarBDPragma.java
index 2038709998..12e507491d 100755
--- a/src/ui/avatarbd/AvatarBDPragma.java
+++ b/src/ui/avatarbd/AvatarBDPragma.java
@@ -121,7 +121,7 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
removable = true;
name = "Proverif Pragma";
- value = "Proverif List of Pragma";
+ value = "";
myImageIcon = IconManager.imgic6000;
}
@@ -160,6 +160,8 @@ public class AvatarBDPragma extends TGCScalableWithoutInternalComponent {
Color c = g.getColor();
int desiredWidth = minWidth;
+ desiredWidth = Math.max(desiredWidth, g.getFontMetrics().stringWidth("Property Pragma") + marginX);
+
for(int i=0; i< values.length; i++) {
desiredWidth = Math.max(desiredWidth, g.getFontMetrics().stringWidth(values[i]) + marginX);
}
diff --git a/src/ui/window/JDialogPragma.java b/src/ui/window/JDialogPragma.java
index 8bb53ac74b..f0f336973e 100755
--- a/src/ui/window/JDialogPragma.java
+++ b/src/ui/window/JDialogPragma.java
@@ -88,7 +88,9 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
popupMenu.setOpaque(false);
popupMenu.setBorder(null);
popupMenu.add(list = createSuggestionList(position, subWord), BorderLayout.CENTER);
+ if (list.getModel().getSize() >0){
popupMenu.show(textarea, location.x, textarea.getBaseline(0, 0) + location.y);
+ }
}
public void hide() {
@@ -141,7 +143,7 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
}
public void moveUp() {
- int index = Math.min(list.getSelectedIndex() - 1, 0);
+ int index = Math.max(list.getSelectedIndex() - 1, 0);
selectIndex(index);
}
@@ -196,7 +198,7 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
return;
}
final String subWord = text.substring(start, position);
- if (subWord.length() < 2) {
+ if (subWord.length() < 1) {
return;
}
suggestion = new SuggestionPanel(textarea, position, subWord, location);
@@ -258,11 +260,12 @@ public class JDialogPragma extends javax.swing.JDialog implements ActionListener
suggestion.moveDown();
} else if (e.getKeyCode() == KeyEvent.VK_UP && suggestion != null) {
suggestion.moveUp();
- } else if (Character.isLetterOrDigit(e.getKeyChar())) {
- showSuggestionLater();
} else if (Character.isWhitespace(e.getKeyChar())) {
hideSuggestion();
}
+ else if (Character.isLetter(e.getKeyChar()) || e.getKeyChar()=='#'){
+ showSuggestionLater();
+ }
}
@Override
--
GitLab