]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/app/src/main/java/com/example/furt/myapplication/GenericFormula.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / app / src / main / java / com / example / furt / myapplication / GenericFormula.java
diff --git a/mainActivity/app/src/main/java/com/example/furt/myapplication/GenericFormula.java b/mainActivity/app/src/main/java/com/example/furt/myapplication/GenericFormula.java
new file mode 100644 (file)
index 0000000..b2136ab
--- /dev/null
@@ -0,0 +1,83 @@
+package com.example.furt.myapplication;
+
+import android.graphics.Paint;
+import android.graphics.Rect;
+
+import java.util.ArrayList;
+import java.util.List;
+
+public class GenericFormula implements Formula
+{
+    Paint p=new Paint();
+    int priority;
+    public String Draw(int p)
+    {
+        return "?";
+    } //la GenericFormula non può essere rappresentata
+    public String toString(){return Draw(0);}
+    public float size(){
+        p.setTextSize(DrawActivity.textSize);
+        return p.measureText(toString())+(float)(p.measureText(toString())*0.20);//ritorna la misura effettuata dalla classe Paint con un padding del 20% per migliorare la stima
+    }
+    public float sizeDeleted()
+    {
+        p.setTextSize(DrawActivity.textSize);
+        return p.measureText(toStringDeleted())+(float)(p.measureText(toStringDeleted())*0.20); //ritorna la misura effettuata dalla classe Paint con un padding del 20% per migliorare la stima
+    }
+    public String toStringDeleted()
+    {
+        return "["+toString()+"]";
+    }
+    public float height()
+    {
+        p.setTextSize(DrawActivity.textSize);
+        Rect bounds=new Rect();
+        p.getTextBounds(toString(),0,toString().length(),bounds);
+        return (float)((bounds.height()+((float)0.20*bounds.height()))*1.5); //l'altezza della formula va moltiplicata per l'inverso della densità dello schermo (circa 1.5)
+    }
+    public List<IntroductionRule> introductionRules(){
+        List<IntroductionRule> rules=new ArrayList<IntroductionRule>();
+        Node thisNode=new Node(this);
+        RuleIntroduction RAA=new RuleIntroduction("RAA",0);                        //R.A.A.
+        Node RAAnode=new Node(new FormulaBOT());                            //Formula=Bottom
+        List<Formula> RAAhp=new ArrayList<Formula>();                             //Tutte le ipotesi del nodo precedente
+        RAAhp.add(new FormulaNot(this));                                    //Più la negazione del nodo attuale
+        RAAnode.addHPFormula(RAAhp,true);
+        thisNode.addChild(RAAnode);
+        RAA.tempRule=thisNode;
+        rules.add(RAA);
+        /*
+        Node thisFakeNode=new Node(this);
+        RuleIntroduction fakeRAA=new RuleIntroduction("RAA",0,true);                        //fake R.A.A.
+        Node fakeRAAnode=new Node(new FormulaNot(this));                            //Formula=!F
+        thisFakeNode.addChild(fakeRAAnode);
+        fakeRAA.tempRule=thisFakeNode;
+        rules.add(fakeRAA);
+        */
+        return rules;
+    }
+    public List<EliminationRule> EliminationRules(){
+        List<EliminationRule> nodes=new ArrayList<EliminationRule>();
+        return nodes;
+    }
+
+    @Override
+    public boolean Fill(Formula F) {
+        return false;
+    }
+
+    @Override
+    public boolean setCursor() {
+        return false;
+    }
+
+    @Override
+    public Formula duplicate() {
+        return null;
+    }
+
+    @Override
+    public Object clone() throws CloneNotSupportedException {
+        return super.clone();
+    }
+}