Skip to content
Snippets Groups Projects
Commit 1efd7c9e authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

[Bugfix] Text looks blurry on high resolution displays. 

Use sWT Label instead of FormText for labels.
parent b159086a
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/AdvancedModelPage.java
+ 13
− 23
View file @ 1efd7c9e
......@@ -16,12 +16,12 @@ import org.eclipse.swt.layout.GridLayout;
import org.eclipse.swt.widgets.Button;
import org.eclipse.swt.widgets.Composite;
import org.eclipse.swt.widgets.Control;
import org.eclipse.swt.widgets.Label;
import org.eclipse.swt.widgets.Spinner;
import org.eclipse.swt.widgets.Text;
import org.eclipse.ui.forms.IManagedForm;
import org.eclipse.ui.forms.IMessageManager;
import org.eclipse.ui.forms.editor.FormEditor;
import org.eclipse.ui.forms.widgets.FormText;
import org.eclipse.ui.forms.widgets.FormToolkit;
import org.eclipse.ui.forms.widgets.Section;
import org.eclipse.ui.forms.widgets.TableWrapData;
......@@ -803,8 +803,8 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
area.setLayout(new GridLayout(2, false));
// // label fp
// FormText fpLabel = toolkit.createFormText(area, true);
// fpLabel.setText("Fingerprint seed index:", false, false);
// Label fpLabel = toolkit.createLabel(area, "Fingerprint seed index:");
// fpLabel.setText(, false, false);
// gd = new GridData();
// gd.horizontalIndent = 10;
// fpLabel.setLayoutData(gd);
......@@ -830,8 +830,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
mcOption.setLayoutData(gd);
// label view
FormText viewLabel = toolkit.createFormText(area, true);
viewLabel.setText("View:", false, false);
Label viewLabel = toolkit.createLabel(area, "View:");
gd = new GridData();
gd.verticalAlignment = SWT.BEGINNING;
gd.horizontalIndent = 10;
......@@ -851,8 +850,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
gd.horizontalIndent = 10;
dfidOption.setLayoutData(gd);
// label depth
FormText dfidDepthLabel = toolkit.createFormText(area, true);
dfidDepthLabel.setText("Depth:", false, false);
Label dfidDepthLabel = toolkit.createLabel(area, "Depth:");
gd = new GridData();
gd.horizontalIndent = 10;
dfidDepthLabel.setLayoutData(gd);
......@@ -870,8 +868,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
simulationOption.addFocusListener(focusListener);
// label depth
FormText depthLabel = toolkit.createFormText(area, true);
depthLabel.setText("Maximum length of the trace:", false, false);
Label depthLabel = toolkit.createLabel(area, "Maximum length of the trace:");
gd = new GridData();
gd.horizontalIndent = 10;
depthLabel.setLayoutData(gd);
......@@ -883,8 +880,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
simuDepthText.addFocusListener(focusListener);
// label seed
FormText seedLabel = toolkit.createFormText(area, true);
seedLabel.setText("Seed:", false, false);
Label seedLabel = toolkit.createLabel(area, "Seed:");
gd = new GridData();
gd.horizontalIndent = 10;
seedLabel.setLayoutData(gd);
......@@ -897,8 +893,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
simuSeedText.addFocusListener(focusListener);
// label seed
FormText arilLabel = toolkit.createFormText(area, true);
arilLabel.setText("Aril:", false, false);
Label arilLabel = toolkit.createLabel(area, "Aril:");
gd = new GridData();
gd.horizontalIndent = 10;
arilLabel.setLayoutData(gd);
......@@ -916,8 +911,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
toolkit.createComposite(area);
// label fp
FormText fpLabel = toolkit.createFormText(area, true);
fpLabel.setText("Fingerprint seed index:", false, false);
Label fpLabel = toolkit.createLabel(area, "Fingerprint seed index:");
gd = new GridData();
gd.horizontalIndent = 0;
fpLabel.setLayoutData(gd);
......@@ -939,8 +933,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
fpIndexSpinner.addFocusListener(focusListener);
// fpbits label
FormText fpBitsLabel = toolkit.createFormText(area, true);
fpBitsLabel.setText("Log base 2 of number of disk storage files:", false, false);
Label fpBitsLabel = toolkit.createLabel(area, "Log base 2 of number of disk storage files:");
gd = new GridData();
gd.horizontalIndent = 0;
fpBitsLabel.setLayoutData(gd);
......@@ -963,8 +956,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
fpBits.setSelection(defaultFPBits);
// maxSetSize label
FormText maxSetSizeLabel = toolkit.createFormText(area, true);
maxSetSizeLabel.setText("Cardinality of largest enumerable set:", false, false);
Label maxSetSizeLabel = toolkit.createLabel(area, "Cardinality of largest enumerable set:");
gd = new GridData();
gd.horizontalIndent = 0;
maxSetSizeLabel.setLayoutData(gd);
......@@ -987,8 +979,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
maxSetSize.setSelection(defaultMaxSetSize);
// Extra/Additional VM arguments and system properties
FormText vmArgsLabel = toolkit.createFormText(area, true);
vmArgsLabel.setText("JVM arguments:", false, false);
toolkit.createLabel(area, "JVM arguments:");
extraVMArgumentsText = toolkit.createText(area, "", SWT.MULTI | SWT.WRAP);
extraVMArgumentsText.setEditable(true);
......@@ -1003,8 +994,7 @@ public class AdvancedModelPage extends BasicFormPage implements IConfigurationCo
extraVMArgumentsText.setLayoutData(gd);
// Extra/Additional TLC arguments
FormText tlcParamsLabel = toolkit.createFormText(area, true);
tlcParamsLabel.setText("TLC command line parameters:", false, false);
toolkit.createLabel(area, "TLC command line parameters:");
extraTLCParametersText = toolkit.createText(area, "", SWT.MULTI | SWT.WRAP);
extraTLCParametersText.setEditable(true);
......
org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/ui/editor/page/MainModelPage.java
+ 1709
− 1719
View file @ 1efd7c9e
......@@ -59,7 +59,6 @@ import org.eclipse.ui.forms.editor.FormEditor;
import org.eclipse.ui.forms.events.HyperlinkAdapter;
import org.eclipse.ui.forms.events.HyperlinkEvent;
import org.eclipse.ui.forms.widgets.ExpandableComposite;
import org.eclipse.ui.forms.widgets.FormText;
import org.eclipse.ui.forms.widgets.FormToolkit;
import org.eclipse.ui.forms.widgets.Hyperlink;
import org.eclipse.ui.forms.widgets.ImageHyperlink;
......@@ -178,7 +177,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
// The widgets to display the checkpoint size and
// the delete button.
private FormText chkpointSizeLabel;
private Label chkpointSizeLabel;
private Text checkpointSizeText;
private Button chkptDeleteButton;
......@@ -1138,8 +1137,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
elementLine.setLayout(new FillLayout(SWT.HORIZONTAL));
// the text
FormText labelText = toolkit.createFormText(elementLine, false);
labelText.setText("Advanced parts of the model:", false, false);
toolkit.createLabel(elementLine, "Advanced parts of the model:");
// the hyperlinks
Hyperlink hyper;
......@@ -1190,8 +1188,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
*/
// label workers
FormText workersLabel = toolkit.createFormText(howToRunArea, true);
workersLabel.setText("Number of worker threads:", false, false);
toolkit.createLabel(howToRunArea, "Number of worker threads:");
// field workers
workers = new Spinner(howToRunArea, SWT.NONE);
......@@ -1214,8 +1211,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
*/
// max heap size label
FormText maxHeapLabel = toolkit.createFormText(howToRunArea, true);
maxHeapLabel.setText("Fraction of physical memory allocated to TLC:", false, false);
toolkit.createLabel(howToRunArea, "Fraction of physical memory allocated to TLC:");
// Create a composite inside the right "cell" of the "how to run"
// section grid layout to fit the scale and the maxHeapSizeFraction
......@@ -1243,10 +1239,10 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
dm.bindAttribute(LAUNCH_MAX_HEAP_SIZE, maxHeapSize, howToRunPart);
// label next to the scale showing the current fraction selected
final FormText maxHeapSizeFraction = toolkit.createFormText(maxHeapScale, false);
final TLCRuntime instance = TLCRuntime.getInstance();
long memory = instance.getAbsolutePhysicalSystemMemory(defaultMaxHeapSize / 100d);
maxHeapSizeFraction.setText(defaultMaxHeapSize + "%" + " (" + memory + " mb)", false, false);
final Label maxHeapSizeFraction = toolkit.createLabel(maxHeapScale,
defaultMaxHeapSize + "%" + " (" + memory + " mb)");
maxHeapSize.addPaintListener(new PaintListener() {
/* (non-Javadoc)
* @see org.eclipse.swt.events.PaintListener#paintControl(org.eclipse.swt.events.PaintEvent)
......@@ -1256,14 +1252,13 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
int value = ((Scale) e.getSource()).getSelection();
final TLCRuntime instance = TLCRuntime.getInstance();
long memory = instance.getAbsolutePhysicalSystemMemory(value / 100d);
maxHeapSizeFraction.setText(value + "%" + " (" + memory + " mb)" , false, false);
maxHeapSizeFraction.setText(value + "%" + " (" + memory + " mb)");
}
});
// // label workers
// FormText workersLabel = toolkit.createFormText(howToRunArea, true);
// workersLabel.setText("Number of worker threads:", false, false);
// toolkit.createLabel(howToRunArea, "Number of worker threads:");
//
// // field workers
// workers = toolkit.createText(howToRunArea, "1");
......@@ -1293,8 +1288,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
checkpointButton.addFocusListener(focusListener);
HelpButton.helpButton(ckptComp, "model/overview-page.html#checkpoint") ;
FormText chkpointIdLabel = toolkit.createFormText(howToRunArea, true);
chkpointIdLabel.setText("Checkpoint ID:", false, false);
toolkit.createLabel(howToRunArea, "Checkpoint ID:");
checkpointIdText = toolkit.createText(howToRunArea, "");
checkpointIdText.setEditable(false);
......@@ -1304,8 +1298,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
checkpointIdText.setLayoutData(gd);
dm.bindAttribute(LAUNCH_RECOVER, checkpointButton, howToRunPart);
chkpointSizeLabel = toolkit.createFormText(howToRunArea, true);
chkpointSizeLabel.setText("Checkpoint size (kbytes):", false, false);
chkpointSizeLabel = toolkit.createLabel(howToRunArea, "Checkpoint size (kbytes):");
checkpointSizeText = toolkit.createText(howToRunArea, "");
gd = new GridData();
gd.horizontalIndent = 10;
......@@ -1407,8 +1400,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
networkInterface.setLayoutData(gd);
// label
FormText networkInterfaceLabel = toolkit.createFormText(networkInterface, true);
networkInterfaceLabel.setText("Master's network address:", false, false);
toolkit.createLabel(networkInterface, "Master's network address:");
// field
networkInterfaceCombo = new Combo(networkInterface, SWT.NONE);
......@@ -1492,8 +1484,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
distributedFPSetCount.setLayoutData(gd);
// label
FormText distributedFPSetCountLabel = toolkit.createFormText(distributedFPSetCount, true);
distributedFPSetCountLabel.setText("Number of distributed fingerprint sets (zero for single built-in set):", false, false);
toolkit.createLabel(distributedFPSetCount, "Number of distributed fingerprint sets (zero for single built-in set):");
// field
distributedFPSetCountSpinner = new Spinner(distributedFPSetCount, SWT.NONE);
......@@ -1581,8 +1572,7 @@ public class MainModelPage extends BasicFormPage implements IConfigurationConsta
/*
* pre-flight script executed prior to distributed TLC (e.g. to start remote workers)
*/
FormText distributedLabel = toolkit.createFormText(howToRunArea, true);
distributedLabel.setText("Pre Flight Script:", false, false);
final Label distributedLabel = toolkit.createLabel(howToRunArea, "Pre Flight Script:");
// non-editable text input
distributedScriptText = toolkit.createText(howToRunArea, "");
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment