]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/Node.java
Ported to latest version of Android SDK
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / Node.java
diff --git a/mainActivity/src/com/example/furt/myapplication/Node.java b/mainActivity/src/com/example/furt/myapplication/Node.java
deleted file mode 100755 (executable)
index 0a39fdf..0000000
+++ /dev/null
@@ -1,436 +0,0 @@
-package com.example.furt.myapplication;
-
-import android.graphics.Color;
-import android.util.TypedValue;
-import android.view.Gravity;
-import android.view.View;
-import android.view.ViewGroup;
-import android.view.ViewTreeObserver;
-import android.widget.RelativeLayout;
-import android.widget.TextView;
-
-import java.util.ArrayList;
-import java.util.List;
-
-
-public class Node implements Tree {
-
-    static int FIELD_UNSET = -1;
-    static int OPEN=0;
-    static int FAKE=1;
-    static int CLOSED=2;
-    static int FAKE_CLOSED=3;
-    static int CANCELED=4;
-    static int FAKE_CANCELED=5;
-
-    Formula F; //formula legata al nodo
-    String ruleName; //nome della regola associata a questo nodo
-    List<Node> Children = new ArrayList<Node>(); //Nodi figli
-    List<Hypothesis> NodeHP = new ArrayList<Hypothesis>(); //ipotesi associate
-    Node Father; //puntatore al padre
-    View.OnClickListener handler; //touchHandler per far comparire il pop-up delle regole
-    View.OnLongClickListener longHandler; //touchHandler per far comparire il menu con tutte le regole
-    boolean hasFocus; //indica se questo nodo è quello selezionato
-    int status; //stato del nodo (chiuso, aperto,fake...)
-    RelativeLayout global; //layout in cui si trova l'albero
-    BorderedTextView view; //view contenente questo oggetto
-    TextView ruleView; //view contenente l'intestazione della regola
-
-    float baseLine; //baseLine del Node: corrisponde alla lunghezza dell'overline
-    float leftOffset; //leftOffset: corrisponde alla larghezza della porzione di albero a sinistra del nodo
-    float rightOffset; //rightOffset: porzione di albero a destra del nodo
-    float maxWidth; //larghezza del sottoalbero di questo nodo (comprensiva del nodo stesso)
-
-    Node(Formula F) {
-        this.F = F;
-        view = null;
-        handler = null;
-        ruleName="";
-        Father = null;
-        status=OPEN;
-        hasFocus = false;
-        leftOffset = 0;
-        rightOffset = 0;
-        baseLine = getBaseWidth();
-        maxWidth = baseLine;
-    }
-
-    /**************SetView**************+*****/
-    /*****************************************/
-    /*******Setta la TextView del node  ******/
-    /** e il layout in cui deve comparire  ***/
-    /*****************************************/
-
-    public void setView(BorderedTextView t,RelativeLayout r) {
-        view = t;
-        ruleView =new TextView(t.getContext());
-        global=r;
-    }
-
-
-    /**************Count****************+*****/
-    /*****************************************/
-    /*******Restituisce il numero di    ******/
-    /*************nodi dell'albero ***********/
-    /*****************************************/
-
-    int count()
-    {
-        int ris=1;
-        for (Node n:Children)
-            ris+=n.count();
-        return ris;
-    }
-    /**************addHP****************+*****/
-    /*****************************************/
-    /*******Metodi per aggiungere ipotesi*****/
-    /*******sotto forma di Hypothesis o di****/
-    /*************Formula*********************/
-    /*****************************************/
-
-    public void addHPFormula(List<Formula>List,boolean deleted) {
-        loop:for (Formula newHp:List) {
-            for (Hypothesis oldHp: NodeHP) {
-                if (oldHp.HP.toString().equals(newHp.toString())) { //ipotesi già presente: passo alla prossima
-                    continue loop;
-                }
-            }
-            NodeHP.add(new Hypothesis(newHp, deleted));
-        }
-    }
-
-    public void addHPList(List<Hypothesis>List) {
-        loop:for (Hypothesis newHp:List) {
-            for (Hypothesis oldHp: NodeHP) {
-                if (oldHp.HP.toString().equals(newHp.HP.toString())) { //ipotesi già presente: passo alla prossima
-                    continue loop;
-                }
-            }
-            Hypothesis copyHP=new Hypothesis(newHp.HP, newHp.isDeleted);
-            copyHP.fromNode=newHp.fromNode;
-            NodeHP.add(copyHP);
-        }
-    }
-
-    /*****************************************/
-    /******* Algoritmo di ricerca del ********/
-    /******* focus: restituisce false ********/
-    /******* se la dimostrazione è completa***/
-
-    public boolean searchFocus(Node caller)
-    {
-        if (Children.size()==0) //caso base: controllo se il focus può essere su di me
-        {
-            if (status!=OPEN && status!=FAKE) //nodo chiuso: il focus non può essere su di me
-                return false;
-            hasFocus=true;                             //posso assumere il focus
-            if (handler!=null)
-                handler.onClick(view);
-            return true;
-        }
-        //passo induttivo: vado su tutti i miei figli, poi su mio padre. Termino se il padre è null.
-        for (Node n:Children) {
-            if (caller != null)
-                if (n == caller) //per ogni figlio diverso dal chiamante
-                {
-                    continue;
-                }
-            if(n.searchFocus(null))
-                return true;
-        }
-        if (caller==null) //ero stato chiamato da mio padre: è inutile richiamarlo
-            return false;
-        else if (Father==null)
-            return false; //padre null: l'albero è dimostrato e non ci sono nodi a cui dare il focus.
-        else
-            return Father.searchFocus(this); //propaga il searchFocus sul padre
-    }
-    public void addChild(Node N) {
-        N.Father = this;
-        Children.add(N);
-        Node tmp=Father;
-        //c'è un nuovo nodo nell'albero: tutti i campi dell'algoritmo di disegno sono da ricalcolare per questo ramo
-        baseLine=FIELD_UNSET;
-        maxWidth=FIELD_UNSET;
-        leftOffset=FIELD_UNSET;
-        rightOffset=FIELD_UNSET;
-        while (tmp!=null)
-        {
-            tmp.baseLine=FIELD_UNSET;
-            tmp.leftOffset=FIELD_UNSET;
-            tmp.rightOffset=FIELD_UNSET;
-            tmp.maxWidth=FIELD_UNSET;
-            tmp=tmp.Father;
-        }
-    }
-
-    public float getBaseWidth() {
-        return F.size();
-    }
-
-    public float getMaxWidth() //ritorna la larghezza massima del sottoalbero
-    {
-        if (maxWidth!=FIELD_UNSET)
-            return maxWidth;
-        else
-            maxWidth=getLeftOffset()+getBaseWidth()+getRightOffset();
-        return (maxWidth);
-    }
-
-    public float getLineWidth()
-    {
-        if (baseLine!=FIELD_UNSET)
-            return baseLine;
-        else
-        {
-            baseLine=Math.max(getUpLine(),getBaseWidth()); //la baseline è il massimo valore tra la upLine e la baseWidth
-            return baseLine;
-        }
-    }
-    public float getUpLine() //calcola la upLine, ovvero la dimensione prevista del sottoalbero assumendo il nodo attuale di lunghezza unitaria
-    {
-        float spaceSize= DrawActivity.spaceSize;
-        if (Children.size()==0)
-            return(getBaseWidth());
-        int res=0;
-        for(Node n:Children)
-            res+=(n.getMaxWidth())+spaceSize;
-        res-=spaceSize;
-        res-=Children.get(0).getLeftOffset(); //la linea deve fermarsi all'inizio della formula del primo figlio sinistro
-        res-=Children.get(Children.size()-1).getRightOffset(); //la linea deve finire alla fine della formula dell'ultimo figlio destro
-        return res;
-    }
-
-    /**Calcolo del leftOffset
-     * esso è uguale al leftOffset del primo figlio, a cui aggiungere la porzione di overline a sinistra della formula del nodo
-     * o rimuovere la mezza differenza tra la baseWidth e la upLine. Se il leftOffset risulterebbe negativo, diventa nullo.
-     */
-
-    public float getLeftOffset() {
-        if (leftOffset != FIELD_UNSET) {
-            return leftOffset;
-        }
-        else {
-            if (Children.size() == 0) //foglia
-                leftOffset=0;
-            else
-                leftOffset=Math.max(Children.get(0).getLeftOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
-            return leftOffset;
-        }
-    }
-
-    public float getRightOffset()
-    {
-        if (rightOffset!=FIELD_UNSET)
-            return rightOffset;
-        else {
-            if (Children.size() == 0) //foglia
-                rightOffset=0;
-            else
-                rightOffset=Math.max(Children.get(Children.size() - 1).getRightOffset() + ((getUpLine() - getBaseWidth()) / 2),0);
-            return rightOffset;
-        }
-    }
-
-    public float getMaxHeight() //calcolo dell'altezza massima dell'albero attuale.
-    {
-        float baseRes=F.height();
-        float res=baseRes;
-        for (Node n:Children)
-        {
-            float tempH=n.getMaxHeight()+baseRes;
-            if(tempH>res)
-                res=tempH;
-        }
-        return res;
-    }
-
-    void Refactor() //metodo di supporto: svuota i campi dell'intero sottoalbero che verranno ricalcolati dall'algoritmo alla prossima applicazione
-    {
-        baseLine=FIELD_UNSET;
-        leftOffset=FIELD_UNSET;
-        rightOffset=FIELD_UNSET;
-        maxWidth=FIELD_UNSET;
-        for(Node n:Children)
-            n.Refactor();
-    }
-
-
-    public void Clean() //metodo di supporto: rimuove dal layout legato al Node tutte le view presenti
-    {
-        global.removeAllViews();
-    }
-
-    public boolean isCorrect() //controlla per l'intero sottoalbero se esso è privo di nodi fake.
-    {
-        if (status==FAKE || status==FAKE_CANCELED || status==FAKE_CLOSED)
-            return false;
-        else for (Node n:Children)
-            if (!n.isCorrect())
-                return false;
-        return true;
-
-    }
-
-    public void Draw()
-    {
-        float interval=0; //intervallo di spazio da sommare nella creazione dei figli
-        float spaceSize= DrawActivity.spaceSize; //dimensione della spaziatura tra i sottoalberi
-        int childNo=Children.size(); //numero di figli del nodo attuale
-        if (childNo==0) //foglia: possibile ramo dimostrato
-
-        {
-            view.setBorders(null); //le foglie non hanno overline
-            if (status!=OPEN && status!=FAKE) { //nodo chiuso
-                view.setTextColor(Color.GRAY);
-                if (hasFocus) //avevo il focus: provo a darlo ad uno dei miei fratelli
-                {
-                    if (!(Father.searchFocus(this))) { //focus inapplicabile nell'albero: dimostrazione completata.
-                        DrawActivity.finishedTree(view.getContext());
-                        return;
-                    }
-                    hasFocus = false;
-                }
-                if (status==CANCELED || status==FAKE_CANCELED) { //nodo cancellato
-                    view.setWidth((int) F.sizeDeleted());
-                    view.setText(F.toStringDeleted());
-                    view.setOnClickListener(null); //rimuove eventuali listener per evitare il proseguimento dell'albero
-                    /**NOTA: è possibile permettere all'utente di proseguire la dimostrazione
-                     * di un ramo chiuso commentando la riga precedente e aggiungendo nel touchnodeHandler
-                     * un'controllo che, in caso di nodo chiuso cliccato, lo riapre e gli riaffida il focus.
-                     */
-                }
-                return;
-            }
-            if (hasFocus && DrawActivity.selectedNode!=this)
-                handler.onClick(view);
-            else if (hasFocus) //hasFocus: must be colored red anyway
-                view.setTextColor(Color.RED);
-            return;
-        }
-
-        ruleView.setText(ruleName);
-        ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
-        RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
-        intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
-        intlp.addRule(RelativeLayout.ABOVE,view.getId());
-        ruleView.setLayoutParams(intlp);
-        global.addView(ruleView);
-
-        hasFocus=false; //se sono arrivato a questo punto il nodo non è una foglia e non può avere il focus di default
-
-        for (int i=0;i<childNo;i++) {
-            final Node newChild=Children.get(i); //recupero l'i-esimo figlio
-            RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
-            final BorderedTextView childView=new BorderedTextView(view.getContext());
-            childView.setBorders(DrawActivity.b);
-            lp.addRule(RelativeLayout.ABOVE, view.getId());
-            if (i==0) //first child
-            {
-                float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0); //il primo figlio è posizionato a sinistra del padre, con un ulteriore offset
-                                                                                                               // sinistro pari allo scarto della sua overline
-                if (getLineWidth()>getUpLine()) //sono più grande dell'overline prevista: aggiungo un ulteriore offset al figlio
-                    leftPos+=((getLineWidth()-getUpLine())/2);
-                lp.setMargins(Math.round(leftPos), 0, 0, 0); //leftPos è il margine sinistro del figlio
-                childView.setLeft(Math.round(leftPos));
-            }
-            else {
-                lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0); //figlio intermedio: basta aggiungere l'interval alla posizione sinistra del padre
-                childView.setLeft(Math.round(view.getLeft() + interval));
-            }
-            childView.setLayoutParams(lp);
-            childView.setId(DrawActivity.globalId++);
-            childView.setText(newChild.F.toString());
-            childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
-            childView.setGravity(Gravity.CENTER); //formula al centro della sua overline
-            childView.setWidth(Math.round(newChild.getLineWidth()));
-            global.addView(childView);
-            childView.getViewTreeObserver().addOnGlobalLayoutListener(new ViewTreeObserver.OnGlobalLayoutListener() {
-                @Override
-                public void onGlobalLayout() {
-                    newChild.setView(childView,global);
-                    if(newChild.handler==null)
-                        newChild.handler=new touchnodeHandler(newChild);
-                    newChild.longHandler=new longnodeHandler(newChild);
-                    newChild.view.setOnClickListener(newChild.handler);
-                    newChild.view.setOnLongClickListener(newChild.longHandler);
-                    childView.getViewTreeObserver().removeOnGlobalLayoutListener(this);
-                    newChild.Draw();
-                }
-            });
-            if (i!=childNo-1) //l'ultimo figlio non ha intervalli
-            {
-                float leftOverflow=Math.max((Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2,0);
-                interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow)); //devo aggiungere all'interval la basewidth del figlio attuale, il rightoffset del figlio attuale e il leftOffset del figlio successivo.
-                interval+=spaceSize;
-                if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
-                    interval+=newChild.getLeftOffset();
-            }
-        }
-    }
-    void Resize() //metodo per ridisegnare l'albero dopo un pinch zoom: l'algoritmo applicato è uguale a quello del metodo Draw()
-    {
-        int i;
-        float interval=0; //intervallo di spazio da sommare nella creazione dei figli
-        float spaceSize= DrawActivity.spaceSize;
-        int childNo=Children.size();
-        if (childNo!=0)
-        {
-
-            ruleView.setText(ruleName);
-            ruleView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize / 2);
-            RelativeLayout.LayoutParams intlp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
-            intlp.addRule(RelativeLayout.RIGHT_OF,view.getId());
-            int sum=0;
-            sum+=F.height();
-            Node tmp=Father;
-            while (tmp!=null)
-            {
-                sum+=tmp.F.height();
-                tmp=tmp.Father;
-            }
-            intlp.setMargins(0,0,0,sum);
-            intlp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM);
-            ruleView.setLayoutParams(intlp);
-        }
-        for (i=0;i<childNo;i++) {
-            Node newChild=Children.get(i);
-            RelativeLayout.LayoutParams lp=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
-            TextView childView=Children.get(i).view;
-            lp.addRule(RelativeLayout.ABOVE,view.getId());
-            if (i==0) //first child
-            {
-                float leftPos= view.getLeft()-Math.max((newChild.getLineWidth()-newChild.getBaseWidth())/2,0);
-                if (getLineWidth()>getUpLine())
-                    leftPos+=((getLineWidth()-getUpLine())/2);
-                lp.setMargins(Math.round(leftPos), 0, 0, 0);
-                childView.setLeft(Math.round(leftPos));
-            }
-            else {
-                lp.setMargins(Math.round(view.getLeft() + interval), 0, 0, 0);
-                childView.setLeft(Math.round(view.getLeft() + interval));
-            }
-            childView.setLayoutParams(lp);
-            childView.setTextSize(TypedValue.COMPLEX_UNIT_PX, DrawActivity.textSize);
-
-            if(newChild.status==CANCELED || newChild.status==FAKE_CANCELED)
-                childView.setWidth((int) ((newChild.F.sizeDeleted())));
-            else
-                childView.setWidth(Math.round(newChild.getLineWidth()));
-
-            newChild.Resize();
-
-            if (i!=childNo-1) //l'ultimo figlio non ha intervalli
-            {
-                float leftOverflow=(Children.get(i+1).getLineWidth()-Children.get(i+1).getBaseWidth())/2;
-                interval += (newChild.getBaseWidth()+newChild.getRightOffset()+Children.get(i+1).getLeftOffset()-(leftOverflow));
-                interval+=spaceSize;
-                if (i!=0) //devo sommare anche il leftOverflow del nuovo figlio
-                    interval+=newChild.getLeftOffset();
-            }
-
-        }
-
-    }
-
-}