]> matita.cs.unibo.it Git - logicplayer.git/blobdiff - mainActivity/src/com/example/furt/myapplication/parserDialog.java
New version (to be tested).
[logicplayer.git] / mainActivity / src / com / example / furt / myapplication / parserDialog.java
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;