]> matita.cs.unibo.it Git - logicplayer.git/commitdiff
New version (to be tested).
authorClaudio Sacerdoti Coen <claudio@zenone.casamia.org>
Tue, 9 Dec 2014 14:39:48 +0000 (15:39 +0100)
committerClaudio Sacerdoti Coen <claudio@zenone.casamia.org>
Tue, 9 Dec 2014 14:39:48 +0000 (15:39 +0100)
43 files changed:
mainActivity/AndroidManifest.xml
mainActivity/res/menu/my.xml
mainActivity/src/com/example/furt/myapplication/BorderedTextView.java
mainActivity/src/com/example/furt/myapplication/CopyPasteDialog.java
mainActivity/src/com/example/furt/myapplication/DialogTouchHandler.java
mainActivity/src/com/example/furt/myapplication/DrawActivity.java
mainActivity/src/com/example/furt/myapplication/EliminationRule.java
mainActivity/src/com/example/furt/myapplication/Formula.java
mainActivity/src/com/example/furt/myapplication/FormulaAnd.java
mainActivity/src/com/example/furt/myapplication/FormulaBOT.java
mainActivity/src/com/example/furt/myapplication/FormulaImpl.java
mainActivity/src/com/example/furt/myapplication/FormulaNot.java
mainActivity/src/com/example/furt/myapplication/FormulaOr.java
mainActivity/src/com/example/furt/myapplication/FormulaTOP.java
mainActivity/src/com/example/furt/myapplication/GenericFormula.java
mainActivity/src/com/example/furt/myapplication/Hypothesis.java
mainActivity/src/com/example/furt/myapplication/IntroductionRule.java
mainActivity/src/com/example/furt/myapplication/Literal.java
mainActivity/src/com/example/furt/myapplication/LongHPClick.java
mainActivity/src/com/example/furt/myapplication/MD5.java
mainActivity/src/com/example/furt/myapplication/Node.java
mainActivity/src/com/example/furt/myapplication/RuleAndElimination.java
mainActivity/src/com/example/furt/myapplication/RuleBotElimination.java
mainActivity/src/com/example/furt/myapplication/RuleDialog.java
mainActivity/src/com/example/furt/myapplication/RuleImplElimination.java
mainActivity/src/com/example/furt/myapplication/RuleIntroduction.java
mainActivity/src/com/example/furt/myapplication/RuleNotElimination.java
mainActivity/src/com/example/furt/myapplication/RuleOrElimination.java
mainActivity/src/com/example/furt/myapplication/TwoDScrollView.java [deleted file]
mainActivity/src/com/example/furt/myapplication/UndefinedFormula.java
mainActivity/src/com/example/furt/myapplication/aggiorna.java
mainActivity/src/com/example/furt/myapplication/aggiornamento.java
mainActivity/src/com/example/furt/myapplication/askFormula.java
mainActivity/src/com/example/furt/myapplication/download_page.java
mainActivity/src/com/example/furt/myapplication/longnodeHandler.java [new file with mode: 0644]
mainActivity/src/com/example/furt/myapplication/mainActivity.java
mainActivity/src/com/example/furt/myapplication/parserDialog.java
mainActivity/src/com/example/furt/myapplication/recuperaPass.java
mainActivity/src/com/example/furt/myapplication/serverComunication.java
mainActivity/src/com/example/furt/myapplication/touchHPHandler.java
mainActivity/src/com/example/furt/myapplication/touchParserHandler.java
mainActivity/src/com/example/furt/myapplication/touchRuleHandler.java [deleted file]
mainActivity/src/com/example/furt/myapplication/touchnodeHandler.java

index 1e9366734167a557aa68293b904fc41aad081fc8..4eb25ff3316c03749726c32c8c60eb762319bb9d 100755 (executable)
@@ -30,6 +30,7 @@
             android:exported="false"/>
         <activity
             android:name=".download_page"
+            android:configChanges="orientation|screenSize">
             android:label="@string/listEs" >
         </activity>
         <activity
index 371dbf8c667cd208718bfe43077a7980fd7de0c9..74a83a17df023791aa129add5b5a8af9f1ef6511 100755 (executable)
@@ -1,10 +1,6 @@
 <menu xmlns:android="http://schemas.android.com/apk/res/android"
     xmlns:tools="http://schemas.android.com/tools"
     tools:context=".MyActivity" >
-    <item android:id="@+id/action_paste"
-        android:title="Incolla sottoalbero"
-        android:orderInCategory="100"
-        android:showAsAction="never" />
     <item android:id="@+id/abandon"
         android:title="Abbandona esercizio"
         android:orderInCategory="100"
index 846aeb1a790596cd50a0f6fc631fc70fb67f055a..40f3852dfb57236ac47d4a3c09286c976de5e15d 100755 (executable)
@@ -5,7 +5,6 @@ import android.graphics.Canvas;
 import android.graphics.Color;
 import android.graphics.Paint;
 import android.util.AttributeSet;
-import android.util.Log;
 import android.widget.TextView;
 
 public class BorderedTextView extends TextView {
index 520ec66ab1ba14e091148ef1d80d62c991805cb2..e40156f8118890692e6780302b78a66971cd590e 100755 (executable)
@@ -8,8 +8,11 @@ import android.os.Bundle;
 
 import java.util.ArrayList;
 
+/**CopyPasteDialog: dialog per la gestione delle operazioni di copia e cancellazione su
+ * nodi intermedi dell'albero
+ */
 public class CopyPasteDialog extends DialogFragment {
-    static Node thisNode;
+    Node thisNode; //nodo legato a questo Dialog
     public CopyPasteDialog(Node n)
     {
         thisNode=n;
@@ -20,19 +23,18 @@ public class CopyPasteDialog extends DialogFragment {
         builder.setMessage("Seleziona un'operazione:")
                 .setPositiveButton("Copia", new DialogInterface.OnClickListener() {
                     public void onClick(DialogInterface dialog, int id) {
-                        DrawActivity.copiedNode=thisNode;
+                        DrawActivity.copiedNode=thisNode; //il nodo viene copiato
                     }
                 });
             builder.setNeutralButton("Cancella", new DialogInterface.OnClickListener() {
                 public void onClick(DialogInterface dialog, int id) {
-                    DrawActivity.selectedNode.Children = new ArrayList<Node>();
+                    DrawActivity.selectedNode.Children = new ArrayList<Node>(); //eliminazione del sottoalbero
                     DrawActivity.rootNode.Clean();
                     DrawActivity.startDraw();
                 }
             });
         builder.setNegativeButton("Annulla", new DialogInterface.OnClickListener() {
             public void onClick(DialogInterface dialog, int id) {
-                thisNode=null;
             }
         });
         // Create the AlertDialog object and return it
index 5e41f79e554d026c1f43ad17cd41f2a52792f45e..eba3c67868ac5c81869bf365df7fcce4bb44c409 100755 (executable)
@@ -1,8 +1,9 @@
 package com.example.furt.myapplication;
 
-import android.graphics.Color;
 import android.view.View;
-import android.widget.TextView;
+
+/**DialogTouchHandler: Handler per la gestione delle regole cliccate
+ * nel Dialog delle regole di introduzione**/
 
 public class DialogTouchHandler implements View.OnClickListener{
     Node node;
@@ -12,21 +13,22 @@ public class DialogTouchHandler implements View.OnClickListener{
     }
     public void onClick(View view)
     {
-        if (RuleDialog.selectedRule!=null)
-            if (node==RuleDialog.selectedRule)
-                return;
-        Node sel=node;
-        while(sel.Father!=null)
-            sel=sel.Father;
-        sel.view.setTextColor(Color.RED);
-        for (Node n:sel.Children)
-            n.view.setTextColor(Color.RED);
-        if (RuleDialog.selectedRule!=null)
-        {
-            RuleDialog.selectedRule.view.setTextColor(Color.BLACK);
-            for (Node n:RuleDialog.selectedRule.Children)
-                n.view.setTextColor(Color.BLACK);
+        Node selectedRule=node;
+        while(selectedRule.Father!=null) //se l'utente ha cliccato su uno dei figli del sottoalbero risalgo alla radice
+            selectedRule=selectedRule.Father;
+        for (Node n : selectedRule.Children) { //incollo i figli del nodo sul selectedNode avendo cura di integrare le ipotesi
+            for (Hypothesis hp : n.NodeHP)
+                hp.fromNode = DrawActivity.selectedNode; //le ipotesi dei nuovi figli provengono dal nodo in cui stanno per essere inserite
+            n.addHPList(DrawActivity.selectedNode.NodeHP);
+            n.handler = null; //rimuovo l'handler per il DialogTouchHandler, che è ora inutile
+            DrawActivity.selectedNode.addChild(n);
         }
-        RuleDialog.selectedRule=sel;
+        DrawActivity.selectedNode.hasFocus = false; //il vecchio selectedNode non ha più il focus
+        DrawActivity.selectedNode.ruleName = selectedRule.Children.get(0).ruleName;
+        DrawActivity.selectedNode.Children.get(0).hasFocus = true; //il primo figlio della regola applicata acquisisce il focus
+        DrawActivity.nmoves++;
+        DrawActivity.rootNode.Clean();
+        DrawActivity.startDraw();
+        touchnodeHandler.ruleDialog.dismiss(); //il ruleDialog del touchnodeHandler non è più necessario
     }
 }
index fea3a50c84a2b1bf50434e05d84480600f3c0d1c..f9a9c849807ecf29b34fa1047f92a65f42449457 100644 (file)
@@ -20,7 +20,8 @@ import android.widget.ScrollView;
 import android.widget.Toast;
 
 import java.sql.Timestamp;
-import java.util.ArrayList;
+
+import static java.lang.Thread.sleep;
 
 public class DrawActivity extends FragmentActivity {
 
@@ -34,7 +35,7 @@ public class DrawActivity extends FragmentActivity {
     static Border[] b; //bordi per le borderedTextView
     static FragmentManager fragmentManager;//per i dialog
     static Node rootNode; //radice dell'albero corrente
-    static ScrollView scroll;
+    static ScrollView scroll; //Vertical ScrollView contenente l'albero
     static int nmoves=0;//numero di mosse
     static int nerrors=0;//nomero di errori
     static long startTime;//tempo di inizio dell'esercizio
@@ -42,6 +43,7 @@ public class DrawActivity extends FragmentActivity {
     static int globalId =10; //variabile incrementale per l'assegnazione di ID univoci
     static DisplayMetrics v = new DisplayMetrics();//altezza lunghezza e densità dello schermo
 
+    //Informazioni per la comunicazione client-server: username, password, nome dell'esercizio e chiave di sessione.
     static String user=null;
     static String pass=null;
     static String sessionKey=null;
@@ -54,17 +56,18 @@ public class DrawActivity extends FragmentActivity {
         setContentView(R.layout.activity_my);
 
         //recupero e setto le variabili globali
-        getWindowManager().getDefaultDisplay().getMetrics(v);
+        getWindowManager().getDefaultDisplay().getMetrics(v); //getMetrics() inserisce nella variabile V i dati metrici (altezza,larghezza,densità...) dello schermo del dispositivo
         globalHP = (RelativeLayout) findViewById(R.id.hpscroll);
         globalR = (RelativeLayout) findViewById(R.id.global);
-        spaceSize = 2*(textSize/v.density);
+        spaceSize = 2*(textSize/v.density); //lo spazio tra due sottoalberi è di due caratteri vuoti
         fragmentManager=getFragmentManager();
-        copiedNode=null;
+        copiedNode=null; //inizialmente non ci sono ovviamente sottoalberi copiati
         scroll=(ScrollView)findViewById(R.id.vscroll);
         startTime=time();
         b=new Border[1];
         b[0]=new Border(BorderedTextView.BORDER_TOP);
         b[0].setWidth(2);
+        //Recupero i dati passati dall'Intent: username, password, nome dell'esercizio da visualizzare e chiave di sessione
         Bundle dati=getIntent().getExtras();
         nomeEs=dati.getString("nomeEs");
         user=dati.getString("user");
@@ -72,7 +75,7 @@ public class DrawActivity extends FragmentActivity {
         sessionKey=dati.getString("sessionKey");
 
         //Creazione dell'albero: setto il rootNode e creo la Formula di partenza (F)
-        if(!populateTree())
+        if(!populateTree()) //populateTree() ha fallito: file dell'esercizio corrotto.
             return;
 
         //Creazione dell'albero: setto i campi della view
@@ -81,8 +84,10 @@ public class DrawActivity extends FragmentActivity {
         globalId++;
         selectedNode=null;
         addFakes=false; //di default non vengono aggiunte regole false
-        rootNode.setView(rootView,globalR);
+        rootNode.setView(rootView,globalR); //il rootNode viene legato al globalLayout attuale e alla TextView creata
         rootNode.handler=new touchnodeHandler(rootNode);
+        rootNode.longHandler=new longnodeHandler(rootNode);
+        rootNode.hasFocus=true; //di default, la radice ha inizialmente il focus.
         startDraw();
 
         //imposto il listener per il pinch zoom
@@ -120,17 +125,27 @@ public class DrawActivity extends FragmentActivity {
                         globalR.setPadding(0,0,(int)Math.max(rootNode.getRightOffset(),halfScreen),0);
                         globalR.getLayoutParams().height=(int)Math.max((v.heightPixels),(rootNode.getMaxHeight()+rootNode.getMaxHeight()*0.10)); //altezza della view=max(h_screen,h_tree). Aggiungo un 10% all'altezza dell'albero per approssimazione dei calcoli.
                         globalR.requestLayout(); //aggiorna i parametri e le dimensioni del RelativeLayout
-                        if (rootNode.treeHeight()< 3)
+                        if (rootNode.getMaxHeight()<v.heightPixels/2) //se l'albero non ha raggiunto almeno la metà dello schermo scrollo la view fino in fondo per visualizzarlo interamente
                             scroll.fullScroll(ScrollView.FOCUS_DOWN);
                         rootNode.view.setOnClickListener(rootNode.handler);
-                        rootNode.hasFocus=true; //di default, la radice ha inizialmente il focus.
+                        rootNode.view.setOnLongClickListener(rootNode.longHandler);
                         rootNode.view.getViewTreeObserver().removeOnGlobalLayoutListener(this); //rimuove il listener per evitare che la funzione parta nuovamente
                         rootNode.Draw();
-
                     }
                 });
     }
     @Override
+    public void onBackPressed() {
+        //abbandona esercizio e torna alla view con la lista degli esercizi
+        Intent i = new Intent(globalHP.getContext(), aggiornamento.class);
+        i.putExtra("user", user);
+        i.putExtra("pass", pass);
+        i.putExtra("sessionKey", sessionKey);
+        i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK);
+        globalHP.getContext().startActivity(i);
+
+    }
+    @Override
     public boolean onCreateOptionsMenu(Menu menu) {
         // Inflate the menu; this adds items to the action bar if it is present.
         getMenuInflater().inflate(R.menu.my, menu);
@@ -154,23 +169,7 @@ public class DrawActivity extends FragmentActivity {
     @Override
     public boolean onOptionsItemSelected(MenuItem item) {
         int id = item.getItemId();
-        if(id==R.id.action_paste) //incolla sottoalbero
-        {
-            if (DrawActivity.copiedNode == null) //non ci sono nodi da copiare
-                return true;
-            else if (!checkHP(DrawActivity.copiedNode, DrawActivity.selectedNode)) //ipotesi incompatibili: impossibile incollare in questo punto
-                return true;
-            else {
-                Node tmp = duplicateNode(DrawActivity.copiedNode); //duplica il nodo copiato
-                DrawActivity.selectedNode.ruleName=tmp.ruleName;
-                DrawActivity.selectedNode.Children = new ArrayList<Node>();
-                for (Node c:tmp.Children)
-                    DrawActivity.selectedNode.addChild(c); //incolla il sottoalbero del nodo copiato nella posizione richiesta
-                DrawActivity.rootNode.Clean();
-                DrawActivity.startDraw();
-            }
-        }
-        else if(id==R.id.abandon)
+        if(id==R.id.abandon)
         {   //abbandona esercizio e torna alla view con la lista degli esercizi
             Intent i = new Intent(globalHP.getContext(), aggiornamento.class);
             i.putExtra("user", user);
@@ -183,35 +182,6 @@ public class DrawActivity extends FragmentActivity {
     }
 
 
-    public boolean checkHP(Node source,Node target) //controlla se le ipotesi di source sono compatibili per una copia in target
-    {
-        boolean found=false;
-        if (!source.F.toString().equals(target.F.toString())) //se i nodi non hanno la stessa formula la copia è automaticamente impossibile
-            return false;
-        for (Hypothesis sourceHp:source.NodeHP) {
-            for (Hypothesis destHp : target.NodeHP) {
-                if (destHp.HP.toString().equals(sourceHp.HP.toString())) { //per ogni ipotesi nel nodo sorgente cerco se è disponibile nel nodo destinazione: in caso affermativo, proseguo il ciclo (found=true).
-                    found = true;
-                    break;
-                }
-            }
-            if (!found)
-                return false;
-            else found=false;
-        }
-        return true;
-    }
-
-    public Node duplicateNode(Node src) //metodo di supporto che duplica un nodo
-    {
-        Node tmp=new Node(src.F);
-        tmp.addHPList(src.NodeHP);
-        tmp.ruleName=src.ruleName;
-        for (Node n:src.Children) {
-            tmp.addChild(duplicateNode(n));
-        }
-        return tmp;
-    }
 
     public class simpleOnScaleGestureListener extends
             ScaleGestureDetector.SimpleOnScaleGestureListener {
@@ -247,8 +217,23 @@ public class DrawActivity extends FragmentActivity {
             int second= (int) ((endTime-startTime)/1000);
             int minute=second/60;
             Toast.makeText(context, "Esercizio completato in " + Integer.toString(nmoves) + " mosse!", Toast.LENGTH_LONG).show();
+            try {
+                sleep(2);
+            } catch (InterruptedException e) {
+                e.printStackTrace();
+            }
             Toast.makeText(context, "Hai commesso " + Integer.toString(nerrors) + " errori!", Toast.LENGTH_LONG).show();
+            try {
+                sleep(2);
+            } catch (InterruptedException e) {
+                e.printStackTrace();
+            }
             Toast.makeText(context, "Numero nodi dell'albero: " + Integer.toString(rootNode.count()), Toast.LENGTH_LONG).show();
+            try {
+                sleep(2);
+            } catch (InterruptedException e) {
+                e.printStackTrace();
+            }
             Toast.makeText(context, "Tempo impiegato: " + Integer.toString(minute) + " minuti e " + Integer.toString(second-(minute*60)) + " secondi", Toast.LENGTH_LONG).show();
             //aggiungo l'esercizio al database
             int voto=valutazione.voto(nomeEs,nmoves,second,rootNode.count(),nerrors);
index 7285a4a835e0e52901b7f179677031552d6ef980..cc55c4587ad74f81a7dca94f33cb6482da3ce1b6 100755 (executable)
@@ -1,11 +1,8 @@
 package com.example.furt.myapplication;
 
-import java.util.ArrayList;
-import java.util.List;
-
+/**EliminationRule: interfaccia per le regole di eliminazione**/
 public interface EliminationRule
 {
-    public String getName();
-    public Node createNodes(Formula F, askFormula ask);
+    public Node createNodes(Formula F, askFormula ask); //restituisce il sottoalbero successivo all'applicazione della regola sul nodo attualmente selezionato
 }
 
index 4209b5803d65dfcc3aa0989e6d45e5b50a48dbfd..01454447a8ce43a0288322cafbbbda3c13a613a7 100755 (executable)
@@ -1,7 +1,8 @@
 package com.example.furt.myapplication;
 
 import java.util.List;
-
+/**Formula:interfaccia per l'implementazione di formule logiche. Prevede metodi per
+ * l'applicazione delle regole e per la gestione dell'editor guidato per l'inserimento.**/
 public interface Formula extends FView{
     public List<IntroductionRule> introductionRules();
     public List<EliminationRule> EliminationRules();
index 2c81ee93c3b57746646d6a863a0a434941a0aa3c..fe75584e9da66bbcd4abf82d66dd80f2f9c0146e 100755 (executable)
@@ -31,6 +31,8 @@ public class FormulaAnd extends GenericFormula implements Formula
     {
         List<IntroductionRule> rules=new ArrayList<IntroductionRule>();
         rules.addAll(super.introductionRules());
+
+        //Regola di introduzione dell'And
         RuleIntroduction andIntroduction=new RuleIntroduction("∧i",5);
         Node Left=new Node(leftF);
         Node Right=new Node(rightF);
@@ -39,6 +41,7 @@ public class FormulaAnd extends GenericFormula implements Formula
         thisNode.addChild(Right);
         andIntroduction.tempRule=thisNode;
         rules.add(andIntroduction);
+
         return rules;
     }
     public List<EliminationRule> EliminationRules()
index 6103bd81a436c4cdc4b2b92a3d7720f575d5880a..f5e905b0c8b904e91f2b28af5603ee39fe6b4080 100755 (executable)
@@ -19,6 +19,7 @@ public class FormulaBOT extends GenericFormula implements Formula{
     }
 
     public List<IntroductionRule> introductionRules(){
+        //Bottom non ha regole di introduzione sensate
         List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
         return nodes;
     }
index 9761a0e58384ce57322d9f7bf6e18e24415f20c8..efe17147ec0749845cb06cc68285372e3cf17212 100755 (executable)
@@ -28,7 +28,10 @@ public class FormulaImpl extends GenericFormula implements Formula
 
     public List<IntroductionRule> introductionRules(){
         List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
-        nodes.addAll(super.introductionRules());
+        nodes.addAll(super.introductionRules()); //aggiunge la regola di R.A.A.
+
+        //Regola di introduzione dell'implicazione
+
         RuleIntroduction implIntro=new RuleIntroduction("⇒i",10);
         Node ImplN=new Node(rightF);
         List<Formula> implHP=new ArrayList<Formula>();
@@ -38,6 +41,7 @@ public class FormulaImpl extends GenericFormula implements Formula
         thisNode.addChild(ImplN);
         implIntro.tempRule=thisNode;
         nodes.add(implIntro);
+
         return nodes;
     }
     public List<EliminationRule> EliminationRules()
index f8b0d37662acb5febfa12758681b95ee7f091da6..6bd80e54f602c6e199353087e750cf2ac526f1fe 100755 (executable)
@@ -27,6 +27,8 @@ public class FormulaNot extends GenericFormula implements Formula{
 
     public List<IntroductionRule> introductionRules(){
         List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
+
+        //Introduzione del not (NOTA: il not non eredita la regola di riduzione ad assurdo)
         RuleIntroduction notIntro=new RuleIntroduction("¬i",4);
         Node notN=new Node(new FormulaBOT());
         List<Formula> notHP=new ArrayList<Formula>();
@@ -63,4 +65,4 @@ public class FormulaNot extends GenericFormula implements Formula{
     public Formula duplicate() {
         return new FormulaNot(Operand.duplicate());
     }
-}
\ No newline at end of file
+}
index 4a1794d7e2fec35a78a9a4be2225a0a56399cf2e..83531cc5a8df1ccf6931261d0cb6843439ee2f41 100755 (executable)
@@ -30,19 +30,24 @@ public class FormulaOr extends GenericFormula implements Formula
 
     public List<IntroductionRule> introductionRules(){
         List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
-        nodes.addAll(super.introductionRules());
+        nodes.addAll(super.introductionRules()); //eredita la R.A.A.
+
+        //Introduzione sinistra dell'or
         RuleIntroduction orIntroductionLeft=new RuleIntroduction("∨i(L)",6);
         Node orLeft=new Node(leftF);
         Node thisNodeL=new Node(this);
         thisNodeL.addChild(orLeft);
         orIntroductionLeft.tempRule=thisNodeL;
         nodes.add(orIntroductionLeft);
+
+        //Introduzione destra dell'or
         RuleIntroduction orIntroductionRight=new RuleIntroduction("∨i(R)",5);
         Node orRight=new Node(rightF);
         Node thisNodeR=new Node(this);
         thisNodeR.addChild(orRight);
         orIntroductionRight.tempRule=thisNodeR;
         nodes.add(orIntroductionRight);
+
         return nodes;
     }
 
index 05cba71e095396200a6ca8a8b46e694869739455..8d9aa70147dc07e8c701e78d0814df30f02e8fbd 100755 (executable)
@@ -14,8 +14,9 @@ public class FormulaTOP extends GenericFormula implements Formula{
     public String Draw(int p){return "Ț";}
 
     public List<IntroductionRule> introductionRules(){
+        //le regole di introduzione ed eliminazione per Top non sono implementate in quanto prive
+        //di un'applicazione effettiva nella dimostrazione
         List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
-        nodes.addAll(super.introductionRules());
         return nodes;
     }
 
@@ -34,9 +35,4 @@ public class FormulaTOP extends GenericFormula implements Formula{
         return new FormulaTOP();
     }
 
-    public List<EliminationRule> eliminationRules(){
-        List<EliminationRule> nodes=new ArrayList<EliminationRule>();
-        return nodes;
-    }
-
 }
index 5e063f536c2e83708495db223f18524fc08fb735..b2136ab0be74c6b06309eba9601553e3fbe52fdb 100755 (executable)
@@ -12,17 +12,17 @@ public class GenericFormula implements Formula
     int priority;
     public String Draw(int p)
     {
-        return "";
-    }
+        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);
+        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);
+        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()
     {
@@ -33,7 +33,7 @@ public class GenericFormula implements Formula
         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);
+        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>();
index 6a7d63882e1e8b91c50e0e18e1ae76f6292c7022..f95143115f1aba5e93c9ba978816b2befe006a28 100755 (executable)
@@ -1,5 +1,8 @@
 package com.example.furt.myapplication;
 
+/**Hypothesis: implementa le ipotesi di un nodo. Contiene una formula, un booleano per verificare se si stratta
+ * di un'ipotesi scaricata e un puntatore al nodo in cui l'ipotesi è stata introdotta
+ */
 public class Hypothesis
 {
     Formula HP;
@@ -11,4 +14,4 @@ public class Hypothesis
         isDeleted=d;
         fromNode=null;
     }
-}
\ No newline at end of file
+}
index 880ca1a772f35276f66f972245397f84663bf6f6..9799a4388a1437307d43f4159e1e5004471e2de1 100755 (executable)
@@ -3,6 +3,5 @@ package com.example.furt.myapplication;
 public interface IntroductionRule
 {
     int getPriority();
-    String getName();
     public Node createNodes(askFormula ask);
 }
index d1299756d7e58037db64db53cc420cdaca0897c3..3da98cee6c9abf3d62515cf556f4fae2ffb577ed 100755 (executable)
@@ -16,7 +16,7 @@ public class Literal extends GenericFormula implements Formula
 
     public List<IntroductionRule> introductionRules(){
         List<IntroductionRule> nodes=new ArrayList<IntroductionRule>();
-        nodes.addAll(super.introductionRules());
+        nodes.addAll(super.introductionRules()); //eredita la R.A.A.
         return nodes;
     }
 
@@ -25,10 +25,6 @@ public class Literal extends GenericFormula implements Formula
         return false;
     }
 
-    public boolean isCompatible(Node n) {
-        return true;
-    }
-
     @Override
     public Formula duplicate() {
         return new Literal(this.L.charAt(0));
index fa59a8d8d1a6d950aa4bfe890ec19450b241107e..69ed7c38cd881743d2c6099fc83b01d3ced45b8e 100755 (executable)
@@ -4,6 +4,9 @@ import android.graphics.Color;
 import android.os.Handler;
 import android.view.View;
 
+/**LongHPClick: handler per il longtouch delle ipotesi. Illumina di giallo il nodo
+ * da cui proviene l'ipotesi in oggetto
+ */
 public class LongHPClick implements View.OnLongClickListener {
 
     Node n;
index 8f7bdc00dc54e323d6c9f6c52c042ae55ee82747..dc2898695b362e72192b063159c91af5036919da 100755 (executable)
@@ -11,25 +11,6 @@ public class MD5 {
 
     MD5(){}
 
-    /*public static String digest(String fileName) throws NoSuchAlgorithmException, IOException
-    {
-
-        MessageDigest md = MessageDigest.getInstance("MD5");
-        return getDigest(new FileInputStream("/var/www/html/esercizi/"+fileName), md, 2048);
-    }
-
-    public static String getDigest(InputStream is, MessageDigest md, int byteArraySize) throws NoSuchAlgorithmException, IOException
-    {
-        md.reset();
-        byte[] bytes = new byte[byteArraySize];
-        int numBytes;
-        while ((numBytes = is.read(bytes)) != -1) {
-            md.update(bytes, 0, numBytes);
-        }
-        byte[] digest = md.digest();
-        String result = new String(Hex.encodeHex(digest));
-        return result;
-    }*/
     public static String digest(String filePath) {
         InputStream inputStream = null;
         try {
index 9b724ffb4068b38de5d493a4e24f68bd1991d03d..0a39fdf635fb59653cd434ce6b15ff7b52015a53 100755 (executable)
@@ -29,16 +29,17 @@ public class Node implements Tree {
     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;
-    float leftOffset;
-    float rightOffset;
-    float maxWidth;
+    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;
@@ -80,11 +81,17 @@ public class Node implements Tree {
             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())) {
+                if (oldHp.HP.toString().equals(newHp.toString())) { //ipotesi già presente: passo alla prossima
                     continue loop;
                 }
             }
@@ -95,7 +102,7 @@ public class Node implements Tree {
     public void addHPList(List<Hypothesis>List) {
         loop:for (Hypothesis newHp:List) {
             for (Hypothesis oldHp: NodeHP) {
-                if (oldHp.HP.toString().equals(newHp.HP.toString())) {
+                if (oldHp.HP.toString().equals(newHp.HP.toString())) { //ipotesi già presente: passo alla prossima
                     continue loop;
                 }
             }
@@ -105,6 +112,11 @@ public class Node implements Tree {
         }
     }
 
+    /*****************************************/
+    /******* 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
@@ -137,6 +149,7 @@ public class Node implements Tree {
         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;
@@ -170,20 +183,11 @@ public class Node implements Tree {
             return baseLine;
         else
         {
-            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();
-            res -= Children.get(Children.size() - 1).getRightOffset();
-            baseLine=Math.max(res,getBaseWidth());
+            baseLine=Math.max(getUpLine(),getBaseWidth()); //la baseline è il massimo valore tra la upLine e la baseWidth
             return baseLine;
         }
     }
-    public float getUpLine()
+    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)
@@ -192,10 +196,16 @@ public class Node implements Tree {
         for(Node n:Children)
             res+=(n.getMaxWidth())+spaceSize;
         res-=spaceSize;
-        res-=Children.get(0).getLeftOffset();
-        res-=Children.get(Children.size()-1).getRightOffset();
+        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;
@@ -209,18 +219,6 @@ public class Node implements Tree {
         }
     }
 
-    public float getMaxHeight()
-    {
-        float baseRes=F.height();
-        float res=baseRes;
-        for (Node n:Children)
-        {
-            float tempH=n.getMaxHeight()+baseRes;
-            if(tempH>res)
-                res=tempH;
-        }
-        return res;
-    }
     public float getRightOffset()
     {
         if (rightOffset!=FIELD_UNSET)
@@ -233,7 +231,21 @@ public class Node implements Tree {
             return rightOffset;
         }
     }
-    void Refactor()
+
+    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;
@@ -243,83 +255,13 @@ public class Node implements Tree {
             n.Refactor();
     }
 
-    void Resize()
-    {
-        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();
-            }
-
-        }
-
-    }
-
-    public int treeHeight()
+    public void Clean() //metodo di supporto: rimuove dal layout legato al Node tutte le view presenti
     {
-        int res=0,tmp;
-        for (Node n:Children)
-        {
-            tmp=n.treeHeight();
-            if (tmp>res)
-                res=tmp;
-        }
-        return res+1;
+        global.removeAllViews();
     }
-    public boolean isCorrect()
+
+    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;
@@ -329,25 +271,21 @@ public class Node implements Tree {
         return true;
 
     }
-    public void Clean()
-    {
-        global.removeAllViews();
-    }
 
     public void Draw()
     {
-        int i;
         float interval=0; //intervallo di spazio da sommare nella creazione dei figli
-        float spaceSize= DrawActivity.spaceSize;
-        int childNo=Children.size();
+        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))) {
+                    if (!(Father.searchFocus(this))) { //focus inapplicabile nell'albero: dimostrazione completata.
                         DrawActivity.finishedTree(view.getContext());
                         return;
                     }
@@ -355,8 +293,12 @@ public class Node implements Tree {
                 }
                 if (status==CANCELED || status==FAKE_CANCELED) { //nodo cancellato
                     view.setWidth((int) F.sizeDeleted());
-                    view.setText("[" + view.getText() + "]");
+                    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;
             }
@@ -371,40 +313,29 @@ public class Node implements Tree {
         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);
+        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
 
-        hasFocus=false;
-        for (i=0;i<childNo;i++) {
-            final Node newChild=Children.get(i);
+        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);
-                if (getLineWidth()>getUpLine())
+                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);
+                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);
+                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);
@@ -420,7 +351,9 @@ public class Node implements Tree {
                     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();
                 }
@@ -428,12 +361,76 @@ public class Node implements Tree {
             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();
             }
+
         }
+
     }
 
-}
\ No newline at end of file
+}
index 5b2c5d4e2e86572a81c4062fc659d881aa8dfaf6..5970a86f07528beff711d7f800cae4507bf660ec 100755 (executable)
@@ -2,13 +2,10 @@ package com.example.furt.myapplication;
 
 import java.util.ArrayList;
 import java.util.List;
+
 public class RuleAndElimination implements EliminationRule
 {
     String ruleName;
-    public String getName()
-    {
-        return ruleName;
-    }
     FormulaAnd Fn;
     RuleAndElimination(FormulaAnd F){
         Fn=F;
@@ -17,14 +14,15 @@ public class RuleAndElimination implements EliminationRule
     public Node createNodes(Formula F,askFormula ask)
     {
             Formula C;
-            if (F==null)
+            if (F==null) //applicazione Top-Down: chiamo la callback
                 C=ask.Ask();
             else
-                C=F;
+                C=F; //applicazione bottom-up: il nuovo nodo è la formula F passata
             Node cNode=new Node(C);
-            if ((C.toString().equals(Fn.leftF.toString())) || (C.toString().equals(Fn.rightF.toString()))) //I can return leftAnd rule or rightAnd rule
+            if ((C.toString().equals(Fn.leftF.toString())) || (C.toString().equals(Fn.rightF.toString()))) //Posso utilizzare le regole di eliminazione sinistra o destra
             {
                 cNode.addChild(new Node(Fn));
+                cNode.ruleName=ruleName;
                 return cNode;
             }
             Node elNode=new Node(Fn);
index 83a54fd76fa5993d9646912159508fc901bb0814..501dfe5967d1239008119dd53dbcff358a035df8 100755 (executable)
@@ -3,10 +3,6 @@ package com.example.furt.myapplication;
 public class RuleBotElimination implements EliminationRule
 {
     String ruleName;
-    public String getName()
-    {
-        return ruleName;
-    }
     FormulaBOT Fn;
     RuleBotElimination(FormulaBOT F)
     {
@@ -15,11 +11,15 @@ public class RuleBotElimination implements EliminationRule
     }
     public Node createNodes(Formula F,askFormula ask)
     {
-        Formula C=ask.Ask();
+        Formula C;
+        if (F!=null)
+            C=F;
+        else
+            C=ask.Ask();
         Node elNode=new Node(Fn);
         Node rNode=new Node(C);
         rNode.addChild(elNode);
         rNode.ruleName=ruleName;
         return rNode;
     }
-}
\ No newline at end of file
+}
index 6bcd7bb16026a4b798236fd5ca8750dd0425fed7..1cffd89af95e98ba5bc0271fc1e066f72115f011 100755 (executable)
@@ -12,17 +12,16 @@ import android.view.View;
 import android.view.ViewGroup;
 import android.view.ViewTreeObserver;
 import android.widget.RelativeLayout;
+import android.widget.Toast;
 
 import java.util.ArrayList;
 import java.util.List;
 
 public class RuleDialog extends DialogFragment {
     List<IntroductionRule> rules;
-    static Node selectedRule;
     boolean showAllRules;
     public RuleDialog(List<IntroductionRule> r)
     {
-        selectedRule=null;
         rules=new ArrayList<IntroductionRule>();
         rules.addAll(r);
         showAllRules=false;
@@ -31,14 +30,23 @@ public class RuleDialog extends DialogFragment {
     public Dialog onCreateDialog(final Bundle savedInstanceState) {
         // Use the Builder class for convenient dialog construction
         AlertDialog.Builder builder = new AlertDialog.Builder(getActivity());
+        int prules=0;
+        for (IntroductionRule r:rules)
+            if (r.getPriority()>0)
+                prules++;
+        if (prules==0 && !showAllRules)
+        {
+            showAllRules=true;
+            reboot();
+            dismiss();
+            return builder.create();
+        }
         LayoutInflater inflater=getActivity().getLayoutInflater();
         View view=inflater.inflate(R.layout.ruledialog,null);
         RelativeLayout layout=(RelativeLayout)((ViewGroup)((ViewGroup)view).getChildAt(0)).getChildAt(0);
         int ruleInterval=50;
-        int i=0;
-        for (i=0;i<rules.size();i++) {
-            IntroductionRule rule=rules.get(i);
-            if (!showAllRules && rule.getPriority()==0)
+        for (IntroductionRule rule : rules) {
+            if (!showAllRules && rule.getPriority() == 0)
                 continue; //only high priority: skip this node
             final Node drawNode = rule.createNodes(new askFormula());
             BorderedTextView t = new BorderedTextView(layout.getContext());
@@ -47,7 +55,7 @@ public class RuleDialog extends DialogFragment {
             drawNode.setView(t, layout);
             RelativeLayout.LayoutParams lp = new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
             lp.setMargins(ruleInterval, 0, 0, 0);
-            ruleInterval+=2*drawNode.getMaxWidth();
+            ruleInterval += 2 * drawNode.getMaxWidth();
             lp.addRule(RelativeLayout.ALIGN_PARENT_BOTTOM, drawNode.view.getId());
             drawNode.view.setLayoutParams(lp);
             drawNode.view.setBorders(DrawActivity.b);
@@ -56,8 +64,8 @@ public class RuleDialog extends DialogFragment {
             drawNode.view.setGravity(Gravity.CENTER); //formula al centro della sua overline
             drawNode.view.setText(drawNode.F.toString()); //setta il contenuto della formula
             drawNode.global.addView(drawNode.view);
-            drawNode.handler=new DialogTouchHandler(drawNode);
-            for (Node n:drawNode.Children) {
+            drawNode.handler = new DialogTouchHandler(drawNode);
+            for (Node n : drawNode.Children) {
                 n.handler = new DialogTouchHandler(drawNode);
             }
             //inserisco un listener a rootView da attivare quando sono state fissate le coordinate nel RelativeLayout
@@ -76,30 +84,31 @@ public class RuleDialog extends DialogFragment {
                     });
         }
         builder.setView(view);
-        builder.setTitle("Scegli una regola:")
-                .setPositiveButton("Ok", new DialogInterface.OnClickListener() {
-                    public void onClick(DialogInterface dialog, int id) {
-                        if (selectedRule == null) return;
-                        for (Node n : selectedRule.Children) {
-                            for (Hypothesis hp : n.NodeHP)
-                                hp.fromNode = DrawActivity.selectedNode; //le ipotesi dei nuovi figli provengono dal nodo in cui stanno per essere inserite
-                            n.addHPList(DrawActivity.selectedNode.NodeHP);
-                            n.handler = null;
-                            DrawActivity.selectedNode.addChild(n);
-                        }
-                        DrawActivity.selectedNode.hasFocus = false;
-                        DrawActivity.selectedNode.ruleName = selectedRule.Children.get(0).ruleName;
-                        DrawActivity.selectedNode.Children.get(0).hasFocus = true;
-                        DrawActivity.nmoves++;
-                        DrawActivity.rootNode.Clean();
-                        DrawActivity.startDraw();
-                        selectedRule=null;
-                    }
-                });
+        builder.setTitle("Scegli una regola:");
+        builder.setPositiveButton("Incolla sottoalbero",new DialogInterface.OnClickListener() {
+            @Override
+            public void onClick(DialogInterface dialog, int which) {
+                if (DrawActivity.copiedNode == null) //non ci sono nodi da copiare
+                {
+                    Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile incollare: nessun nodo copiato",Toast.LENGTH_LONG).show();
+                }
+                else if (!checkHP(DrawActivity.copiedNode, DrawActivity.selectedNode)) //ipotesi incompatibili: impossibile incollare in questo punto
+                    Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile incollare: sottoalberi incompatibili",Toast.LENGTH_LONG).show();
+                else {
+                    Node tmp = duplicateNode(DrawActivity.copiedNode); //duplica il nodo copiato
+                    DrawActivity.selectedNode.ruleName=tmp.ruleName; //eredita il nome della regola
+                    DrawActivity.selectedNode.Children = new ArrayList<Node>();
+                    for (Node c:tmp.Children)
+                        DrawActivity.selectedNode.addChild(c); //incolla il sottoalbero del nodo copiato nella posizione richiesta
+                    DrawActivity.rootNode.Clean();
+                    DrawActivity.startDraw();
+                }
+            }
+        });
         if (!showAllRules) {
             builder.setNeutralButton("Mostra tutte", new DialogInterface.OnClickListener() {
                 public void onClick(DialogInterface dialog, int id) {
-                    showAllRules = true;
+                    showAllRules=true;
                     reboot();
                 }
             });
@@ -107,14 +116,13 @@ public class RuleDialog extends DialogFragment {
         else {
             builder.setNeutralButton("Nascondi", new DialogInterface.OnClickListener() {
                 public void onClick(DialogInterface dialog, int id) {
-                    showAllRules = false;
+                    showAllRules=false;
                     reboot();
                 }
             });
         }
         builder.setNegativeButton("Annulla", new DialogInterface.OnClickListener() {
             public void onClick(DialogInterface dialog, int id) {
-                selectedRule=null;
             }
         });
         // Create the AlertDialog object and return it
@@ -122,10 +130,39 @@ public class RuleDialog extends DialogFragment {
     }
     void reboot()
     {
-        selectedRule=null;
-        RuleDialog ruleDialog=new RuleDialog(rules);
-        ruleDialog.showAllRules=showAllRules;
-        ruleDialog.show(DrawActivity.fragmentManager, "CIAO");
+        touchnodeHandler.ruleDialog=new RuleDialog(rules);
+        touchnodeHandler.ruleDialog.showAllRules=showAllRules;
+        touchnodeHandler.ruleDialog.show(DrawActivity.fragmentManager, "CIAO");
+    }
+
+    public boolean checkHP(Node source,Node target) //controlla se le ipotesi di source sono compatibili per una copia in target
+    {
+        boolean found=false;
+        if (!source.F.toString().equals(target.F.toString())) //se i nodi non hanno la stessa formula la copia è automaticamente impossibile
+            return false;
+        for (Hypothesis sourceHp:source.NodeHP) {
+            for (Hypothesis destHp : target.NodeHP) {
+                if (destHp.HP.toString().equals(sourceHp.HP.toString())) { //per ogni ipotesi nel nodo sorgente cerco se è disponibile nel nodo destinazione: in caso affermativo, proseguo il ciclo (found=true).
+                    found = true;
+                    break;
+                }
+            }
+            if (!found)
+                return false;
+            else found=false;
+        }
+        return true;
+    }
+
+    public Node duplicateNode(Node src) //metodo di supporto che duplica un nodo
+    {
+        Node tmp=new Node(src.F);
+        tmp.addHPList(src.NodeHP);
+        tmp.ruleName=src.ruleName;
+        for (Node n:src.Children) {
+            tmp.addChild(duplicateNode(n));
+        }
+        return tmp;
     }
 }
 
index 0c266dd34b85d9b8effff26e7c8f2e8c18d6ab3b..f2fd1ffefbf4d7dbaf16a6e53a42a72579731677 100755 (executable)
@@ -3,10 +3,6 @@ package com.example.furt.myapplication;
 public class RuleImplElimination implements EliminationRule
 {
     String ruleName;
-    public String getName()
-    {
-        return ruleName;
-    }
     FormulaImpl Fn;
     RuleImplElimination(FormulaImpl F)
     {
index 67301e0c90971fa443cb013d11283e8285cdaf7b..ed0b6a12e41eede9480e7406136cc1719c424e89 100755 (executable)
@@ -11,10 +11,6 @@ public class RuleIntroduction implements IntroductionRule
     {
         ruleName=name; priority=p;
     }
-    public String getName()
-    {
-        return ruleName;
-    }
     public Node createNodes(askFormula ask)
     {
         Formula C=ask.Ask();
index ec5034b9482190866a545f3ae673cc083cebeb2a..7c7aaca7511eea01c353e316d68945a0b7dab74d 100755 (executable)
@@ -3,10 +3,6 @@ package com.example.furt.myapplication;
 public class RuleNotElimination implements EliminationRule
 {
     String ruleName;
-    public String getName()
-    {
-        return ruleName;
-    }
     FormulaNot Fn;
     RuleNotElimination(FormulaNot F)
     {
index 3d678b7f1b52df439622940994410edbe8d76399..75d1a7765e26b1f1a00f48407bf948c80b6390a8 100755 (executable)
@@ -6,10 +6,6 @@ import java.util.List;
 public class RuleOrElimination implements EliminationRule
 {
     String ruleName;
-    public String getName()
-    {
-        return ruleName;
-    }
     FormulaOr Fn;
     RuleOrElimination(FormulaOr F)
     {
diff --git a/mainActivity/src/com/example/furt/myapplication/TwoDScrollView.java b/mainActivity/src/com/example/furt/myapplication/TwoDScrollView.java
deleted file mode 100755 (executable)
index 8108428..0000000
+++ /dev/null
@@ -1,1129 +0,0 @@
-package com.example.furt.myapplication;
-
-import android.content.Context;
-import android.graphics.Rect;
-import android.util.AttributeSet;
-import android.view.FocusFinder;
-import android.view.KeyEvent;
-import android.view.MotionEvent;
-import android.view.VelocityTracker;
-import android.view.View;
-import android.view.ViewConfiguration;
-import android.view.ViewGroup;
-import android.view.ViewParent;
-import android.view.animation.AnimationUtils;
-import android.widget.FrameLayout;
-import android.widget.Scroller;
-
-import java.util.List;
-
-
-/**
- * Copyright (C) 2006 The Android Open Source Project
- *
- * Licensed under the Apache License, Version 2.0 (the "License");
- * you may not use this file except in compliance with the License.
- * You may obtain a copy of the License at
- *
- *      http://www.apache.org/licenses/LICENSE-2.0
- *
- * Unless required by applicable law or agreed to in writing, software
- * distributed under the License is distributed on an "AS IS" BASIS,
- * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
- * See the License for the specific language governing permissions and
- * limitations under the License.
- *
-*
- * Revised 5/19/2010 by GORGES
- * Now supports two-dimensional view scrolling
- * http://GORGES.us
- */
-
-/**
- * Layout container for a view hierarchy that can be scrolled by the user,
- * allowing it to be larger than the physical display.  A TwoDScrollView
- * is a {@link android.widget.FrameLayout}, meaning you should place one child in it
- * containing the entire contents to scroll; this child may itself be a layout
- * manager with a complex hierarchy of objects.  A child that is often used
- * is a {@link android.widget.LinearLayout} in a vertical orientation, presenting a vertical
- * array of top-level items that the user can scroll through.
- *
- * <p>The {@link android.widget.TextView} class also
- * takes care of its own scrolling, so does not require a TwoDScrollView, but
- * using the two together is possible to achieve the effect of a text view
- * within a larger container.
- */
-
-public class TwoDScrollView extends FrameLayout {
-    static final int ANIMATED_SCROLL_GAP = 250;
-    static final float MAX_SCROLL_FACTOR = 0.5f;
-
-    private long mLastScroll;
-
-    private final Rect mTempRect = new Rect();
-    private Scroller mScroller;
-
-    /*
-     * Flag to indicate that we are moving focus ourselves. This is so the
-     * code that watches for focus changes initiated outside this TwoDScrollView
-     * knows that it does not have to do anything.
-     */
-    private boolean mTwoDScrollViewMovedFocus;
-
-    /*
-     * Position of the last motion event.
-     */
-    private float mLastMotionY;
-    private float mLastMotionX;
-
-    /*
-     * True when the layout has changed but the traversal has not come through yet.
-     * Ideally the view hierarchy would keep track of this for us.
-     */
-    private boolean mIsLayoutDirty = true;
-
-    /*
-     * The child to give focus to in the event that a child has requested focus while the
-     * layout is dirty. This prevents the scroll from being wrong if the child has not been
-     * laid out before requesting focus.
-     */
-    private View mChildToScrollTo = null;
-
-    /*
-     * True if the user is currently dragging this TwoDScrollView around. This is
-     * not the same as 'is being flinged', which can be checked by
-     * mScroller.isFinished() (flinging begins when the user lifts his finger).
-     */
-    private boolean mIsBeingDragged = false;
-
-    /*
-     * Determines speed during touch scrolling
-     */
-    private VelocityTracker mVelocityTracker;
-
-    /*
-     * Whether arrow scrolling is animated.
-     */
-    private int mTouchSlop;
-    private int mMinimumVelocity;
-    private int mMaximumVelocity;
-
-    public TwoDScrollView(Context context) {
-        super(context);
-        initTwoDScrollView();
-    }
-
-    public TwoDScrollView(Context context, AttributeSet attrs) {
-        super(context, attrs);
-        initTwoDScrollView();
-    }
-
-    public TwoDScrollView(Context context, AttributeSet attrs, int defStyle) {
-        super(context, attrs, defStyle);
-        initTwoDScrollView();
-    }
-
-    @Override
-    protected float getTopFadingEdgeStrength() {
-        if (getChildCount() == 0) {
-            return 0.0f;
-        }
-        final int length = getVerticalFadingEdgeLength();
-        if (getScrollY() < length) {
-            return getScrollY() / (float) length;
-        }
-        return 1.0f;
-    }
-
-    @Override
-    protected float getBottomFadingEdgeStrength() {
-        if (getChildCount() == 0) {
-            return 0.0f;
-        }
-        final int length = getVerticalFadingEdgeLength();
-        final int bottomEdge = getHeight() - getPaddingBottom();
-        final int span = getChildAt(0).getBottom() - getScrollY() - bottomEdge;
-        if (span < length) {
-            return span / (float) length;
-        }
-        return 1.0f;
-    }
-
-    @Override
-    protected float getLeftFadingEdgeStrength() {
-        if (getChildCount() == 0) {
-            return 0.0f;
-        }
-        final int length = getHorizontalFadingEdgeLength();
-        if (getScrollX() < length) {
-            return getScrollX() / (float) length;
-        }
-        return 1.0f;
-    }
-
-    @Override
-    protected float getRightFadingEdgeStrength() {
-        if (getChildCount() == 0) {
-            return 0.0f;
-        }
-        final int length = getHorizontalFadingEdgeLength();
-        final int rightEdge = getWidth() - getPaddingRight();
-        final int span = getChildAt(0).getRight() - getScrollX() - rightEdge;
-        if (span < length) {
-            return span / (float) length;
-        }
-        return 1.0f;
-    }
-
-    /**
-     * @return The maximum amount this scroll view will scroll in response to
-     *   an arrow event.
-     */
-    public int getMaxScrollAmountVertical() {
-        return (int) (MAX_SCROLL_FACTOR * getHeight());
-    }
-    public int getMaxScrollAmountHorizontal() {
-        return (int) (MAX_SCROLL_FACTOR * getWidth());
-    }
-
-    private void initTwoDScrollView() {
-        mScroller = new Scroller(getContext());
-        setFocusable(true);
-        setDescendantFocusability(FOCUS_AFTER_DESCENDANTS);
-        setWillNotDraw(false);
-        final ViewConfiguration configuration = ViewConfiguration.get(getContext());
-        mTouchSlop = configuration.getScaledTouchSlop();
-        mMinimumVelocity = configuration.getScaledMinimumFlingVelocity();
-        mMaximumVelocity = configuration.getScaledMaximumFlingVelocity();
-    }
-
-    @Override
-    public void addView(View child) {
-        if (getChildCount() > 0) {
-            throw new IllegalStateException("TwoDScrollView can host only one direct child");
-        }
-        super.addView(child);
-    }
-
-    @Override
-    public void addView(View child, int index) {
-        if (getChildCount() > 0) {
-            throw new IllegalStateException("TwoDScrollView can host only one direct child");
-        }
-        super.addView(child, index);
-    }
-
-    @Override
-    public void addView(View child, ViewGroup.LayoutParams params) {
-        if (getChildCount() > 0) {
-            throw new IllegalStateException("TwoDScrollView can host only one direct child");
-        }
-        super.addView(child, params);
-    }
-
-    @Override
-    public void addView(View child, int index, ViewGroup.LayoutParams params) {
-        if (getChildCount() > 0) {
-            throw new IllegalStateException("TwoDScrollView can host only one direct child");
-        }
-        super.addView(child, index, params);
-    }
-
-    /**
-     * @return Returns true this TwoDScrollView can be scrolled
-     */
-    private boolean canScroll() {
-        View child = getChildAt(0);
-        if (child != null) {
-            int childHeight = child.getHeight();
-            int childWidth = child.getWidth();
-            return (getHeight() < childHeight + getPaddingTop() + getPaddingBottom()) ||
-                    (getWidth() < childWidth + getPaddingLeft() + getPaddingRight());
-        }
-        return false;
-    }
-
-    @Override
-    public boolean dispatchKeyEvent(KeyEvent event) {
-        // Let the focused view and/or our descendants get the key first
-        boolean handled = super.dispatchKeyEvent(event);
-        if (handled) {
-            return true;
-        }
-        return executeKeyEvent(event);
-    }
-
-    /**
-     * You can call this function yourself to have the scroll view perform
-     * scrolling from a key event, just as if the event had been dispatched to
-     * it by the view hierarchy.
-     *
-     * @param event The key event to execute.
-     * @return Return true if the event was handled, else false.
-     */
-    public boolean executeKeyEvent(KeyEvent event) {
-        mTempRect.setEmpty();
-        if (!canScroll()) {
-            if (isFocused()) {
-                View currentFocused = findFocus();
-                if (currentFocused == this) currentFocused = null;
-                View nextFocused = FocusFinder.getInstance().findNextFocus(this, currentFocused, View.FOCUS_DOWN);
-                return nextFocused != null && nextFocused != this && nextFocused.requestFocus(View.FOCUS_DOWN);
-            }
-            return false;
-        }
-        boolean handled = false;
-        if (event.getAction() == KeyEvent.ACTION_DOWN) {
-            switch (event.getKeyCode()) {
-                case KeyEvent.KEYCODE_DPAD_UP:
-                    if (!event.isAltPressed()) {
-                        handled = arrowScroll(View.FOCUS_UP, false);
-                    } else {
-                        handled = fullScroll(View.FOCUS_UP, false);
-                    }
-                    break;
-                case KeyEvent.KEYCODE_DPAD_DOWN:
-                    if (!event.isAltPressed()) {
-                        handled = arrowScroll(View.FOCUS_DOWN, false);
-                    } else {
-                        handled = fullScroll(View.FOCUS_DOWN, false);
-                    }
-                    break;
-                case KeyEvent.KEYCODE_DPAD_LEFT:
-                    if (!event.isAltPressed()) {
-                        handled = arrowScroll(View.FOCUS_LEFT, true);
-                    } else {
-                        handled = fullScroll(View.FOCUS_LEFT, true);
-                    }
-                    break;
-                case KeyEvent.KEYCODE_DPAD_RIGHT:
-                    if (!event.isAltPressed()) {
-                        handled = arrowScroll(View.FOCUS_RIGHT, true);
-                    } else {
-                        handled = fullScroll(View.FOCUS_RIGHT, true);
-                    }
-                    break;
-            }
-        }
-        return handled;
-    }
-
-    @Override
-    public boolean onInterceptTouchEvent(MotionEvent ev) {
-   /*
-   * This method JUST determines whether we want to intercept the motion.
-   * If we return true, onMotionEvent will be called and we do the actual
-   * scrolling there.
-   *
-   * Shortcut the most recurring case: the user is in the dragging
-   * state and he is moving his finger.  We want to intercept this
-   * motion.
-   */
-        final int action = ev.getAction();
-        if ((action == MotionEvent.ACTION_MOVE) && (mIsBeingDragged)) {
-            return true;
-        }
-        if (!canScroll()) {
-            mIsBeingDragged = false;
-            return false;
-        }
-        final float y = ev.getY();
-        final float x = ev.getX();
-        switch (action) {
-            case MotionEvent.ACTION_MOVE:
-       /*
-       * mIsBeingDragged == false, otherwise the shortcut would have caught it. Check
-       * whether the user has moved far enough from his original down touch.
-       */
-       /*
-       * Locally do absolute value. mLastMotionY is set to the y value
-       * of the down event.
-       */
-                final int yDiff = (int) Math.abs(y - mLastMotionY);
-                final int xDiff = (int) Math.abs(x - mLastMotionX);
-                if (yDiff > mTouchSlop || xDiff > mTouchSlop) {
-                    mIsBeingDragged = true;
-                }
-                break;
-
-            case MotionEvent.ACTION_DOWN:
-       /* Remember location of down touch */
-                mLastMotionY = y;
-                mLastMotionX = x;
-
-       /*
-       * If being flinged and user touches the screen, initiate drag;
-       * otherwise don't.  mScroller.isFinished should be false when
-       * being flinged.
-       */
-                mIsBeingDragged = !mScroller.isFinished();
-                break;
-
-            case MotionEvent.ACTION_CANCEL:
-            case MotionEvent.ACTION_UP:
-       /* Release the drag */
-                mIsBeingDragged = false;
-                break;
-        }
-
-   /*
-   * The only time we want to intercept motion events is if we are in the
-   * drag mode.
-   */
-        return mIsBeingDragged;
-    }
-
-    @Override
-    public boolean onTouchEvent(MotionEvent ev) {
-
-        if (ev.getAction() == MotionEvent.ACTION_DOWN && ev.getEdgeFlags() != 0) {
-            // Don't handle edge touches immediately -- they may actually belong to one of our
-            // descendants.
-            return false;
-        }
-
-        if (!canScroll()) {
-            return false;
-        }
-
-        if (mVelocityTracker == null) {
-            mVelocityTracker = VelocityTracker.obtain();
-        }
-        mVelocityTracker.addMovement(ev);
-
-        final int action = ev.getAction();
-        final float y = ev.getY();
-        final float x = ev.getX();
-
-        switch (action) {
-            case MotionEvent.ACTION_DOWN:
-       /*
-       * If being flinged and user touches, stop the fling. isFinished
-       * will be false if being flinged.
-       */
-                if (!mScroller.isFinished()) {
-                    mScroller.abortAnimation();
-                }
-
-                // Remember where the motion event started
-                mLastMotionY = y;
-                mLastMotionX = x;
-                break;
-            case MotionEvent.ACTION_MOVE:
-                // Scroll to follow the motion event
-                int deltaX = (int) (mLastMotionX - x);
-                int deltaY = (int) (mLastMotionY - y);
-                mLastMotionX = x;
-                mLastMotionY = y;
-
-                if (deltaX < 0) {
-                    if (getScrollX() < 0) {
-                        deltaX = 0;
-                    }
-                } else if (deltaX > 0) {
-                    final int rightEdge = getWidth() - getPaddingRight();
-                    final int availableToScroll = getChildAt(0).getRight() - getScrollX() - rightEdge;
-                    if (availableToScroll > 0) {
-                        deltaX = Math.min(availableToScroll, deltaX);
-                    } else {
-                        deltaX = 0;
-                    }
-                }
-                if (deltaY < 0) {
-                    if (getScrollY() < 0) {
-                        deltaY = 0;
-                    }
-                } else if (deltaY > 0) {
-                    final int bottomEdge = getHeight() - getPaddingBottom();
-                    final int availableToScroll = getChildAt(0).getBottom() - getScrollY() - bottomEdge;
-                    if (availableToScroll > 0) {
-                        deltaY = Math.min(availableToScroll, deltaY);
-                    } else {
-                        deltaY = 0;
-                    }
-                }
-                if (deltaY != 0 || deltaX != 0)
-                    scrollBy(deltaX, deltaY);
-                break;
-            case MotionEvent.ACTION_UP:
-                final VelocityTracker velocityTracker = mVelocityTracker;
-                velocityTracker.computeCurrentVelocity(1000, mMaximumVelocity);
-                int initialXVelocity = (int) velocityTracker.getXVelocity();
-                int initialYVelocity = (int) velocityTracker.getYVelocity();
-                if ((Math.abs(initialXVelocity) + Math.abs(initialYVelocity) > mMinimumVelocity) && getChildCount() > 0) {
-                    fling(-initialXVelocity, -initialYVelocity);
-                }
-                if (mVelocityTracker != null) {
-                    mVelocityTracker.recycle();
-                    mVelocityTracker = null;
-                }
-        }
-        return true;
-    }
-
-    /**
-     * Finds the next focusable component that fits in this View's bounds
-     * (excluding fading edges) pretending that this View's top is located at
-     * the parameter top.
-     *
-     * @param topFocus           look for a candidate is the one at the top of the bounds
-     *                           if topFocus is true, or at the bottom of the bounds if topFocus is
-     *                           false
-     * @param top                the top offset of the bounds in which a focusable must be
-     *                           found (the fading edge is assumed to start at this position)
-     * @param preferredFocusable the View that has highest priority and will be
-     *                           returned if it is within my bounds (null is valid)
-     * @return the next focusable component in the bounds or null if none can be
-     *         found
-     */
-    private View findFocusableViewInMyBounds(final boolean topFocus, final int top, final boolean leftFocus, final int left, View preferredFocusable) {
-   /*
-   * The fading edge's transparent side should be considered for focus
-   * since it's mostly visible, so we divide the actual fading edge length
-   * by 2.
-   */
-        final int verticalFadingEdgeLength = getVerticalFadingEdgeLength() / 2;
-        final int topWithoutFadingEdge = top + verticalFadingEdgeLength;
-        final int bottomWithoutFadingEdge = top + getHeight() - verticalFadingEdgeLength;
-        final int horizontalFadingEdgeLength = getHorizontalFadingEdgeLength() / 2;
-        final int leftWithoutFadingEdge = left + horizontalFadingEdgeLength;
-        final int rightWithoutFadingEdge = left + getWidth() - horizontalFadingEdgeLength;
-
-        if ((preferredFocusable != null)
-                && (preferredFocusable.getTop() < bottomWithoutFadingEdge)
-                && (preferredFocusable.getBottom() > topWithoutFadingEdge)
-                && (preferredFocusable.getLeft() < rightWithoutFadingEdge)
-                && (preferredFocusable.getRight() > leftWithoutFadingEdge)) {
-            return preferredFocusable;
-        }
-        return findFocusableViewInBounds(topFocus, topWithoutFadingEdge, bottomWithoutFadingEdge, leftFocus, leftWithoutFadingEdge, rightWithoutFadingEdge);
-    }
-
-    /**
-     * Finds the next focusable component that fits in the specified bounds.
-     * </p>
-     *
-     * @param topFocus look for a candidate is the one at the top of the bounds
-     *                 if topFocus is true, or at the bottom of the bounds if topFocus is
-     *                 false
-     * @param top      the top offset of the bounds in which a focusable must be
-     *                 found
-     * @param bottom   the bottom offset of the bounds in which a focusable must
-     *                 be found
-     * @return the next focusable component in the bounds or null if none can
-     *         be found
-     */
-    private View findFocusableViewInBounds(boolean topFocus, int top, int bottom, boolean leftFocus, int left, int right) {
-        List<View> focusables = getFocusables(View.FOCUS_FORWARD);
-        View focusCandidate = null;
-
-   /*
-   * A fully contained focusable is one where its top is below the bound's
-   * top, and its bottom is above the bound's bottom. A partially
-   * contained focusable is one where some part of it is within the
-   * bounds, but it also has some part that is not within bounds.  A fully contained
-   * focusable is preferred to a partially contained focusable.
-   */
-        boolean foundFullyContainedFocusable = false;
-
-        int count = focusables.size();
-        for (int i = 0; i < count; i++) {
-            View view = focusables.get(i);
-            int viewTop = view.getTop();
-            int viewBottom = view.getBottom();
-            int viewLeft = view.getLeft();
-            int viewRight = view.getRight();
-
-            if (top < viewBottom && viewTop < bottom && left < viewRight && viewLeft < right) {
-       /*
-       * the focusable is in the target area, it is a candidate for
-       * focusing
-       */
-                final boolean viewIsFullyContained = (top < viewTop) && (viewBottom < bottom) && (left < viewLeft) && (viewRight < right);
-                if (focusCandidate == null) {
-         /* No candidate, take this one */
-                    focusCandidate = view;
-                    foundFullyContainedFocusable = viewIsFullyContained;
-                } else {
-                    final boolean viewIsCloserToVerticalBoundary =
-                            (topFocus && viewTop < focusCandidate.getTop()) ||
-                                    (!topFocus && viewBottom > focusCandidate.getBottom());
-                    final boolean viewIsCloserToHorizontalBoundary =
-                            (leftFocus && viewLeft < focusCandidate.getLeft()) ||
-                                    (!leftFocus && viewRight > focusCandidate.getRight());
-                    if (foundFullyContainedFocusable) {
-                        if (viewIsFullyContained && viewIsCloserToVerticalBoundary && viewIsCloserToHorizontalBoundary) {
-             /*
-              * We're dealing with only fully contained views, so
-              * it has to be closer to the boundary to beat our
-              * candidate
-              */
-                            focusCandidate = view;
-                        }
-                    } else {
-                        if (viewIsFullyContained) {
-             /* Any fully contained view beats a partially contained view */
-                            focusCandidate = view;
-                            foundFullyContainedFocusable = true;
-                        } else if (viewIsCloserToVerticalBoundary && viewIsCloserToHorizontalBoundary) {
-             /*
-              * Partially contained view beats another partially
-              * contained view if it's closer
-              */
-                            focusCandidate = view;
-                        }
-                    }
-                }
-            }
-        }
-        return focusCandidate;
-    }
-
-    /**
-     * <p>Handles scrolling in response to a "home/end" shortcut press. This
-     * method will scroll the view to the top or bottom and give the focus
-     * to the topmost/bottommost component in the new visible area. If no
-     * component is a good candidate for focus, this scrollview reclaims the
-     * focus.</p>
-     *
-     * @param direction the scroll direction: {@link android.view.View#FOCUS_UP}
-     *                  to go the top of the view or
-     *                  {@link android.view.View#FOCUS_DOWN} to go the bottom
-     * @return true if the key event is consumed by this method, false otherwise
-     */
-    public boolean fullScroll(int direction, boolean horizontal) {
-        if (!horizontal) {
-            boolean down = direction == View.FOCUS_DOWN;
-            int height = getHeight();
-            mTempRect.top = 0;
-            mTempRect.bottom = height;
-            if (down) {
-                int count = getChildCount();
-                if (count > 0) {
-                    View view = getChildAt(count - 1);
-                    mTempRect.bottom = view.getBottom();
-                    mTempRect.top = mTempRect.bottom - height;
-                }
-            }
-            return scrollAndFocus(direction, mTempRect.top, mTempRect.bottom, 0, 0, 0);
-        } else {
-            boolean right = direction == View.FOCUS_DOWN;
-            int width = getWidth();
-            mTempRect.left = 0;
-            mTempRect.right = width;
-            if (right) {
-                int count = getChildCount();
-                if (count > 0) {
-                    View view = getChildAt(count - 1);
-                    mTempRect.right = view.getBottom();
-                    mTempRect.left = mTempRect.right - width;
-                }
-            }
-            return scrollAndFocus(0, 0, 0, direction, mTempRect.top, mTempRect.bottom);
-        }
-    }
-
-    /**
-     * <p>Scrolls the view to make the area defined by <code>top</code> and
-     * <code>bottom</code> visible. This method attempts to give the focus
-     * to a component visible in this area. If no component can be focused in
-     * the new visible area, the focus is reclaimed by this scrollview.</p>
-     *
-     * @param direction the scroll direction: {@link android.view.View#FOCUS_UP}
-     *                  to go upward
-     *                  {@link android.view.View#FOCUS_DOWN} to downward
-     * @param top       the top offset of the new area to be made visible
-     * @param bottom    the bottom offset of the new area to be made visible
-     * @return true if the key event is consumed by this method, false otherwise
-     */
-    private boolean scrollAndFocus(int directionY, int top, int bottom, int directionX, int left, int right) {
-        boolean handled = true;
-        int height = getHeight();
-        int containerTop = getScrollY();
-        int containerBottom = containerTop + height;
-        boolean up = directionY == View.FOCUS_UP;
-        int width = getWidth();
-        int containerLeft = getScrollX();
-        int containerRight = containerLeft + width;
-        boolean leftwards = directionX == View.FOCUS_UP;
-        View newFocused = findFocusableViewInBounds(up, top, bottom, leftwards, left, right);
-        if (newFocused == null) {
-            newFocused = this;
-        }
-        if ((top >= containerTop && bottom <= containerBottom) || (left >= containerLeft && right <= containerRight)) {
-            handled = false;
-        } else {
-            int deltaY = up ? (top - containerTop) : (bottom - containerBottom);
-            int deltaX = leftwards ? (left - containerLeft) : (right - containerRight);
-            doScroll(deltaX, deltaY);
-        }
-        if (newFocused != findFocus() && newFocused.requestFocus(directionY)) {
-            mTwoDScrollViewMovedFocus = true;
-            mTwoDScrollViewMovedFocus = false;
-        }
-        return handled;
-    }
-
-    /**
-     * Handle scrolling in response to an up or down arrow click.
-     *
-     * @param direction The direction corresponding to the arrow key that was
-     *                  pressed
-     * @return True if we consumed the event, false otherwise
-     */
-    public boolean arrowScroll(int direction, boolean horizontal) {
-        View currentFocused = findFocus();
-        if (currentFocused == this) currentFocused = null;
-        View nextFocused = FocusFinder.getInstance().findNextFocus(this, currentFocused, direction);
-        final int maxJump = horizontal ? getMaxScrollAmountHorizontal() : getMaxScrollAmountVertical();
-
-        if (!horizontal) {
-            if (nextFocused != null) {
-                nextFocused.getDrawingRect(mTempRect);
-                offsetDescendantRectToMyCoords(nextFocused, mTempRect);
-                int scrollDelta = computeScrollDeltaToGetChildRectOnScreen(mTempRect);
-                doScroll(0, scrollDelta);
-                nextFocused.requestFocus(direction);
-            } else {
-                // no new focus
-                int scrollDelta = maxJump;
-                if (direction == View.FOCUS_UP && getScrollY() < scrollDelta) {
-                    scrollDelta = getScrollY();
-                } else if (direction == View.FOCUS_DOWN) {
-                    if (getChildCount() > 0) {
-                        int daBottom = getChildAt(0).getBottom();
-                        int screenBottom = getScrollY() + getHeight();
-                        if (daBottom - screenBottom < maxJump) {
-                            scrollDelta = daBottom - screenBottom;
-                        }
-                    }
-                }
-                if (scrollDelta == 0) {
-                    return false;
-                }
-                doScroll(0, direction == View.FOCUS_DOWN ? scrollDelta : -scrollDelta);
-            }
-        } else {
-            if (nextFocused != null) {
-                nextFocused.getDrawingRect(mTempRect);
-                offsetDescendantRectToMyCoords(nextFocused, mTempRect);
-                int scrollDelta = computeScrollDeltaToGetChildRectOnScreen(mTempRect);
-                doScroll(scrollDelta, 0);
-                nextFocused.requestFocus(direction);
-            } else {
-                // no new focus
-                int scrollDelta = maxJump;
-                if (direction == View.FOCUS_UP && getScrollY() < scrollDelta) {
-                    scrollDelta = getScrollY();
-                } else if (direction == View.FOCUS_DOWN) {
-                    if (getChildCount() > 0) {
-                        int daBottom = getChildAt(0).getBottom();
-                        int screenBottom = getScrollY() + getHeight();
-                        if (daBottom - screenBottom < maxJump) {
-                            scrollDelta = daBottom - screenBottom;
-                        }
-                    }
-                }
-                if (scrollDelta == 0) {
-                    return false;
-                }
-                doScroll(direction == View.FOCUS_DOWN ? scrollDelta : -scrollDelta, 0);
-            }
-        }
-        return true;
-    }
-
-    /**
-     * Smooth scroll by a Y delta
-     *
-     * @param delta the number of pixels to scroll by on the Y axis
-     */
-    private void doScroll(int deltaX, int deltaY) {
-        if (deltaX != 0 || deltaY != 0) {
-            smoothScrollBy(deltaX, deltaY);
-        }
-    }
-
-    /**
-     * Like {@link android.view.View#scrollBy}, but scroll smoothly instead of immediately.
-     *
-     * @param dx the number of pixels to scroll by on the X axis
-     * @param dy the number of pixels to scroll by on the Y axis
-     */
-    public final void smoothScrollBy(int dx, int dy) {
-        long duration = AnimationUtils.currentAnimationTimeMillis() - mLastScroll;
-        if (duration > ANIMATED_SCROLL_GAP) {
-            mScroller.startScroll(getScrollX(), getScrollY(), dx, dy);
-            awakenScrollBars(mScroller.getDuration());
-            invalidate();
-        } else {
-            if (!mScroller.isFinished()) {
-                mScroller.abortAnimation();
-            }
-            scrollBy(dx, dy);
-        }
-        mLastScroll = AnimationUtils.currentAnimationTimeMillis();
-    }
-
-    /**
-     * Like {@link #scrollTo}, but scroll smoothly instead of immediately.
-     *
-     * @param x the position where to scroll on the X axis
-     * @param y the position where to scroll on the Y axis
-     */
-    public final void smoothScrollTo(int x, int y) {
-        smoothScrollBy(x - getScrollX(), y - getScrollY());
-    }
-
-    /**
-     * <p>The scroll range of a scroll view is the overall height of all of its
-     * children.</p>
-     */
-    @Override
-    protected int computeVerticalScrollRange() {
-        int count = getChildCount();
-        return count == 0 ? getHeight() : (getChildAt(0)).getBottom();
-    }
-    @Override
-    protected int computeHorizontalScrollRange() {
-        int count = getChildCount();
-        return count == 0 ? getWidth() : (getChildAt(0)).getRight();
-    }
-
-    @Override
-    protected void measureChild(View child, int parentWidthMeasureSpec, int parentHeightMeasureSpec) {
-        ViewGroup.LayoutParams lp = child.getLayoutParams();
-        int childWidthMeasureSpec;
-        int childHeightMeasureSpec;
-
-        childWidthMeasureSpec = getChildMeasureSpec(parentWidthMeasureSpec, getPaddingLeft() + getPaddingRight(), lp.width);
-        childHeightMeasureSpec = MeasureSpec.makeMeasureSpec(0, MeasureSpec.UNSPECIFIED);
-
-        child.measure(childWidthMeasureSpec, childHeightMeasureSpec);
-    }
-
-    @Override
-    protected void measureChildWithMargins(View child, int parentWidthMeasureSpec, int widthUsed, int parentHeightMeasureSpec, int heightUsed) {
-        final MarginLayoutParams lp = (MarginLayoutParams) child.getLayoutParams();
-        final int childWidthMeasureSpec = getChildMeasureSpec(parentWidthMeasureSpec,
-                getPaddingLeft() + getPaddingRight() + lp.leftMargin + lp.rightMargin + widthUsed, lp.width);
-        final int childHeightMeasureSpec = MeasureSpec.makeMeasureSpec(lp.topMargin + lp.bottomMargin, MeasureSpec.UNSPECIFIED);
-
-        child.measure(childWidthMeasureSpec, childHeightMeasureSpec);
-    }
-
-    @Override
-    public void computeScroll() {
-        if (mScroller.computeScrollOffset()) {
-            // This is called at drawing time by ViewGroup.  We don't want to
-            // re-show the scrollbars at this point, which scrollTo will do,
-            // so we replicate most of scrollTo here.
-            //
-            //         It's a little odd to call onScrollChanged from inside the drawing.
-            //
-            //         It is, except when you remember that computeScroll() is used to
-            //         animate scrolling. So unless we want to defer the onScrollChanged()
-            //         until the end of the animated scrolling, we don't really have a
-            //         choice here.
-            //
-            //         I agree.  The alternative, which I think would be worse, is to post
-            //         something and tell the subclasses later.  This is bad because there
-            //         will be a window where mScrollX/Y is different from what the app
-            //         thinks it is.
-            //
-            int oldX = getScrollX();
-            int oldY = getScrollY();
-            int x = mScroller.getCurrX();
-            int y = mScroller.getCurrY();
-            if (getChildCount() > 0) {
-                View child = getChildAt(0);
-                scrollTo(clamp(x, getWidth() - getPaddingRight() - getPaddingLeft(), child.getWidth()),
-                        clamp(y, getHeight() - getPaddingBottom() - getPaddingTop(), child.getHeight()));
-            } else {
-                scrollTo(x, y);
-            }
-            if (oldX != getScrollX() || oldY != getScrollY()) {
-                onScrollChanged(getScrollX(), getScrollY(), oldX, oldY);
-            }
-
-            // Keep on drawing until the animation has finished.
-            postInvalidate();
-        }
-    }
-
-    /**
-     * Scrolls the view to the given child.
-     *
-     * @param child the View to scroll to
-     */
-    private void scrollToChild(View child) {
-        child.getDrawingRect(mTempRect);
-   /* Offset from child's local coordinates to TwoDScrollView coordinates */
-        offsetDescendantRectToMyCoords(child, mTempRect);
-        int scrollDelta = computeScrollDeltaToGetChildRectOnScreen(mTempRect);
-        if (scrollDelta != 0) {
-            scrollBy(0, scrollDelta);
-        }
-    }
-
-    /**
-     * If rect is off screen, scroll just enough to get it (or at least the
-     * first screen size chunk of it) on screen.
-     *
-     * @param rect      The rectangle.
-     * @param immediate True to scroll immediately without animation
-     * @return true if scrolling was performed
-     */
-    private boolean scrollToChildRect(Rect rect, boolean immediate) {
-        final int delta = computeScrollDeltaToGetChildRectOnScreen(rect);
-        final boolean scroll = delta != 0;
-        if (scroll) {
-            if (immediate) {
-                scrollBy(0, delta);
-            } else {
-                smoothScrollBy(0, delta);
-            }
-        }
-        return scroll;
-    }
-
-    /**
-     * Compute the amount to scroll in the Y direction in order to get
-     * a rectangle completely on the screen (or, if taller than the screen,
-     * at least the first screen size chunk of it).
-     *
-     * @param rect The rect.
-     * @return The scroll delta.
-     */
-    protected int computeScrollDeltaToGetChildRectOnScreen(Rect rect) {
-        if (getChildCount() == 0) return 0;
-        int height = getHeight();
-        int screenTop = getScrollY();
-        int screenBottom = screenTop + height;
-        int fadingEdge = getVerticalFadingEdgeLength();
-        // leave room for top fading edge as long as rect isn't at very top
-        if (rect.top > 0) {
-            screenTop += fadingEdge;
-        }
-
-        // leave room for bottom fading edge as long as rect isn't at very bottom
-        if (rect.bottom < getChildAt(0).getHeight()) {
-            screenBottom -= fadingEdge;
-        }
-        int scrollYDelta = 0;
-        if (rect.bottom > screenBottom && rect.top > screenTop) {
-            // need to move down to get it in view: move down just enough so
-            // that the entire rectangle is in view (or at least the first
-            // screen size chunk).
-            if (rect.height() > height) {
-                // just enough to get screen size chunk on
-                scrollYDelta += (rect.top - screenTop);
-            } else {
-                // get entire rect at bottom of screen
-                scrollYDelta += (rect.bottom - screenBottom);
-            }
-
-            // make sure we aren't scrolling beyond the end of our content
-            int bottom = getChildAt(0).getBottom();
-            int distanceToBottom = bottom - screenBottom;
-            scrollYDelta = Math.min(scrollYDelta, distanceToBottom);
-
-        } else if (rect.top < screenTop && rect.bottom < screenBottom) {
-            // need to move up to get it in view: move up just enough so that
-            // entire rectangle is in view (or at least the first screen
-            // size chunk of it).
-
-            if (rect.height() > height) {
-                // screen size chunk
-                scrollYDelta -= (screenBottom - rect.bottom);
-            } else {
-                // entire rect at top
-                scrollYDelta -= (screenTop - rect.top);
-            }
-
-            // make sure we aren't scrolling any further than the top our content
-            scrollYDelta = Math.max(scrollYDelta, -getScrollY());
-        }
-        return scrollYDelta;
-    }
-
-    @Override
-    public void requestChildFocus(View child, View focused) {
-        if (!mTwoDScrollViewMovedFocus) {
-            if (!mIsLayoutDirty) {
-                scrollToChild(focused);
-            } else {
-                // The child may not be laid out yet, we can't compute the scroll yet
-                mChildToScrollTo = focused;
-            }
-        }
-        super.requestChildFocus(child, focused);
-    }
-
-    /**
-     * When looking for focus in children of a scroll view, need to be a little
-     * more careful not to give focus to something that is scrolled off screen.
-     *
-     * This is more expensive than the default {@link android.view.ViewGroup}
-     * implementation, otherwise this behavior might have been made the default.
-     */
-    @Override
-    protected boolean onRequestFocusInDescendants(int direction, Rect previouslyFocusedRect) {
-        // convert from forward / backward notation to up / down / left / right
-        // (ugh).
-        if (direction == View.FOCUS_FORWARD) {
-            direction = View.FOCUS_DOWN;
-        } else if (direction == View.FOCUS_BACKWARD) {
-            direction = View.FOCUS_UP;
-        }
-
-        final View nextFocus = previouslyFocusedRect == null ?
-                FocusFinder.getInstance().findNextFocus(this, null, direction) :
-                FocusFinder.getInstance().findNextFocusFromRect(this,
-                        previouslyFocusedRect, direction);
-
-        if (nextFocus == null) {
-            return false;
-        }
-
-        return nextFocus.requestFocus(direction, previouslyFocusedRect);
-    }
-
-    @Override
-    public boolean requestChildRectangleOnScreen(View child, Rect rectangle, boolean immediate) {
-        // offset into coordinate space of this scroll view
-        rectangle.offset(child.getLeft() - child.getScrollX(), child.getTop() - child.getScrollY());
-        return scrollToChildRect(rectangle, immediate);
-    }
-
-    @Override
-    public void requestLayout() {
-        mIsLayoutDirty = true;
-        super.requestLayout();
-    }
-
-    @Override
-    protected void onLayout(boolean changed, int l, int t, int r, int b) {
-        super.onLayout(changed, l, t, r, b);
-        mIsLayoutDirty = false;
-        // Give a child focus if it needs it
-        if (mChildToScrollTo != null && isViewDescendantOf(mChildToScrollTo, this)) {
-            scrollToChild(mChildToScrollTo);
-        }
-        mChildToScrollTo = null;
-
-        // Calling this with the present values causes it to re-clam them
-        scrollTo(getScrollX(), getScrollY());
-    }
-
-    @Override
-    protected void onSizeChanged(int w, int h, int oldw, int oldh) {
-        super.onSizeChanged(w, h, oldw, oldh);
-
-        View currentFocused = findFocus();
-        if (null == currentFocused || this == currentFocused)
-            return;
-
-        // If the currently-focused view was visible on the screen when the
-        // screen was at the old height, then scroll the screen to make that
-        // view visible with the new screen height.
-        currentFocused.getDrawingRect(mTempRect);
-        offsetDescendantRectToMyCoords(currentFocused, mTempRect);
-        int scrollDeltaX = computeScrollDeltaToGetChildRectOnScreen(mTempRect);
-        int scrollDeltaY = computeScrollDeltaToGetChildRectOnScreen(mTempRect);
-        doScroll(scrollDeltaX, scrollDeltaY);
-    }
-
-    /**
-     * Return true if child is an descendant of parent, (or equal to the parent).
-     */
-    private boolean isViewDescendantOf(View child, View parent) {
-        if (child == parent) {
-            return true;
-        }
-
-        final ViewParent theParent = child.getParent();
-        return (theParent instanceof ViewGroup) && isViewDescendantOf((View) theParent, parent);
-    }
-
-    /**
-     * Fling the scroll view
-     *
-     * @param velocityY The initial velocity in the Y direction. Positive
-     *                  numbers mean that the finger/curor is moving down the screen,
-     *                  which means we want to scroll towards the top.
-     */
-    public void fling(int velocityX, int velocityY) {
-        if (getChildCount() > 0) {
-            int height = getHeight() - getPaddingBottom() - getPaddingTop();
-            int bottom = getChildAt(0).getHeight();
-            int width = getWidth() - getPaddingRight() - getPaddingLeft();
-            int right = getChildAt(0).getWidth();
-
-            mScroller.fling(getScrollX(), getScrollY(), velocityX, velocityY, 0, right - width, 0, bottom - height);
-
-            final boolean movingDown = velocityY > 0;
-            final boolean movingRight = velocityX > 0;
-
-            View newFocused = findFocusableViewInMyBounds(movingRight, mScroller.getFinalX(), movingDown, mScroller.getFinalY(), findFocus());
-            if (newFocused == null) {
-                newFocused = this;
-            }
-
-            if (newFocused != findFocus() && newFocused.requestFocus(movingDown ? View.FOCUS_DOWN : View.FOCUS_UP)) {
-                mTwoDScrollViewMovedFocus = true;
-                mTwoDScrollViewMovedFocus = false;
-            }
-
-            awakenScrollBars(mScroller.getDuration());
-            invalidate();
-        }
-    }
-
-    /**
-     * {@inheritDoc}
-     *
-     * <p>This version also clamps the scrolling to the bounds of our child.
-     */
-    public void scrollTo(int x, int y) {
-        // we rely on the fact the View.scrollBy calls scrollTo.
-        if (getChildCount() > 0) {
-            View child = getChildAt(0);
-            x = clamp(x, getWidth() - getPaddingRight() - getPaddingLeft(), child.getWidth());
-            y = clamp(y, getHeight() - getPaddingBottom() - getPaddingTop(), child.getHeight());
-            if (x != getScrollX() || y != getScrollY()) {
-                super.scrollTo(x, y);
-            }
-        }
-    }
-
-    private int clamp(int n, int my, int child) {
-        if (my >= child || n < 0) {
-     /* my >= child is this case:
-      *                    |--------------- me ---------------|
-      *     |------ child ------|
-      * or
-      *     |--------------- me ---------------|
-      *            |------ child ------|
-      * or
-      *     |--------------- me ---------------|
-      *                                  |------ child ------|
-      *
-      * n < 0 is this case:
-      *     |------ me ------|
-      *                    |-------- child --------|
-      *     |-- mScrollX --|
-      */
-            return 0;
-        }
-        if ((my+n) > child) {
-     /* this case:
-      *                    |------ me ------|
-      *     |------ child ------|
-      *     |-- mScrollX --|
-      */
-            return child-my;
-        }
-        return n;
-    }
-}
index 309cb4c637b9c4809a0a37ebd90b88c622d733ed..c5885a0108d0ee860cdd118220751da0fe62b696 100755 (executable)
@@ -8,7 +8,7 @@ public class UndefinedFormula implements Formula{
 
     Paint p=new Paint();
     int priority;
-    boolean currentF;
+    boolean currentF; //indica se la formula è quella su cui sta lavorando il parser per l'inserimento di ipotesi
     UndefinedFormula()
     {
         priority=100;
@@ -16,13 +16,13 @@ public class UndefinedFormula implements Formula{
     }
     public String Draw(int x)
     {
-        if(currentF)
+        if(currentF) //la formula corrente visualizza un _
             return "_";
         else
            return " ";
     }
     public String toString(){return Draw(0);}
-    public String toStringDeleted(){return null;} //UndefinedFormula should never be deleted
+    public String toStringDeleted(){return null;} //UndefinedFormula non può essere scaricata
     public float size(){
         p.setTextSize(DrawActivity.textSize);
         return p.measureText(toString());
@@ -30,11 +30,11 @@ public class UndefinedFormula implements Formula{
     public float height()
     {
         return 0;
-    }
+    } //UndefinedFormula non ha dimensioni e non accetta regole
     public float sizeDeleted(){return(0);}
     public List<IntroductionRule> introductionRules(){
         return null;
-    } //UndefinedFormula accepts no rules
+    }
     public List<EliminationRule> EliminationRules(){
         return null;
     }
index a97220e983a57be932289b35a628719f4b9916a4..7ea276dcf5c58387f7694937cd45f529c603b25f 100755 (executable)
@@ -4,7 +4,6 @@ package com.example.furt.myapplication;
 import android.content.Context;
 import android.os.AsyncTask;
 import android.os.Environment;
-import android.util.Log;
 import android.widget.Toast;
 
 import java.io.File;
@@ -64,8 +63,7 @@ public class aggiorna {
         personalDBHelper connessione = new personalDBHelper(aggiornamento.t.getContext());
         List<listElem> esercizi=connessione.getElem(user);
         if(esercizi!=null && !esercizi.isEmpty()) {
-            for (listElem esercizio : esercizi) {
-                Log.e("",esercizio.getEsercizio());}
+
             for (listElem esercizio : esercizi) {
                 String richiesta = "8/" + sessionKey + "/" + esercizio.getEsercizio() + "/" + esercizio.getMd5() + "/" + esercizio.getTime() + "/" + esercizio.getClick();
                 String ritorno = serverComunication.connessione(richiesta);
index c3893fe2c679f40df79d2b49b50f86779a4b1209..ee114a9127c55ce92881a416b63f98f71cd7bc3a 100755 (executable)
@@ -3,7 +3,6 @@ package com.example.furt.myapplication;
 import android.app.Activity;
 import android.content.Intent;
 import android.os.Bundle;
-import android.util.Log;
 import android.widget.RelativeLayout;
 
 
@@ -24,7 +23,6 @@ public class aggiornamento extends Activity
             sessionKey = serverComunication.connessione("1/" + user + "/" + pass);
             if(sessionKey.contentEquals("request-login") || sessionKey.contains("err"))
             {
-                Log.e("", "ciao");
                 Intent i = new Intent(getApplicationContext(), mainActivity.class);
                 i.putExtra("logout", "si");
                 i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK);
index a6fb161016d779863177bffb32a4737ae0a6e01f..ca15a35f976e72625367f861ac067270b774db97 100755 (executable)
@@ -1,5 +1,8 @@
 package com.example.furt.myapplication;
 
+/**
+ * askFormula(): callback per ottenere informazioni aggiuntive sulla regola da applicare
+ */
 public class askFormula{
     public Formula Ask(){return DrawActivity.selectedNode.F;};
 }
index 119381572faae7f8c57215980b14a4139f28e522..4541b317151b4e92f8e5f5fef625a02e38ebd32b 100755 (executable)
@@ -96,7 +96,13 @@ public class download_page extends Activity
         getMenuInflater().inflate(R.menu.menu_dow, menu);
         return true;
     }
-
+    @Override
+    public void onBackPressed() {
+        Intent i = new Intent(getApplicationContext(), mainActivity.class);
+        i.putExtra("logout","si");
+        i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK);
+        getApplicationContext().startActivity(i);
+    }
 
     @Override
     public boolean onOptionsItemSelected(MenuItem item) {
@@ -104,6 +110,7 @@ public class download_page extends Activity
         // automatically handle clicks on the Home/Up button, so long
         // as you specify a parent activity in AndroidManifest.xml.
         int id = item.getItemId();
+
         if(id==R.id.aggiorna)
         {
             Intent i = new Intent(getApplicationContext(), aggiornamento.class);
diff --git a/mainActivity/src/com/example/furt/myapplication/longnodeHandler.java b/mainActivity/src/com/example/furt/myapplication/longnodeHandler.java
new file mode 100644 (file)
index 0000000..b17796d
--- /dev/null
@@ -0,0 +1,26 @@
+package com.example.furt.myapplication;
+
+import android.view.View;
+
+/**LongNodeHandler: handler per la pressione prolungata di un nodo**/
+
+public class longnodeHandler implements View.OnLongClickListener {
+    Node n; //nodo a cui è legato questo handler
+
+    longnodeHandler(Node node) {
+        n = node;
+    }
+
+    @Override
+    public boolean onLongClick(View view) {
+        if (DrawActivity.selectedNode != null)
+            if (DrawActivity.selectedNode.view == view) {
+                if (DrawActivity.selectedNode.Children.size() == 0) { //se l'hold click è stato fatto sul selectedNode ed esso è un nodo foglia
+                        touchnodeHandler.ruleDialog = new RuleDialog(DrawActivity.selectedNode.F.introductionRules());
+                        touchnodeHandler.ruleDialog.showAllRules=true; //nuovo ruleDialog con l'opzione showAllRules già settata
+                        touchnodeHandler.ruleDialog.show(DrawActivity.fragmentManager, "CIAO");
+                }
+            }
+        return true;
+    }
+}
index 1c6814827487a460f21d68a76324783278e99c94..3f456a5c9d3932a0adfcb281ca6ef2285ba541f2 100755 (executable)
@@ -72,6 +72,8 @@ public class mainActivity extends Activity {
                                 i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK);
                                 getApplicationContext().startActivity(i);//avvio la "aggiornamento.class"
                             }
+                            else
+                                Toast.makeText(getApplicationContext(),"credenziali errate", Toast.LENGTH_SHORT).show();
                         }
                     } catch (Exception e) {
                         e.printStackTrace();
index e871b7f21a07059a3b992f5a08f7757350f24b9a..ccc18ccb295b41a5b519d1f0a885a0702b955230 100755 (executable)
@@ -5,13 +5,13 @@ import android.app.Dialog;
 import android.app.DialogFragment;
 import android.content.DialogInterface;
 import android.os.Bundle;
-import android.util.Log;
 import android.view.LayoutInflater;
 import android.view.View;
 import android.view.ViewGroup;
 import android.widget.Button;
 import android.widget.RelativeLayout;
 import android.widget.TextView;
+import android.widget.Toast;
 
 import java.util.ArrayList;
 import java.util.List;
@@ -20,7 +20,6 @@ public class parserDialog extends DialogFragment {
     static Formula F=null; //formula che sto costruendo
     static RelativeLayout formulaLayout;
     static TextView FView; //View contenente la formula che sto visualizzando
-    static Button dismissButton;
     static boolean reload=false;
     static ArrayList<String> esliter=new ArrayList<String>();
     static ArrayList<Formula> undo=new ArrayList<Formula>();
@@ -35,7 +34,6 @@ public class parserDialog extends DialogFragment {
             F.setCursor();
         }
         esliter.addAll(parser.getLiteral(DrawActivity.nomeEs));
-        Log.e("","⊤");
     }
     @Override
     public Dialog onCreateDialog(final Bundle savedInstanceState) {
@@ -110,24 +108,32 @@ public class parserDialog extends DialogFragment {
             public void onClick(DialogInterface dialog, int id) {
                 if(!F.toString().contains("_")) {
                     List<EliminationRule> L = F.EliminationRules();
-                    if (L.size()==0)
+                    if (L.size()==0){
+                        F=null;
+                        Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare questa ipotesi ora",Toast.LENGTH_LONG).show();
                         return;
+                    }
+                    if (F.toString().equals(DrawActivity.selectedNode.F.toString())) //sto provando a scaricare il nodo selezionato
+                    {
+                        Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare un nodo aperto senza dimostrarlo",Toast.LENGTH_LONG).show();
+                        F=null;
+                        return;
+                    }
                     touchHPHandler t = new touchHPHandler(L.get(0).createNodes(null, new askFormula()),new Hypothesis(F,true));
                     F = null;
                     t.discard=false;
                     t.onClick(null);
                 }
-                else
+                else{
+                    Toast.makeText(DrawActivity.rootNode.view.getContext(),"Completa l'inserimento!",Toast.LENGTH_SHORT).show();
                     reboot();
+                }
             }
         });
         builder.setNeutralButton("Undo", new DialogInterface.OnClickListener() {
             public void onClick(DialogInterface dialog, int id) {
                 if(undo.size()>1) {
                     F = undo.remove(undo.size() - 1);
-                    /*for(int i=0;i<undo.size();i++) {
-                        Log.e(String.valueOf(i), undo.get(i).toString());
-                    }*/
                 }
                 else
                     F=null;
index 612af06d1b1666bcb8c5c367aa4fba1a8d505812..0dfe4253034b9836f599a92a26fdc0050b7e139d 100644 (file)
@@ -36,6 +36,7 @@ public class recuperaPass extends Activity{
                     String request = serverComunication.connessioneMain("a0/" + utente + "/" + oldPass + "/" + newPass );
                     if(!request.contains("error"))
                     {
+                        Toast.makeText(getApplicationContext(), "password cambiata", Toast.LENGTH_SHORT).show();
                         Intent i = new Intent(getApplicationContext(), mainActivity.class);
                         i.putExtra("logout", "si");
                         i.addFlags(Intent.FLAG_ACTIVITY_NEW_TASK);
index 9ac2c79818b5609960d2abd0cae0124b6fd573af..a82ea2770905df78f87cf7c00b72f6f56ad9fe4c 100755 (executable)
@@ -43,7 +43,17 @@ public class serverComunication
         return null;
     }
 
-
+    static String connessioneMain(String parametri)
+    {
+        try {
+            return new richiestaServerMain().execute(parametri).get();
+        } catch (InterruptedException e) {
+            e.printStackTrace();
+        } catch (ExecutionException e) {
+            e.printStackTrace();
+        }
+        return null;
+    }
 
     static class richiestaServer extends AsyncTask<String, String, String> {
         @Override
@@ -105,21 +115,7 @@ public class serverComunication
         }
     }
 
-    public static String connessioneMain(String parametri)
-    {
-        try {
-            return new richiestaServerMain().execute(parametri).get();
-        } catch (InterruptedException e) {
-            e.printStackTrace();
-        } catch (ExecutionException e) {
-            e.printStackTrace();
-        }
-        return null;
-    }
-
-
-
-    static class richiestaServerMain extends AsyncTask<String, String, String> {
+   public static class richiestaServerMain extends AsyncTask<String, String, String> {
         @Override
         protected String doInBackground(String... params)
         {
index 44691ce165ca0740e5b043b3e10e60c87c083bce..0e62a534947d999d3465ac0a245cf16a21549944 100755 (executable)
@@ -1,10 +1,11 @@
 package com.example.furt.myapplication;
 
 import android.view.View;
+import android.widget.Toast;
 
 public class touchHPHandler implements View.OnClickListener
 {
-    Node L;
+    Node L; //nodo contenente il sottoalbero successivo all'eliminazione dell'ipotesi
     boolean discard;
     Hypothesis thisHP; //ipotesi che sto eliminando
     touchHPHandler(Node n,Hypothesis hp)
@@ -15,13 +16,14 @@ public class touchHPHandler implements View.OnClickListener
     }
     public void onClick(View view)
     {
-        if (DrawActivity.selectedNode==null) //non-existent selectedNode (should never happen)
+        if (DrawActivity.selectedNode==null) //selectedNode non esiste (non dovrebbe mai succedere)
             return;
-        if (DrawActivity.selectedNode.Children.size()!=0) //not a leaf: can't add children
+        if (DrawActivity.selectedNode.Children.size()!=0) //non è una foglia: non si possono applicare regole.
         {
+            Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare ipotesi su nodi intermedi",Toast.LENGTH_LONG).show();
             return;
         }
-        if (thisHP.HP.toString().equals(DrawActivity.selectedNode.F.toString())) //close current Node
+        if (thisHP.HP.toString().equals(DrawActivity.selectedNode.F.toString())) //sto scaricando una formula uguale al nodo corrente: lo chiudo aggiornando lo stato del nodo
         {
             if (thisHP.isDeleted) {
                 if (DrawActivity.selectedNode.status == Node.OPEN)
@@ -39,17 +41,21 @@ public class touchHPHandler implements View.OnClickListener
             DrawActivity.startDraw();
             return;
         }
-        if (L==null) //incompatible elimination
+        if (L==null) //eliminazione incompatibile con il nodo attuale
+        {
+            Toast.makeText(DrawActivity.rootNode.view.getContext(),"Impossibile scaricare questa ipotesi ora",Toast.LENGTH_LONG).show();
             return;
-        for (Node n:L.Children) {
+        }
+        for (Node n:L.Children) { //aggiungo al sottoalbero della regola da applicare tutte le ipotesi del selectedNode. In più aggiungo alle ipotesi introdotte da questa regola il fromNode corretto.
             for (Hypothesis hp:n.NodeHP)
                 hp.fromNode= DrawActivity.selectedNode; //le ipotesi dei nuovi figli provengono dal nodo in cui stanno per essere inserite
             n.addHPList(DrawActivity.selectedNode.NodeHP);
             DrawActivity.selectedNode.addChild(n);
         }
-        DrawActivity.selectedNode.hasFocus=false;
-        DrawActivity.selectedNode.Children.get(0).hasFocus=true;
-        if(discard) {
+        DrawActivity.selectedNode.hasFocus=false; //il nodo su cui ho applicato la regola non è più una foglia e non ha più focus
+        DrawActivity.selectedNode.ruleName = L.ruleName;
+        DrawActivity.selectedNode.Children.get(0).hasFocus=true; //il primo figlio dell'applicazione della regola ha di default il focus
+        if(discard) { //sto scaricando un'ipotesi: il primo figlio è automaticamente chiuso
             if (thisHP.isDeleted)
                 DrawActivity.selectedNode.Children.get(0).status = Node.CANCELED;
             else
@@ -57,8 +63,6 @@ public class touchHPHandler implements View.OnClickListener
         }
         else
             DrawActivity.selectedNode.Children.get(0).status= Node.OPEN;
-        DrawActivity.selectedNode.hasFocus = false;
-        DrawActivity.selectedNode.ruleName = L.ruleName;
         DrawActivity.nmoves++;
         DrawActivity.rootNode.Clean();
         DrawActivity.startDraw();
index 464cc09c9bfe8aedd11a9d539b6432596a99c720..655901f4da3cfbdbb16d679196188b4313946a6b 100755 (executable)
@@ -2,6 +2,7 @@ package com.example.furt.myapplication;
 
 import android.view.View;
 import android.widget.TextView;
+import android.widget.Toast;
 
 public class touchParserHandler implements View.OnClickListener
 {
@@ -14,6 +15,11 @@ public class touchParserHandler implements View.OnClickListener
     }
     public void onClick(View view)
     {
+        if(!parserDialog.F.toString().contains("_"))
+        {
+            Toast.makeText(DrawActivity.rootNode.view.getContext(),"Formula completa! Premere \"Undo\" per modificare", Toast.LENGTH_SHORT).show();
+            return;
+        }
         parserDialog.undo.add(parserDialog.F.duplicate());
         parserDialog.formulaLayout.removeAllViews();
         if(type==0)
diff --git a/mainActivity/src/com/example/furt/myapplication/touchRuleHandler.java b/mainActivity/src/com/example/furt/myapplication/touchRuleHandler.java
deleted file mode 100755 (executable)
index 7443ebc..0000000
+++ /dev/null
@@ -1,30 +0,0 @@
-package com.example.furt.myapplication;
-import android.view.View;
-
-import java.util.List;
-
-public class touchRuleHandler implements View.OnClickListener
-{
-    List<Node> L;
-    touchRuleHandler(List<Node> list)
-    {
-        L=list;
-    }
-    public void onClick(View view)
-    {
-        if (DrawActivity.selectedNode.Children.size()!=0) //not a leaf: can't add children
-            return;
-        for (Node n:L) {
-            for (Hypothesis hp:n.NodeHP)
-                hp.fromNode= DrawActivity.selectedNode; //le ipotesi dei nuovi figli provengono dal nodo in cui stanno per essere inserite
-            n.addHPList(DrawActivity.selectedNode.NodeHP);
-            DrawActivity.selectedNode.addChild(n);
-        }
-        DrawActivity.selectedNode.hasFocus=false;
-        DrawActivity.selectedNode.ruleName=L.get(0).ruleName;
-        DrawActivity.selectedNode.Children.get(0).hasFocus=true;
-        DrawActivity.nmoves++;
-        DrawActivity.rootNode.Clean();
-        DrawActivity.startDraw();
-    }
-}
index 4fcb64de0fa96094622599f734c643f1c7483922..002fb00a2020bc831a9b6aff7eb4d79b286c41f4 100755 (executable)
@@ -1,39 +1,39 @@
 package com.example.furt.myapplication;
 
 import android.graphics.Color;
+import android.graphics.Paint;
 import android.util.TypedValue;
 import android.view.View;
 import android.view.ViewGroup;
 import android.widget.Button;
 import android.widget.RelativeLayout;
 import android.widget.TextView;
-import android.util.Log;
-import android.graphics.Paint;
 
 import java.util.ArrayList;
 import java.util.List;
 
 public class touchnodeHandler implements View.OnClickListener {
-
-    Node n;
+    static RuleDialog ruleDialog; //il ruleDialog da far comparire nel caso in cui l'utente voglia visualizzare le regole di introduzione disponibili
+    Node n; //nodo a cui è legato questo handler
     touchnodeHandler(Node node) {
-        n=node;
+        n=node; ruleDialog=null;
     }
     @Override
     public void onClick(View view) {
+        Paint p=new Paint();
+        n.hasFocus=true; //il nodo cliccato ha il focus
         TextView v=(TextView)view;
-        v.setTextColor(Color.RED);
+        v.setTextColor(Color.RED); //colorazione rossa per il nodo
         if (DrawActivity.selectedNode!=null)
-            if (DrawActivity.selectedNode.view==view) {
+            if (DrawActivity.selectedNode.view==view) { //doppio clic sul nodo: parte il Dialog per le regole di introduzione
                 if (DrawActivity.selectedNode.Children.size()==0){
                     List<IntroductionRule> L=new ArrayList<IntroductionRule>();
-
                     for (IntroductionRule r: DrawActivity.selectedNode.F.introductionRules())
                     {
-                        if (r.getPriority()!=0)
+                        if (r.getPriority()!=0) //short click: aggiungo solo le regole a priorità alta
                             L.add(r);
                     }
-                    if (L.size()==1)
+                    if (L.size()==1) //c'è una sola regola: la applico immediatamente.
                     {
                         Node selectedRule=L.get(0).createNodes(new askFormula());
                         for (Node n : selectedRule.Children) {
@@ -49,13 +49,15 @@ public class touchnodeHandler implements View.OnClickListener {
                         DrawActivity.nmoves++;
                         DrawActivity.rootNode.Clean();
                         DrawActivity.startDraw();
+                        return;
                     }
                     else {
-                        RuleDialog ruleDialog = new RuleDialog(DrawActivity.selectedNode.F.introductionRules());
+                        //parte il ruleDialog
+                        ruleDialog = new RuleDialog(DrawActivity.selectedNode.F.introductionRules());
                         ruleDialog.show(DrawActivity.fragmentManager, "CIAO");
                     }
                 }
-                else
+                else //nodo intermedio: parte il Dialog per le operazioni di copia/cancella
                 {
                     CopyPasteDialog copyPasteDialog=new CopyPasteDialog(DrawActivity.selectedNode);
                     copyPasteDialog.show(DrawActivity.fragmentManager,"");
@@ -63,38 +65,18 @@ public class touchnodeHandler implements View.OnClickListener {
                 return;
             }
         int i,size;
-        if (DrawActivity.selectedNode!=null) {
+        if (DrawActivity.selectedNode!=null) { //c'era già un selectedNode: lo ricoloro adeguatamente.
             if(DrawActivity.selectedNode.status==Node.OPEN || DrawActivity.selectedNode.status==Node.FAKE)
                 DrawActivity.selectedNode.view.setTextColor(Color.BLACK);
             else
                 DrawActivity.selectedNode.view.setTextColor(Color.GRAY);
         }
         DrawActivity.selectedNode = n;
-        DrawActivity.globalHP.removeAllViews();
-        size = n.NodeHP.size();
-        int leftID=0;
-        int headID=0;
-        float sum=0;
-        final Button elim=new Button(view.getContext());
-        String newText = "Nuova";
-        elim.setText(newText);
-        elim.setTextSize(TypedValue.COMPLEX_UNIT_SP,16);
-        elim.setId(DrawActivity.globalId++);
-        RelativeLayout.LayoutParams myP2=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
-        elim.setLayoutParams(myP2);
-        elim.setOnClickListener(new View.OnClickListener() {
-            @Override
-            public void onClick(View v) {
-                parserDialog p=new parserDialog();
-                p.show(DrawActivity.fragmentManager, ""); //parte l'editor per inserire nuove formule
-            }
-        });
-        DrawActivity.globalHP.addView(elim);
-        Paint p = new Paint();
-        p.setTextSize(DrawActivity.textSize);
-        float newSize=p.measureText(newText)+(float)(p.measureText(newText)*0.20) + 200;
-        sum+=newSize;
-        leftID=elim.getId();
+        DrawActivity.globalHP.removeAllViews(); //rimuovo le eventuali vecchie ipotesi per mostrare quelle del nuovo selectedNode
+        size = n.NodeHP.size(); //numero di ipotesi
+        int leftID=0; //ID dell'eventuale ipotesi a destra della quale dev'essere posizionata l'ipotesi (0=assente)
+        int headID=0; //ID dell'eventuale ipotesi sotto la quale deve comparire l'ipotesi (0=assente)
+        float sum=0; //lunghezza raggiunta finora: se supera la larghezza dello schermo devo andare a capo
         for (i = 0; i<size; i++) //fa apparire le ipotesi cancellate
         {
             final TextView newT=new TextView(view.getContext());
@@ -102,40 +84,49 @@ public class touchnodeHandler implements View.OnClickListener {
             newT.setText(n.NodeHP.get(i).HP.toString());
             newT.setTextSize(TypedValue.COMPLEX_UNIT_SP,30);
             newT.setId(DrawActivity.globalId++);
+            if (i==0) //prima ipotesi: sarà il leftID per le successive
+                leftID=newT.getId();
             myP.setMargins(50,0,0,0);
-            sum+=n.NodeHP.get(i).HP.size();
-            if (sum>(DrawActivity.v.widthPixels/1.5)) //ho superato la larghezza dello schermo: devo andare a capo
+            float thisSize;
+            p.setTextSize(30);
+            thisSize=p.measureText(newT.getText().toString()); //misuro la larghezza dell'ipotesi inserita
+            thisSize+=thisSize*0.2; //con un'approssimazione per eccesso del 20%
+            sum+=thisSize; //aggiungo alla somma totale la larghezza di questa ipotesi e della spaziatura
+            sum+=50;
+            if (sum>(DrawActivity.v.widthPixels+20)) //ho superato la larghezza dello schermo: devo andare a capo
             {
-                sum=n.NodeHP.get(i).HP.size();
-                headID=leftID;
+                sum=thisSize; //il nuovo nodo è il primo della nuova riga
+                headID=leftID; //tutti gli altri devono stare sotto un nodo della riga precedente
             }
             else
-                myP.addRule(RelativeLayout.RIGHT_OF,leftID);
+                myP.addRule(RelativeLayout.RIGHT_OF,leftID); //non vado a capo: mi limito a posizionarmi a destra del leftID
             if (headID!=0)
-                myP.addRule(RelativeLayout.BELOW,headID);
+                myP.addRule(RelativeLayout.BELOW,headID); //mi posiziono sotto l'headID se esiste
             newT.setLayoutParams(myP);
             List<EliminationRule> R=n.NodeHP.get(i).HP.EliminationRules();
-            if (R.size()!=0) {
+            if (R.size()!=0) { //ci sono regole di eliminazione per questa formula
                 Node L= R.get(0).createNodes(null,new askFormula());
                 newT.setOnClickListener(new touchHPHandler(L,n.NodeHP.get(i)));
             }
-            else
+            else //setto comunuqe il listener nel caso in cui la formula venga scaricata
                 newT.setOnClickListener(new touchHPHandler(null,n.NodeHP.get(i)));
-            newT.setOnLongClickListener(new LongHPClick(n.NodeHP.get(i).fromNode));
-            leftID=newT.getId();
+            newT.setOnLongClickListener(new LongHPClick(n.NodeHP.get(i).fromNode)); //setto un longclick listener che mostra il nodo da cui viene l'ipotesi
+            leftID=newT.getId(); //aggiorno il leftID
             DrawActivity.globalHP.addView(newT);
         }
-/*
+        //disegno il bottone utilizzando lo stesso algoritmo utilizzato per le ipotesi
+
         final Button elim=new Button(view.getContext());
         RelativeLayout.LayoutParams myP=new RelativeLayout.LayoutParams(ViewGroup.LayoutParams.WRAP_CONTENT, ViewGroup.LayoutParams.WRAP_CONTENT);
-        elim.setText("Nuova");
+        elim.setText("Nuova...");
         elim.setTextSize(TypedValue.COMPLEX_UNIT_SP,16);
         elim.setId(DrawActivity.globalId++);
         myP.setMargins(50,0,0,0);
-        sum+=elim.getWidth();
+        p.setTextSize(16);
+        float buttonSize=p.measureText("Nuova...");
+        sum+=buttonSize;
         if (sum>(DrawActivity.v.widthPixels/1.5)) //ho superato la larghezza dello schermo: devo andare a capo
         {
-            sum=n.NodeHP.get(i).HP.size();
             headID=leftID;
         }
         else
@@ -151,7 +142,7 @@ public class touchnodeHandler implements View.OnClickListener {
             }
         });
         DrawActivity.globalHP.addView(elim);
-*/
-
     }
 }
+
+