diff --git a/clause_frame.py b/clause_frame.py index d26a58f..c102f7b 100644 --- a/clause_frame.py +++ b/clause_frame.py @@ -27,11 +27,7 @@ def __init__(self, app, canvas, master=None, **kwargs): # make and grid the valid text in the frame self.valid = ttk.Label(self, textvariable=self.info) - self.valid.grid(row=1, sticky=(W)) - - # make and grid the check button in the frame - self.check = ttk.Button(self, text="✓", width=3) - self.check.grid(row=1, sticky=(E)) + self.valid.grid(row=1, sticky=(W,E)) # bindings self.bind("", self.clicked) diff --git a/gui_main.py b/gui_main.py index 360e5a0..6a06851 100644 --- a/gui_main.py +++ b/gui_main.py @@ -51,6 +51,10 @@ def get_help(self, *args): def show_error(self, error_text): error_window = InfoWindow(self.root, "Error Window!", error_text) + # used to display an successful resolution to the user + def show_success(self, success_text): + success_window = InfoWindow(self.root, "Success Window!", success_text) + def update_clause_premise(self, index, conclusion=False): # get the clause frame that is selected clause = self.canvas.frames[self.selected_clause_id] @@ -92,13 +96,12 @@ def create_menu(self): self.menubar.add_command(label="Help", command=self.get_help) self.filemenu.add_command(label='Open') - self.filemenu.add_command(label='Save', command=self.save) - self.filemenu.add_command(label='Save As', command=self.saveas) + self.filemenu.add_command(label='Save') + self.filemenu.add_command(label='Save As') self.root.configure(menu=self.menubar) def save(self, *args): - #InfoWindow(self.root, "Save Window!", self.canvas.get_save_string()) if not self.filename: self.saveas() else: @@ -132,6 +135,10 @@ def set_row_col(self): self.leftframe.grid_rowconfigure(0, weight=5) self.leftframe.grid_rowconfigure(1, weight=1) + def success(self, text): + self.show_success(text) + self.canvas.success() + def start(self): self.root.mainloop() diff --git a/info_window.py b/info_window.py index 380446b..d9d174d 100644 --- a/info_window.py +++ b/info_window.py @@ -15,8 +15,9 @@ def __init__(self, master, title, text_or_file, file=False): if file: with open(text_or_file, 'r') as f: text = f.read() + + s = ttk.Style() + s.configure('Label1.TLabel', background="white") - label = Text(window, wrap="word") - label.insert("1.0", text) - label.configure(state="disabled") + label = ttk.Label(window, text=text, anchor=W, style='Label1.TLabel') label.grid(row=0, column=0, padx=10, pady=10, sticky=(N,S,E,W)) diff --git a/resolution_canvas.py b/resolution_canvas.py index 0dc9521..ffbbd7e 100644 --- a/resolution_canvas.py +++ b/resolution_canvas.py @@ -253,6 +253,10 @@ def get_save_string(self): string += "\n" return string + + def success(self): + for frame in self.frames.values(): + frame.info.set("valid!") diff --git a/resolution_engine.py b/resolution_engine.py index f119a98..1378a7f 100644 --- a/resolution_engine.py +++ b/resolution_engine.py @@ -71,6 +71,9 @@ def __init__(self, master, app, **kwargs): self.app = app # the parent app def verify_all(self): + # used to return errors to user + errorstr = "" + premise_listbox = self.app.leftframe.plist conclusion_listbox = self.app.leftframe.clist plist_exps = list() @@ -80,7 +83,8 @@ def verify_all(self): # parse all premises if premise_listbox.size() < 1: - print("ERROR: no premises") + errorstr += "ERROR: no premises\n" + self.app.show_error(errorstr) return for i in range(premise_listbox.size()): @@ -97,16 +101,18 @@ def verify_all(self): #premises_OR[pstr] = remove_outer_parens(part) this_lis.append(remove_outer_parens(part).upper()) else: - print("ERROR: premise '" + str(premise_listbox.get(i)) - + "' is not in CNF!") + errorstr += str("ERROR: premise '" + str(premise_listbox.get(i)) + + "' is not in CNF!\n") + self.app.show_error(errorstr) return premises_OR[pstr] = this_lis plist_exps.append(this_exp) except pyparse.ParseException: - print("ERROR: could not parse '" + str(premise_listbox.get(i)) - + "'") + errorstr += str("ERROR: could not parse '" + str(premise_listbox.get(i)) + + "'\n") ## INCOMP! Need to show verification failed in GUI + self.app.show_error(errorstr) return # parse the conclusion @@ -120,11 +126,13 @@ def verify_all(self): if paren_even(strip_all(part)): concl_OR.append(remove_outer_parens(strip_all(part)).upper()) else: - print("ERROR: conclusion does not validate to CNF!") + errorstr += "ERROR: conclusion does not validate to CNF!\n" + self.app.show_error(errorstr) return except pyparse.ParseException: - print("ERROR: could not parse '" + str(conclusion_listbox.get(0)) - + "'") + errorstr += str("ERROR: could not parse '" + str(conclusion_listbox.get(0)) + + "'\n") + self.app.show_error(errorstr) return # You might be wondering, shouldn't we invert the conclusion? @@ -133,7 +141,8 @@ def verify_all(self): try: premises_check = pyp.proves(plist_exps, concl_exp) except: # leave this exception generic - print("ERROR: premises or conclusion unsound") + errorstr += "ERROR: premises or conclusion unsound\n" + self.app.show_error(errorstr) return #print("Premises and conclusion are sound: " + str(premises_check)) ## INCOMP! Need to display in GUI @@ -200,12 +209,14 @@ def verify_all(self): concl_OR.remove(crop_str) else: # error triggered if clause is tagging the wrong premise - print("ERROR: clause '" + part_str + "' does not match " - + "the premise tagged") + errorstr += str("ERROR: clause '" + part_str + "' does not match " + + "the premise tagged\n") + self.app.show_error(errorstr) return except KeyError: - print("ERROR: clause '" + part_str + "' is pointing " - + "to a nonexistent premise") + errorstr += str("ERROR: clause '" + part_str + "' is pointing " + + "to a nonexistent premise\n") + self.app.show_error(errorstr) return # now we check to see if we *missed* any premises @@ -213,11 +224,12 @@ def verify_all(self): for key in premises_OR: if len(premises_OR[key]) > 0: end_early = True - print("ERROR: premise " + str(key) + " not represented") + errorstr += "ERROR: premise " + str(key) + " not represented\n" if len(concl_OR) > 0: end_early = True - print("ERROR: conclusion not represented") + errorstr += "ERROR: conclusion not represented\n" if end_early: + self.app.show_error(errorstr) return #print("debug: okay, great! all premises/conclusion represented!") @@ -237,8 +249,9 @@ def verify_all(self): #print(parent_lis) # should be two items here that will be converted into a list if len(parent_lis) != 2: - print("ERROR: clause '" + part_str + "' has " + - str(len(parent_lis)) + " parent(s), but expected 2") + errorstr += str("ERROR: clause '" + part_str + "' has " + + str(len(parent_lis)) + " parent(s), but expected 2\n") + self.app.show_error(errorstr) return # first, analyze the parents @@ -248,12 +261,14 @@ def verify_all(self): expected = list_as_str(simplify_onestep(pl1, pl2), "|") if expected is not None: if crop_str != expected: - print("ERROR: clause '" + part_str + "' is not a correct " + - "derivation from its parents") + errorstr += str("ERROR: clause '" + part_str + "' is not a correct " + + "derivation from its parents\n") + self.app.show_error(errorstr) return else: - print("ERROR: clause '" + part_str + "' is not within one " + - "derivation step from its parents") + errorstr += str("ERROR: clause '" + part_str + "' is not within one " + + "derivation step from its parents\n") + self.app.show_error(errorstr) return #if lower_lvl[key].child is not None: @@ -269,25 +284,28 @@ def verify_all(self): # then this is the final step! num_final_steps += 1 if num_final_steps != 1: - print("ERROR: there are at least " + str(num_final_steps) + errorstr += str("ERROR: there are at least " + str(num_final_steps) + " 'final steps' (no child clauses) in the " - + "derivation") + + "derivation\n") + self.app.show_error(errorstr) return # now we harken back to premises_check to see what we expect if premises_check: if crop_str != "": - print("ERROR: the premises and conclusion are valid, " + errorstr += str("ERROR: the premises and conclusion are valid, " + "but the derivation does not completely " - + "resolve") + + "resolve\n") + self.app.show_error(errorstr) return else: if crop_str == "": - print("ERROR: the premises and conclusion are invalid, " - + "but the derivation resolves completely") + errorstr += str("ERROR: the premises and conclusion are invalid, " + + "but the derivation resolves completely\n") + self.app.show_error(errorstr) return # if we have made it this far, we are actually done. - print("Successful resolution!") + self.app.success("Successful resolution!") return