diff options
| author | kr.angelov <kr.angelov@gmail.com> | 2014-07-03 18:27:39 +0000 |
|---|---|---|
| committer | kr.angelov <kr.angelov@gmail.com> | 2014-07-03 18:27:39 +0000 |
| commit | 7ad2f7dac33a57692495fecf10e1467e303e45d4 (patch) | |
| tree | c1b46fe4ba2618f2f5cd6b0fae0600e6e62686b5 | |
| parent | aa746ad0f646351fbdcfe279324cd9175d9c44e0 (diff) | |
filter out the leading +/* from the parser tree
| -rw-r--r-- | src/ui/android/src/org/grammaticalframework/ui/android/AlternativesActivity.java | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/src/ui/android/src/org/grammaticalframework/ui/android/AlternativesActivity.java b/src/ui/android/src/org/grammaticalframework/ui/android/AlternativesActivity.java index 1815fbf54..89bf92ac6 100644 --- a/src/ui/android/src/org/grammaticalframework/ui/android/AlternativesActivity.java +++ b/src/ui/android/src/org/grammaticalframework/ui/android/AlternativesActivity.java @@ -147,7 +147,18 @@ public class AlternativesActivity extends ListActivity { } Object[] brackets = mTranslator.bracketedLinearize(ep.getExpr()); - parseView.setBrackets(brackets); + if (brackets[0] instanceof Bracket) { + Bracket b = (Bracket) brackets[0]; + if (b.children[0].equals("*") || + b.children[0].equals("+")) { + Object[] children = new Object[b.children.length-1]; + for (int i = 1; i < b.children.length; i++) + children[i-1] = b.children[i]; + b = new Bracket(b.cat, b.fun, b.fid, b.lindex, children); + brackets[0] = b; + } + } + parseView.setBrackets(brackets); expandedView = view; } |
