From 4cd211ee9006b1fe7a83c0c9671b8cc55f9e8b62 Mon Sep 17 00:00:00 2001
From: Mroik <mroik@delayed.space>
Date: Wed, 24 Jul 2024 02:22:03 +0200
Subject: [PATCH] Make parsing fail on non-empty queue

---
 src/app.rs | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

diff --git a/src/app.rs b/src/app.rs
index 7064025..8cecd32 100644
--- a/src/app.rs
+++ b/src/app.rs
@@ -48,9 +48,7 @@ impl App {
             | State::OrState(OrState::EliminateGetAssumption) => {
                 ("And expression to eliminate", true)
             }
-            State::AndState(AndState::EliminateGetProposition(_)) => {
-                ("Resulting expression", true)
-            }
+            State::AndState(AndState::EliminateGetProposition(_)) => ("Resulting expression", true),
             State::OrState(OrState::EliminateGetLeftSubproof(_))
             | State::OrState(OrState::EliminateGetRightSubproof(_, _))
             | State::ImpliesState(ImpliesState::Introduce)
@@ -319,6 +317,9 @@ impl App {
                     parser::Result::Failure => app_context
                         .info_buffer
                         .push_str("The input expression is not valid"),
+                    parser::Result::Success(_, rest) if rest.trim() != "" => app_context
+                        .info_buffer
+                        .push_str("The input expression is not valid"),
                     parser::Result::Success(ris, _) => {
                         if !app_context.model.introduce_or(ass, &ris) {
                             app_context.info_buffer.push_str(
@@ -436,6 +437,9 @@ impl App {
                     parser::Result::Failure => app_context
                         .info_buffer
                         .push_str("Expression entered is invalid"),
+                    parser::Result::Success(_, rest) if rest.trim() != "" => app_context
+                        .info_buffer
+                        .push_str("Expression entered is invalid"),
                     parser::Result::Success(r, _) => {
                         if !app_context.model.eliminate_and(assum, &r) {
                             app_context
@@ -507,6 +511,9 @@ impl App {
                     parser::Result::Failure => app_context
                         .info_buffer
                         .push_str("Expression entered is invalid"),
+                    parser::Result::Success(_, rest) if rest.trim() != "" => app_context
+                        .info_buffer
+                        .push_str("Expression entered is invalid"),
                     parser::Result::Success(ded, _) => {
                         if !app_context.model.eliminate_absurdum(assum, &ded) {
                             app_context
@@ -565,6 +572,9 @@ impl App {
                 parser::Result::Failure => app_context
                     .info_buffer
                     .push_str("Expression entered is invalid"),
+                parser::Result::Success(_, rest) if rest.trim() != "" => app_context
+                    .info_buffer
+                    .push_str("Expression entered is invalid"),
                 parser::Result::Success(expr, _) => {
                     app_context.model.add_subproof(&expr);
                     app_context.state = State::Noraml;
@@ -582,6 +592,9 @@ impl App {
                 parser::Result::Failure => app_context
                     .info_buffer
                     .push_str("Expression entered is invalid"),
+                parser::Result::Success(_, rest) if rest.trim() != "" => app_context
+                    .info_buffer
+                    .push_str("Expression entered is invalid"),
                 parser::Result::Success(expr, _) => {
                     if !app_context.model.add_assumption(&expr) {
                         app_context