Add current level indicator

Mroik · May 9, 2024 · 23b05c6 · 23b05c6
1 parent e0c5148
commit 23b05c6
Show file tree

Hide file tree

Showing 2 changed files with 31 additions and 8 deletions.
diff --git a/src/app.rs b/src/app.rs
@@ -100,7 +100,7 @@ impl App {
                     State::NotState(_) => self.listen_not(&key.code),
                     State::ImpliesState(_) => self.listen_implies(&key.code),
                     State::IffState(_) => self.listen_iff(&key.code),
-                    _ => todo!(),
+                    _ => unreachable!(),
                 }
             }
 
@@ -585,7 +585,12 @@ impl App {
                     .info_buffer
                     .push_str("Expression entered is invalid"),
                 parser::Result::Success(expr, _) => {
-                    app_context.model.add_assumption(&expr);
+                    if !app_context.model.add_assumption(&expr) {
+                        app_context
+                            .info_buffer
+                            .push_str("Delete all deductions before adding assumptions");
+                        app_context.warning = true;
+                    }
                     app_context.state = State::Noraml;
                     app_context.reset_expression_box();
                 }

diff --git a/src/fitch.rs b/src/fitch.rs
@@ -96,11 +96,16 @@ impl Display for Fitch {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let mut res = String::new();
         let mut temp = self.statements.len() as i32 - 1;
+        if temp == 0 {
+            temp = 1;
+        }
+
         let mut max = 0;
         while temp > 0 {
             temp /= 10;
             max += 1;
         }
+
         self.statements
             .iter()
             .enumerate()
@@ -138,6 +143,16 @@ impl Display for Fitch {
                 res.push_str(expression.unwrap().to_string().as_str());
                 res.push('\n');
             });
+
+        for _ in 0..max + 4 {
+            res.push(' ');
+        }
+
+        for _ in 0..self.current_level {
+            res.push_str("    ");
+        }
+
+        res.push_str("^\n");
         write!(f, "{}", res)
     }
 }
@@ -151,12 +166,15 @@ impl Fitch {
         }
     }
 
-    pub fn add_assumption(&mut self, prop: &Rc<Proposition>) {
-        self.statements.insert(
-            self.start_of_deductions,
-            (0, FitchComponent::Deduction(prop.clone())),
-        );
+    pub fn add_assumption(&mut self, prop: &Rc<Proposition>) -> bool {
+        if self.statements.len() > self.start_of_deductions {
+            return false;
+        }
+
+        self.statements
+            .push((0, FitchComponent::Deduction(prop.clone())));
         self.start_of_deductions += 1;
+        true
     }
 
     pub fn add_subproof(&mut self, prop: &Rc<Proposition>) {
@@ -178,7 +196,7 @@ impl Fitch {
             self.start_of_deductions = self.statements.len();
         }
         match self.statements.last() {
-            None => (),
+            None => self.current_level = 0,
             Some((l, _)) => self.current_level = *l,
         }
     }