mirror of
https://github.com/hneemann/Digital.git
synced 2025-09-19 09:54:49 -04:00
added a special style for text in inputs and outputs
This commit is contained in:
parent
3b406a3a8d
commit
076c193d46
@ -156,7 +156,7 @@ public class GraphicSVG implements Graphic {
|
||||
if (text == null || text.length() == 0) return;
|
||||
|
||||
try {
|
||||
text = formatText(text, style.getFontSize());
|
||||
text = formatText(text, style);
|
||||
|
||||
boolean rotateText = false;
|
||||
if (p1.y == p2.y) { // 0 and 180 deg
|
||||
@ -196,11 +196,11 @@ public class GraphicSVG implements Graphic {
|
||||
* Is used by drawText to format the given text to SVG.
|
||||
* This implementation only calls escapeXML(text).
|
||||
*
|
||||
* @param text the text
|
||||
* @param fontSize the fontsize
|
||||
* @param text the text
|
||||
* @param style the text style
|
||||
* @return the formatted text
|
||||
*/
|
||||
public String formatText(String text, int fontSize) {
|
||||
public String formatText(String text, Style style) {
|
||||
return escapeXML(text);
|
||||
}
|
||||
|
||||
|
@ -37,7 +37,7 @@ public class GraphicSVGIndex extends GraphicSVG {
|
||||
}
|
||||
|
||||
@Override
|
||||
public String formatText(String text, int fontSize) {
|
||||
public String formatText(String text, Style style) {
|
||||
text = text.replace('~', '\u00ac');
|
||||
return formatSVGIndex(escapeXML(formatIndex(cleanLabel(text))));
|
||||
}
|
||||
|
@ -85,7 +85,7 @@ public class GraphicSVGLaTeX extends GraphicSVG {
|
||||
}
|
||||
|
||||
@Override
|
||||
public String formatText(String text, int fontSize) {
|
||||
public String formatText(String text, Style style) {
|
||||
text = formatIndex(text);
|
||||
StringBuilder sb = new StringBuilder();
|
||||
boolean inMath = false;
|
||||
@ -121,8 +121,8 @@ public class GraphicSVGLaTeX extends GraphicSVG {
|
||||
}
|
||||
}
|
||||
text = sb.toString();
|
||||
if (fontSize != Style.NORMAL.getFontSize()) {
|
||||
final String fontSizeName = getFontSizeName(fontSize);
|
||||
if (style.getFontSize() != Style.NORMAL.getFontSize()) {
|
||||
final String fontSizeName = getFontSizeName(style.getFontSize());
|
||||
if (!fontSizeName.equals("normalsize"))
|
||||
text = "{\\" + fontSizeName + " " + text + "}";
|
||||
}
|
||||
|
@ -25,6 +25,10 @@ public final class Style {
|
||||
* used for all lines to draw the shapes itself
|
||||
*/
|
||||
public static final Style NORMAL = new Builder().build();
|
||||
/**
|
||||
* used for input and output labels
|
||||
*/
|
||||
public static final Style INOUT = new Builder(NORMAL).setFontStyle(Font.ITALIC).build();
|
||||
/**
|
||||
* used to draw the failed state lines in the measurement graph
|
||||
*/
|
||||
@ -141,6 +145,7 @@ public final class Style {
|
||||
private final BasicStroke stroke;
|
||||
private final Font font;
|
||||
private final boolean mattersForSize;
|
||||
private final int fontStyle;
|
||||
|
||||
/**
|
||||
* Creates a new style
|
||||
@ -152,11 +157,12 @@ public final class Style {
|
||||
this.filled = builder.filled;
|
||||
this.color = builder.color;
|
||||
this.fontSize = builder.fontSize;
|
||||
this.fontStyle = builder.fontStyle;
|
||||
this.dash = builder.dash;
|
||||
this.mattersForSize = builder.mattersForSize;
|
||||
|
||||
stroke = new BasicStroke(thickness, builder.endCap, BasicStroke.JOIN_MITER, 10f, dash, 0f);
|
||||
font = new Font("Arial", Font.PLAIN, fontSize);
|
||||
font = new Font("Arial", fontStyle, fontSize);
|
||||
}
|
||||
|
||||
/**
|
||||
@ -194,6 +200,13 @@ public final class Style {
|
||||
return fontSize;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the font style
|
||||
*/
|
||||
public int getFontStyle() {
|
||||
return fontStyle;
|
||||
}
|
||||
|
||||
/**
|
||||
* @return the font to use
|
||||
*/
|
||||
@ -284,6 +297,7 @@ public final class Style {
|
||||
private float[] dash = null;
|
||||
private boolean mattersForSize = false;
|
||||
private int endCap = BasicStroke.CAP_SQUARE;
|
||||
private int fontStyle = Font.PLAIN;
|
||||
|
||||
private Builder() {
|
||||
}
|
||||
@ -318,6 +332,11 @@ public final class Style {
|
||||
return this;
|
||||
}
|
||||
|
||||
private Builder setFontStyle(int fontStyle) {
|
||||
this.fontStyle = fontStyle;
|
||||
return this;
|
||||
}
|
||||
|
||||
private Builder setDash(float[] dash) {
|
||||
this.dash = dash;
|
||||
return this;
|
||||
@ -336,6 +355,7 @@ public final class Style {
|
||||
private Style build() {
|
||||
return new Style(this);
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -115,7 +115,7 @@ public class InputShape implements Shape {
|
||||
Vector center = new Vector(-LATEX_RAD.x, 0);
|
||||
graphic.drawCircle(center.sub(LATEX_RAD), center.add(LATEX_RAD), Style.NORMAL);
|
||||
Vector textPos = new Vector(-SIZE2 - LATEX_RAD.x, 0);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.RIGHTCENTER, Style.NORMAL);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.RIGHTCENTER, Style.INOUT);
|
||||
} else {
|
||||
Style style = Style.NORMAL;
|
||||
if (value != null) {
|
||||
@ -131,7 +131,7 @@ public class InputShape implements Shape {
|
||||
graphic.drawPolygon(new Polygon(true).add(-SIZE * 2 - 1, -SIZE).add(-1, -SIZE).add(-1, SIZE).add(-SIZE * 2 - 1, SIZE), Style.NORMAL);
|
||||
|
||||
Vector textPos = new Vector(-SIZE * 3, 0);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.RIGHTCENTER, Style.NORMAL);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.RIGHTCENTER, Style.INOUT);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -85,7 +85,7 @@ public class OutputShape implements Shape {
|
||||
Vector center = new Vector(LATEX_RAD.x, 0);
|
||||
graphic.drawCircle(center.sub(LATEX_RAD), center.add(LATEX_RAD), Style.NORMAL);
|
||||
Vector textPos = new Vector(SIZE2 + LATEX_RAD.x, 0);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.LEFTCENTER, Style.NORMAL);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.LEFTCENTER, Style.INOUT);
|
||||
} else {
|
||||
Style style = Style.NORMAL;
|
||||
if (value != null) {
|
||||
@ -100,7 +100,7 @@ public class OutputShape implements Shape {
|
||||
graphic.drawCircle(center.sub(RAD), center.add(RAD), style);
|
||||
graphic.drawCircle(center.sub(RADL), center.add(RADL), Style.NORMAL);
|
||||
Vector textPos = new Vector(SIZE * 3, 0);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.LEFTCENTER, Style.NORMAL);
|
||||
graphic.drawText(textPos, textPos.add(1, 0), label, Orientation.LEFTCENTER, Style.INOUT);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -10,9 +10,9 @@ public class GraphicSVGIndexTest extends TestCase {
|
||||
GraphicSVGIndex gs = new GraphicSVGIndex(System.out, null, 30);
|
||||
gs.setBoundingBox(new Vector(0, 0), new Vector(30, 30));
|
||||
|
||||
assertEquals("Z<tspan style=\"font-size:80%;baseline-shift:sub\">0</tspan>", gs.formatText("Z_0", 0));
|
||||
assertEquals("<a>", gs.formatText("<a>", 0));
|
||||
assertEquals("¬Z", gs.formatText("~Z", 0));
|
||||
assertEquals("Z<tspan style=\"font-size:80%;baseline-shift:sub\">0</tspan>", gs.formatText("Z_0", Style.NORMAL));
|
||||
assertEquals("<a>", gs.formatText("<a>", Style.NORMAL));
|
||||
assertEquals("¬Z", gs.formatText("~Z", Style.NORMAL));
|
||||
}
|
||||
|
||||
}
|
@ -12,22 +12,22 @@ public class GraphicSVGLaTeXTest extends TestCase {
|
||||
public void testFormatText() throws Exception {
|
||||
GraphicSVGLaTeX gs = new GraphicSVGLaTeX(System.out, null, 30);
|
||||
|
||||
assertEquals("$Z_0$", gs.formatText("$Z_0$", Style.NORMAL.getFontSize()));
|
||||
assertEquals("$Z_{in}$", gs.formatText("$Z_{in}$", Style.NORMAL.getFontSize()));
|
||||
assertEquals("Z$_{0}$", gs.formatText("Z_0", Style.NORMAL.getFontSize()));
|
||||
assertEquals("\\&", gs.formatText("&", Style.NORMAL.getFontSize()));
|
||||
assertEquals("$\\geq\\!\\!{}$1", gs.formatText("\u22651", Style.NORMAL.getFontSize()));
|
||||
assertEquals("$\\geq\\!\\!{}1$", gs.formatText("$\u22651$", Style.NORMAL.getFontSize()));
|
||||
assertEquals("$\\neg{}$Q", gs.formatText("~Q", Style.NORMAL.getFontSize()));
|
||||
assertEquals("$\\neg{}Q$", gs.formatText("$~Q$", Style.NORMAL.getFontSize()));
|
||||
assertEquals("\\textless{}a\\textgreater{}", gs.formatText("<a>", Style.NORMAL.getFontSize()));
|
||||
assertEquals("Grün", gs.formatText("Grün", Style.NORMAL.getFontSize()));
|
||||
assertEquals("$Z_0$", gs.formatText("$Z_0$", Style.NORMAL));
|
||||
assertEquals("$Z_{in}$", gs.formatText("$Z_{in}$", Style.NORMAL));
|
||||
assertEquals("Z$_{0}$", gs.formatText("Z_0", Style.NORMAL));
|
||||
assertEquals("\\&", gs.formatText("&", Style.NORMAL));
|
||||
assertEquals("$\\geq\\!\\!{}$1", gs.formatText("\u22651", Style.NORMAL));
|
||||
assertEquals("$\\geq\\!\\!{}1$", gs.formatText("$\u22651$", Style.NORMAL));
|
||||
assertEquals("$\\neg{}$Q", gs.formatText("~Q", Style.NORMAL));
|
||||
assertEquals("$\\neg{}Q$", gs.formatText("$~Q$", Style.NORMAL));
|
||||
assertEquals("\\textless{}a\\textgreater{}", gs.formatText("<a>", Style.NORMAL));
|
||||
assertEquals("Grün", gs.formatText("Grün", Style.NORMAL));
|
||||
|
||||
|
||||
assertEquals("{\\scriptsize Grün}", gs.formatText("Grün", Style.SHAPE_PIN.getFontSize()));
|
||||
assertEquals("{\\scriptsize Z$_{0}$}", gs.formatText("Z_0", Style.SHAPE_PIN.getFontSize()));
|
||||
assertEquals("{\\tiny Z$_{0}$}", gs.formatText("Z_0", 14));
|
||||
assertEquals("{\\tiny Z$_{0}$}", gs.formatText("Z_0", Style.WIRE_BITS.getFontSize()));
|
||||
assertEquals("{\\scriptsize Grün}", gs.formatText("Grün", Style.SHAPE_PIN));
|
||||
assertEquals("{\\scriptsize Z$_{0}$}", gs.formatText("Z_0", Style.SHAPE_PIN));
|
||||
assertEquals("{\\tiny Z$_{0}$}", gs.formatText("Z_0", Style.SHAPE_SPLITTER));
|
||||
assertEquals("{\\tiny Z$_{0}$}", gs.formatText("Z_0", Style.WIRE_BITS));
|
||||
}
|
||||
|
||||
public void testCleanLabel() throws IOException {
|
||||
@ -39,7 +39,7 @@ public class GraphicSVGLaTeXTest extends TestCase {
|
||||
|
||||
private void check(String orig, String clean, String LaTeX) throws IOException {
|
||||
GraphicSVGLaTeX gs = new GraphicSVGLaTeX(System.out, null, 30);
|
||||
assertEquals(LaTeX, gs.formatText(orig, Style.NORMAL.getFontSize()));
|
||||
assertEquals(LaTeX, gs.formatText(orig, Style.NORMAL));
|
||||
assertEquals(clean, ElementAttributes.cleanLabel(orig));
|
||||
}
|
||||
}
|
@ -10,8 +10,8 @@ public class GraphicSVGTest extends TestCase {
|
||||
GraphicSVG gs = new GraphicSVG(System.out, null, 30);
|
||||
gs.setBoundingBox(new Vector(0, 0), new Vector(30, 30));
|
||||
|
||||
assertEquals("Z0", gs.formatText("Z0", 0));
|
||||
assertEquals("<a>", gs.formatText("<a>", 0));
|
||||
assertEquals("Z0", gs.formatText("Z0", Style.NORMAL));
|
||||
assertEquals("<a>", gs.formatText("<a>", Style.NORMAL));
|
||||
}
|
||||
|
||||
}
|
Loading…
x
Reference in New Issue
Block a user