Hide turnstile when not needed

Nadrieril · Jan 2, 2025 · 40d07eb · 40d07eb
1 parent 2cd19c9
commit 40d07eb
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 1 deletion.
diff --git a/src/ast/printer.rs b/src/ast/printer.rs
@@ -221,7 +221,12 @@ impl<'a> TypingPredicate<'a> {
                     .to_display_tree(a)
                     .sep_then(a, ": ", ty);
 
-                pre_turnstile.sep_then(a, " ⊢ ", post_turnstile)
+                let parts: &[_] = if pre_turnstile.is_empty() {
+                    &[post_turnstile]
+                } else {
+                    &[pre_turnstile, post_turnstile]
+                };
+                DisplayTree::sep_by(a, " ⊢ ", parts)
             }
         }
     }

diff --git a/src/ast/printer/display_tree.rs b/src/ast/printer/display_tree.rs
@@ -77,6 +77,13 @@ fn strip_markup(s: &str) -> String {
 }
 
 impl<'a> DisplayTree<'a> {
+    pub fn is_empty(&self) -> bool {
+        match self.kind {
+            Leaf(s) => s.is_empty(),
+            Separated { children, .. } => children.is_empty(),
+        }
+    }
+
     pub fn len_ignoring_markup(&self) -> usize {
         match self.kind {
             Leaf(s) => len_ignoring_markup(s),