From 17ac305bf95b7aabe2c8bf0106ce32e1988d8802 Mon Sep 17 00:00:00 2001
From: fallensky2077 <mercur1al@outlook.com>
Date: Fri, 19 Dec 2025 14:39:30 +0000
Subject: [PATCH 1/7] try to add proof tree

---
 TeXmacs/progs/generic/generic-edit.scm     | 324 +++++++++++++++++++++
 TeXmacs/progs/math/math-drd.scm            |   5 +-
 TeXmacs/progs/math/math-menu.scm           |  51 +++-
 TeXmacs/progs/math/math-sem-edit.scm       |   1 +
 TeXmacs/progs/utils/library/cpp-wrap.scm   |   1 +
 moebius/moebius/drd/drd_std.cpp            |   5 +
 moebius/moebius/tree_label.hpp             |   3 +
 src/Edit/Interface/edit_footer.cpp         |   8 +
 src/Edit/Modify/edit_delete.cpp            |   3 +
 src/Edit/Modify/edit_math.cpp              |  16 +-
 src/Edit/Modify/edit_math.hpp              |   1 +
 src/Edit/editor.hpp                        |   1 +
 src/Scheme/Glue/build-glue-editor.scm      |   1 +
 src/Scheme/Glue/glue_editor.lua            |   7 +-
 src/Typeset/Boxes/Composite/math_boxes.cpp | 165 +++++++++++
 src/Typeset/Boxes/construct.hpp            |   2 +
 src/Typeset/Concat/concat_math.cpp         |  17 ++
 src/Typeset/Concat/concater.cpp            |   9 +
 src/Typeset/Concat/concater.hpp            |   2 +
 19 files changed, 618 insertions(+), 4 deletions(-)

diff --git a/TeXmacs/progs/generic/generic-edit.scm b/TeXmacs/progs/generic/generic-edit.scm
index 37a716485c..a7d0a091ef 100644
--- a/TeXmacs/progs/generic/generic-edit.scm
+++ b/TeXmacs/progs/generic/generic-edit.scm
@@ -338,6 +338,14 @@
   (or (tree-in? t '(tree))
       (table-markup-context? t)))
 
+(tm-define (structured-vertical? t)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  #t)
+
+(tm-define (structured-horizontal? t)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  #t)
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Focus predicates
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -767,6 +775,322 @@
   (:require (tree-is? t 'tree))
   (go-to-repeat (if downwards? structured-down structured-up)))
 
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Proof tree editing
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(tm-define (proof-tree-tag? t)
+  (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+
+(define (proof-tree-labeled? t)
+  (tree-in? t '(proof-tree* proof-tree**)))
+
+;; Predicate: are we inside a proof-tree?
+(define (inside-proof-tree?)
+  (and (tree-innermost '(proof-tree proof-tree* proof-tree**)) #t))
+
+(define (proof-tree-premise-start t)
+  ;; Return the index of the first premise
+  (if (proof-tree-labeled? t) 2 1))
+
+(define (proof-tree-conclusion-idx t)
+  ;; Return the index of the conclusion
+  (if (proof-tree-labeled? t) 1 0))
+
+;; Find the proof-tree when cursor might be in a child
+(define (proof-tree-active t)
+  (with i (tree-down-index t)
+    (if (and (proof-tree-tag? t)
+             (or (not (proof-tree-labeled? t))
+                 (> i 0)))
+        t
+        (if (and (tree-up t) (proof-tree-tag? (tree-up t)))
+            (tree-up t)
+            t))))
+
+;; Override variant-set for proof-tree to handle structure changes
+(tm-define (variant-set t new-tag)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  (with-focus-after t
+    (let* ((old-lab (tree-label t))
+           (old-labeled? (in? old-lab '(proof-tree* proof-tree**)))
+           (new-labeled? (in? new-tag '(proof-tree* proof-tree**)))
+           (idx (or (tree-down-index t) 0)))
+      (cond
+        ;; Adding label: insert empty label at position 0
+        ((and (not old-labeled?) new-labeled?)
+         (tree-insert! t 0 '(""))
+         (tree-assign-node! t new-tag))
+        ;; Removing label: remove label at position 0
+        ((and old-labeled? (not new-labeled?))
+         (tree-remove! t 0 1)
+         (tree-assign-node! t new-tag))
+        ;; Just changing between proof-tree* and proof-tree**, or no change
+        (else
+         (tree-assign-node! t new-tag))))))
+
+;; Define variants for proof-tree
+(tm-define (focus-variants-of t)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  '(proof-tree proof-tree* proof-tree**))
+
+;; Cursor navigation for proof-tree:
+;; - In conclusion: up → first premise, left/right → do nothing (stay)
+;; - In premise: down → conclusion
+;; - In last premise: right → exit proof-tree
+;; - In non-last premise: right → next premise
+;; - In first premise: left → exit backward
+;; - In non-first premise: left → previous premise
+
+;; Helper to get cursor position within proof-tree
+(define (proof-tree-cursor-child-index pt)
+  "Get the index of the child containing the cursor within proof-tree pt"
+  (let* ((p (tree->path pt))
+         (c (cursor-path))
+         (plen (length p)))
+    (if (and (>= (length c) (+ plen 1))
+             (== (sublist c 0 plen) p))
+        (list-ref c plen)
+        #f)))
+
+;; Structured horizontal navigation for proof-tree
+;; Only moves between premises, does not jump to/from conclusion
+(define (proof-tree-navigate-horizontal pt forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt))
+         (n (tree-arity pt)))
+    (when (and i (>= i prem-start))  ;; Only act when in premises
+      (cond
+        ;; Moving right from last premise: exit proof-tree
+        ((and forwards? (== i (- n 1)))
+         (tree-go-to pt :end))
+        ;; Moving right to next premise
+        ((and forwards? (< i (- n 1)))
+         (tree-go-to pt (+ i 1) :start))
+        ;; Moving left from first premise: do nothing (stay in first premise)
+        ((and (not forwards?) (== i prem-start))
+         (noop))
+        ;; Moving left to previous premise
+        ((and (not forwards?) (> i prem-start))
+         (tree-go-to pt (- i 1) :end))))))
+
+(define (proof-tree-navigate-vertical pt to-premises?)
+  ;; Visual layout: premises at TOP, conclusion at BOTTOM
+  ;; Tree structure: (proof-tree conclusion premise1 premise2 ...)
+  ;; to-premises? = #t means go to premises (visual UP)
+  ;; to-premises? = #f means go to conclusion (visual DOWN)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (conc-idx (proof-tree-conclusion-idx pt))
+         (i (proof-tree-cursor-child-index pt)))
+    (when i
+      (cond
+        ;; In conclusion, want to go to premises (UP key)
+        ((and to-premises? (== i conc-idx))
+         (tree-go-to pt prem-start :start))
+        ;; In premise, want to go to conclusion (DOWN key)
+        ((and (not to-premises?) (>= i prem-start))
+         (tree-go-to pt conc-idx :start))
+        ;; In label, want to go to premises (UP key)
+        ((and to-premises? (proof-tree-labeled? pt) (== i 0))
+         (tree-go-to pt prem-start :start))
+        ;; In label, want to go to conclusion (DOWN key)
+        ((and (not to-premises?) (proof-tree-labeled? pt) (== i 0))
+         (tree-go-to pt conc-idx :start))))))
+
+;; Override kbd-left for proof-tree
+;; Only intercept when crossing field boundary within proof-tree
+(tm-define (kbd-left)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (let* ((old-idx (proof-tree-cursor-child-index pt))
+           (prem-start (proof-tree-premise-start pt))
+           (conc-idx (proof-tree-conclusion-idx pt))
+           (old-path (cursor-path)))
+      ;; Try default movement
+      (go-left)
+      ;; Check where we ended up
+      (let ((new-idx (proof-tree-cursor-child-index pt)))
+        (cond
+          ;; Stayed in same field - keep the movement
+          ((and old-idx new-idx (== old-idx new-idx))
+           (noop))
+          ;; Left proof-tree entirely - that's fine, keep it
+          ((not new-idx)
+           (noop))
+          ;; Crossed from conclusion to a premise - not allowed, exit left instead
+          ;; Must restore cursor first to avoid double-movement
+          ((and old-idx (== old-idx conc-idx) new-idx (>= new-idx prem-start))
+           (go-to old-path)
+           (tree-go-to pt :start))
+          ;; Crossed from first premise to conclusion - not allowed, exit left instead
+          ;; Must restore cursor first to avoid double-movement
+          ((and old-idx (== old-idx prem-start) new-idx (== new-idx conc-idx))
+           (go-to old-path)
+           (tree-go-to pt :start))
+          ;; Crossed from one premise to another premise - that's fine for left movement
+          ;; (moving left from premise N should go to premise N-1)
+          ((and old-idx (> old-idx prem-start) new-idx (>= new-idx prem-start) (< new-idx old-idx))
+           (noop))  ;; Keep the movement
+          ;; Crossed from premise to conclusion - not allowed, go to previous premise instead
+          ;; Must restore cursor first to avoid double-movement
+          ((and old-idx (> old-idx prem-start) new-idx (== new-idx conc-idx))
+           (go-to old-path)
+           (tree-go-to pt (- old-idx 1) :end))
+          ;; Any other unexpected crossing - keep the movement
+          (else (noop)))))))
+
+;; Override kbd-right for proof-tree
+;; Only intercept when crossing field boundary within proof-tree
+(tm-define (kbd-right)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (let* ((old-idx (proof-tree-cursor-child-index pt))
+           (prem-start (proof-tree-premise-start pt))
+           (conc-idx (proof-tree-conclusion-idx pt))
+           (n (tree-arity pt))
+           (old-path (cursor-path)))
+      ;; Try default movement
+      (go-right)
+      ;; Check where we ended up
+      (let ((new-idx (proof-tree-cursor-child-index pt)))
+        (cond
+          ;; Stayed in same field - keep the movement
+          ((and old-idx new-idx (== old-idx new-idx))
+           (noop))
+          ;; Left proof-tree entirely - that's fine, keep it
+          ((not new-idx)
+           (noop))
+          ;; Crossed from conclusion to a premise - not allowed, exit right instead
+          ;; Must restore cursor first to avoid double-movement
+          ((and old-idx (== old-idx conc-idx) new-idx (>= new-idx prem-start))
+           (go-to old-path)
+           (tree-go-to pt :end))
+          ;; Crossed from last premise to conclusion - not allowed, exit right instead
+          ;; Must restore cursor first to avoid double-movement
+          ((and old-idx (== old-idx (- n 1)) new-idx (== new-idx conc-idx))
+           (go-to old-path)
+           (tree-go-to pt :end))
+          ;; Crossed from one premise to another premise - that's fine for right movement
+          ;; (moving right from premise N should go to premise N+1)
+          ((and old-idx (>= old-idx prem-start) (< old-idx (- n 1)) new-idx (> new-idx old-idx) (>= new-idx prem-start))
+           (noop))  ;; Keep the movement
+          ;; Crossed from premise to conclusion - not allowed, go to next premise instead
+          ;; Must restore cursor first to avoid double-movement
+          ((and old-idx (>= old-idx prem-start) (< old-idx (- n 1)) new-idx (== new-idx conc-idx))
+           (go-to old-path)
+           (tree-go-to pt (+ old-idx 1) :start))
+          ;; Any other unexpected crossing - keep the movement
+          (else (noop)))))))
+
+(tm-define (kbd-up)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    ;; UP key = go to premises (which are at top visually)
+    (proof-tree-navigate-vertical pt #t)))
+
+(tm-define (kbd-down)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    ;; DOWN key = go to conclusion (which is at bottom visually)
+    (proof-tree-navigate-vertical pt #f)))
+
+;; Override structured-left/right/up/down to find proof-tree ancestor
+(tm-define (structured-left)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-navigate-horizontal pt #f)))
+
+(tm-define (structured-right)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-navigate-horizontal pt #t)))
+
+(tm-define (structured-up)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    ;; UP visually = go to premises (which are at top)
+    (proof-tree-navigate-vertical pt #t)))
+
+(tm-define (structured-down)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    ;; DOWN visually = go to conclusion (which is at bottom)
+    (proof-tree-navigate-vertical pt #f)))
+
+;; Insert/remove helpers for proof-tree
+(define (proof-tree-insert-horizontal pt forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt)))
+    ;; Only insert when in premises area
+    (when (and i (>= i prem-start))
+      (with pos (if forwards? (+ i 1) i)
+        (tree-insert! pt pos '(""))
+        (tree-go-to pt pos 0)))))
+
+(define (proof-tree-remove-horizontal pt forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt))
+         (n (tree-arity pt)))
+    ;; Only remove when in premises area and more than one premise
+    (when (and i (>= i prem-start) (> n (+ prem-start 1)))
+      (cond
+        (forwards?
+         (tree-remove! pt i 1)
+         (if (>= i (tree-arity pt))
+             (tree-go-to pt (- i 1) :end)
+             (tree-go-to pt i :start)))
+        ((> i prem-start)
+         (tree-remove! pt i 1)
+         (tree-go-to pt (- i 1) :end))))))
+
+(define (proof-tree-insert-vertical pt downwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (i (proof-tree-cursor-child-index pt)))
+    ;; Insert sub-proof: wrap current premise in a new proof-tree
+    (when (and i (>= i prem-start))
+      (if downwards?
+          ;; Insert down: add empty conclusion below, current stays as premise
+          ;; This creates a sub-tree where current is premise, "" is conclusion
+          (begin
+            (tree-set! pt i `(proof-tree "" ,(tree-ref pt i)))
+            (tree-go-to pt i 0 0))
+          ;; Insert up: wrap current as conclusion of new sub-tree with empty premise above
+          ;; This creates a sub-tree where current becomes conclusion, "" is new premise
+          (begin
+            (tree-set! pt i `(proof-tree ,(tree-ref pt i) ""))
+            (tree-go-to pt i 1 0))))))
+
+;; Override structured-insert/remove for proof-tree
+(tm-define (structured-insert-left)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-insert-horizontal pt #f)))
+
+(tm-define (structured-insert-right)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-insert-horizontal pt #t)))
+
+(tm-define (structured-remove-left)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-remove-horizontal pt #f)))
+
+(tm-define (structured-remove-right)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-remove-horizontal pt #t)))
+
+(tm-define (structured-insert-up)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-insert-vertical pt #f)))
+
+(tm-define (structured-insert-down)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+    (proof-tree-insert-vertical pt #t)))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Extra editing functions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/TeXmacs/progs/math/math-drd.scm b/TeXmacs/progs/math/math-drd.scm
index 625ba9388e..bdd61618b5 100644
--- a/TeXmacs/progs/math/math-drd.scm
+++ b/TeXmacs/progs/math/math-drd.scm
@@ -16,7 +16,10 @@
 
 (define-group variant-tag
   (fraction-tag) (vertical-script-tag)
-  (textual-operator-tag))
+  (textual-operator-tag) (proof-tree-tag))
+
+(define-group proof-tree-tag
+  proof-tree proof-tree* proof-tree**)
 
 (define-group fraction-tag
   frac tfrac dfrac frac* cfrac)
diff --git a/TeXmacs/progs/math/math-menu.scm b/TeXmacs/progs/math/math-menu.scm
index 6f65460d09..a8584d45fe 100644
--- a/TeXmacs/progs/math/math-menu.scm
+++ b/TeXmacs/progs/math/math-menu.scm
@@ -1065,7 +1065,12 @@
   ("Square root" (make-sqrt))
   ("N-th root" (make-var-sqrt))
   ("Negation" (make-neg))
-  ("Tree" (make-tree))
+  (-> "Tree"
+      ("Tree" (make-tree))
+      ---
+      ("Proof tree" (make-proof-tree))
+      ("Proof tree (right label)" (make 'proof-tree*))
+      ("Proof tree (left label)" (make 'proof-tree**)))
   ---
   (-> "Script"
       ("Left subscript" (make-script #f #f))
@@ -1470,3 +1475,47 @@
   ;;((balloon (icon "tm_reset.xpm") "Reset to default bracket size")
   ;; (geometry-reset))
   )
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Proof tree focus menus
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(tm-define (focus-can-insert-remove? t)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  #t)
+
+(tm-define (focus-tag-name l)
+  (:require (in? l '(proof-tree proof-tree* proof-tree**)))
+  (cond ((== l 'proof-tree) "No label")
+        ((== l 'proof-tree*) "Right label")
+        ((== l 'proof-tree**) "Left label")))
+
+;; Custom variant menu for proof-tree
+;; Note: t is already the proof-tree when :require matches
+(tm-menu (focus-variant-menu t)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  ((check "No label" "v" (tree-is? t 'proof-tree))
+   (variant-set t 'proof-tree))
+  ((check "Right label" "v" (tree-is? t 'proof-tree*))
+   (variant-set t 'proof-tree*))
+  ((check "Left label" "v" (tree-is? t 'proof-tree**))
+   (variant-set t 'proof-tree**)))
+
+(tm-menu (focus-insert-menu t)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  ("Insert premise before" (structured-insert-left))
+  ("Insert premise after" (structured-insert-right))
+  ---
+  ("Insert sub-proof above" (structured-insert-up))
+  ("Remove premise" (structured-remove-right)))
+
+(tm-menu (focus-insert-icons t)
+  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  ((balloon (icon "tm_insert_left.xpm") "Insert premise before")
+   (structured-insert-left))
+  ((balloon (icon "tm_insert_right.xpm") "Insert premise after")
+   (structured-insert-right))
+  ((balloon (icon "tm_insert_up.xpm") "Insert sub-proof above")
+   (structured-insert-up))
+  ((balloon (icon "tm_delete_right.xpm") "Remove premise")
+   (structured-remove-right)))
diff --git a/TeXmacs/progs/math/math-sem-edit.scm b/TeXmacs/progs/math/math-sem-edit.scm
index 8b6f7c58a4..ad5ba2582f 100644
--- a/TeXmacs/progs/math/math-sem-edit.scm
+++ b/TeXmacs/progs/math/math-sem-edit.scm
@@ -434,6 +434,7 @@
 (wrap-inserter make-wide-under)
 (wrap-inserter make-neg)
 (wrap-inserter make-tree)
+(wrap-inserter make-proof-tree)
 (wrap-inserter make-long-arrow)
 (wrap-inserter make-long-arrow*)
 
diff --git a/TeXmacs/progs/utils/library/cpp-wrap.scm b/TeXmacs/progs/utils/library/cpp-wrap.scm
index 41082e0bc6..3c59f4433e 100644
--- a/TeXmacs/progs/utils/library/cpp-wrap.scm
+++ b/TeXmacs/progs/utils/library/cpp-wrap.scm
@@ -108,6 +108,7 @@
 (tm-define (make-wide-under s) (cpp-make-wide-under s))
 (tm-define (make-neg) (cpp-make-neg))
 (tm-define (make-tree) (cpp-make-tree))
+(tm-define (make-proof-tree) (cpp-make-proof-tree))
 
 (tm-define (clipboard-copy cb) (cpp-clipboard-copy cb))
 (tm-define (clipboard-cut cb) (cpp-clipboard-cut cb))
diff --git a/moebius/moebius/drd/drd_std.cpp b/moebius/moebius/drd/drd_std.cpp
index 3d6a740666..f441e0c8f0 100644
--- a/moebius/moebius/drd/drd_std.cpp
+++ b/moebius/moebius/drd/drd_std.cpp
@@ -282,6 +282,11 @@ init_std_drd () {
             ->name (1, "accent"));
   init (NEG, "neg", fixed (1)->accessible (0)->name ("negation"));
   init (TREE, "tree", repeat (2, 1)->accessible (0));
+  init (PROOF_TREE, "proof-tree", repeat (2, 1)->accessible (0));
+  init (VAR_PROOF_TREE, "proof-tree*",
+        repeat (3, 1)->accessible (0)->name (0, "label"));
+  init (VAR_VAR_PROOF_TREE, "proof-tree**",
+        repeat (3, 1)->accessible (0)->name (0, "label"));
   init (SYNTAX, "syntax",
         fixed (1, 1, BIFORM)
             ->accessible (0)
diff --git a/moebius/moebius/tree_label.hpp b/moebius/moebius/tree_label.hpp
index 70dd417f27..a24ad3c195 100644
--- a/moebius/moebius/tree_label.hpp
+++ b/moebius/moebius/tree_label.hpp
@@ -107,6 +107,9 @@ enum tree_label : int {
   VAR_WIDE,
   NEG,
   TREE,
+  PROOF_TREE,
+  VAR_PROOF_TREE,    // proof-tree* (label on right)
+  VAR_VAR_PROOF_TREE, // proof-tree** (label on left)
   SYNTAX,
 
   // tabular material
diff --git a/src/Edit/Interface/edit_footer.cpp b/src/Edit/Interface/edit_footer.cpp
index 461d9e11e9..f6849a000c 100644
--- a/src/Edit/Interface/edit_footer.cpp
+++ b/src/Edit/Interface/edit_footer.cpp
@@ -363,6 +363,14 @@ edit_interface_rep::compute_compound_footer (tree t, path p) {
   case TREE:
     if (l == 0) return concat (up, "root ");
     else return concat (up, "branch(" * as_string (l) * ") ");
+  case PROOF_TREE:
+    if (l == 0) return concat (up, "conclusion ");
+    else return concat (up, "premise(" * as_string (l) * ") ");
+  case VAR_PROOF_TREE:
+  case VAR_VAR_PROOF_TREE:
+    if (l == 0) return concat (up, "label ");
+    else if (l == 1) return concat (up, "conclusion ");
+    else return concat (up, "premise(" * as_string (l - 1) * ") ");
   case TFORMAT:
     return up;
   case TABLE:
diff --git a/src/Edit/Modify/edit_delete.cpp b/src/Edit/Modify/edit_delete.cpp
index 90a0b133e4..4b56207c05 100644
--- a/src/Edit/Modify/edit_delete.cpp
+++ b/src/Edit/Modify/edit_delete.cpp
@@ -233,6 +233,9 @@ edit_text_rep::remove_text_sub (bool forward) {
       back_in_wide (u, p, forward);
       return;
     case TREE:
+    case PROOF_TREE:
+    case VAR_PROOF_TREE:
+    case VAR_VAR_PROOF_TREE:
       back_in_tree (u, p, forward);
       return;
     case TFORMAT:
diff --git a/src/Edit/Modify/edit_math.cpp b/src/Edit/Modify/edit_math.cpp
index 919c5efdc7..4663b8f7ec 100644
--- a/src/Edit/Modify/edit_math.cpp
+++ b/src/Edit/Modify/edit_math.cpp
@@ -331,6 +331,18 @@ edit_math_rep::make_tree () {
   }
 }
 
+void
+edit_math_rep::make_proof_tree () {
+  if (selection_active_small ())
+    insert_tree (tree (PROOF_TREE, selection_get_cut (), ""), path (1, 0));
+  else {
+    insert_tree (tree (PROOF_TREE, "", ""), path (0, 0));
+    set_message (concat (kbd_shortcut ("(structured-insert-right)"),
+                         ": insert a new premise"),
+                 "proof-tree");
+  }
+}
+
 void
 edit_math_rep::back_in_tree (tree t, path p, bool forward) {
   int i= last_item (p);
@@ -354,7 +366,9 @@ edit_math_rep::back_in_tree (tree t, path p, bool forward) {
     else go_to_start (path_up (p) * (i + 1));
   }
   else {
-    if (t == tree (TREE, "", "")) {
+    if (t == tree (TREE, "", "") || t == tree (PROOF_TREE, "", "") ||
+        t == tree (VAR_PROOF_TREE, "", "", "") ||
+        t == tree (VAR_VAR_PROOF_TREE, "", "", "")) {
       p= path_up (p);
       assign (p, "");
       correct (path_up (p));
diff --git a/src/Edit/Modify/edit_math.hpp b/src/Edit/Modify/edit_math.hpp
index 6891572a9d..01f98562e4 100644
--- a/src/Edit/Modify/edit_math.hpp
+++ b/src/Edit/Modify/edit_math.hpp
@@ -31,6 +31,7 @@ class edit_math_rep : virtual public editor_rep {
   void make_wide_under (string wide);
   void make_neg ();
   void make_tree ();
+  void make_proof_tree ();
   void back_around (tree t, path p, bool forward);
   void back_prime (tree t, path p, bool forward);
   void back_in_around (tree t, path p, bool forward);
diff --git a/src/Edit/editor.hpp b/src/Edit/editor.hpp
index 1e44f9cef9..53f5dc04f2 100644
--- a/src/Edit/editor.hpp
+++ b/src/Edit/editor.hpp
@@ -417,6 +417,7 @@ class editor_rep : public simple_widget_rep {
   virtual void make_wide_under (string wide)     = 0;
   virtual void make_neg ()                       = 0;
   virtual void make_tree ()                      = 0;
+  virtual void make_proof_tree ()                = 0;
 
   /* public routines from edit_table */
   virtual void       make_table (int nr_rows= 1, int nr_cols= 1)         = 0;
diff --git a/src/Scheme/Glue/build-glue-editor.scm b/src/Scheme/Glue/build-glue-editor.scm
index 21d1b40a3c..471f1d22ac 100644
--- a/src/Scheme/Glue/build-glue-editor.scm
+++ b/src/Scheme/Glue/build-glue-editor.scm
@@ -142,6 +142,7 @@
   (cpp-make-var-sqrt make_var_sqrt (void))
   (cpp-make-neg make_neg (void))
   (cpp-make-tree make_tree (void))
+  (cpp-make-proof-tree make_proof_tree (void))
 
   ;; modify tables
   (make-subtable make_subtable (void))
diff --git a/src/Scheme/Glue/glue_editor.lua b/src/Scheme/Glue/glue_editor.lua
index 143d8b1c86..8e6a804a8f 100644
--- a/src/Scheme/Glue/glue_editor.lua
+++ b/src/Scheme/Glue/glue_editor.lua
@@ -852,7 +852,12 @@ function main()
                 cpp_name = "make_tree",
                 ret_type = "void"
             },
-            
+            {
+                scm_name = "cpp-make-proof-tree",
+                cpp_name = "make_proof_tree",
+                ret_type = "void"
+            },
+
             -- modify tables
             {
                 scm_name = "make-subtable",
diff --git a/src/Typeset/Boxes/Composite/math_boxes.cpp b/src/Typeset/Boxes/Composite/math_boxes.cpp
index c536165cb9..69a026b280 100644
--- a/src/Typeset/Boxes/Composite/math_boxes.cpp
+++ b/src/Typeset/Boxes/Composite/math_boxes.cpp
@@ -754,6 +754,171 @@ tree_box (path ip, array<box> bs, font fn, pencil pen) {
   return tm_new<tree_box_rep> (ip, bs, fn, pen);
 }
 
+/******************************************************************************
+ * Proof tree boxes (natural deduction trees)
+ ******************************************************************************/
+
+struct proof_tree_box_rep : public composite_box_rep {
+  font   fn;
+  pencil pen;
+  SI     border;
+  bool   has_label;
+  bool   label_left;
+  proof_tree_box_rep (path ip, array<box> bs, font fn, pencil pen,
+                      bool has_label, bool label_left);
+  operator tree () { return "proof-tree box"; }
+  box adjust_kerning (int mode, double factor);
+  box expand_glyphs (int mode, double factor);
+  int find_child (SI x, SI y, SI delta, bool force);
+};
+
+proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
+                                        pencil pen2, bool has_label2,
+                                        bool label_left2)
+    : composite_box_rep (ip), fn (fn2), pen (pen2), has_label (has_label2),
+      label_left (label_left2) {
+  // For labeled: bs[0] is label, bs[1] is conclusion, bs[2..n-1] are premises
+  // For unlabeled: bs[0] is conclusion, bs[1..n-1] are premises
+  SI sep     = fn->sep;
+  SI hsep    = 2 * fn->spc->def;
+  SI vsep    = 2 * fn->spc->def;
+  SI line_w  = fn->wline;
+  SI label_sp= fn->spc->def; // space between line and label
+
+  int i, n= N (bs);
+  int conc_idx   = has_label ? 1 : 0;
+  int prem_start = has_label ? 2 : 1;
+
+  // Calculate premises total width and baseline alignment info
+  SI prem_w  = 0;
+  SI max_y2  = MIN_SI; // max ascent (height above baseline)
+  SI min_y1  = MAX_SI; // min descent (depth below baseline, negative value)
+  for (i= prem_start; i < n; i++)
+    prem_w+= bs[i]->w ();
+  for (i= prem_start; i < n; i++) {
+    max_y2= max (max_y2, bs[i]->y2);
+    min_y1= min (min_y1, bs[i]->y1);
+  }
+  if (n > prem_start) prem_w+= (n - prem_start - 1) * hsep;
+
+  // Calculate conclusion dimensions
+  SI conc_w= bs[conc_idx]->w ();
+
+  // Calculate label width if present
+  SI label_w= has_label ? bs[0]->w () : 0;
+
+  // Calculate total width for the inference line
+  SI line_margin  = fn->spc->def;
+  SI line_w_total = max (prem_w, conc_w) + 2 * line_margin;
+  SI content_w    = max (line_w_total, max (prem_w, conc_w));
+  SI total_w      = content_w;
+
+  // Add space for label if present
+  if (has_label) total_w= content_w + label_sp + label_w;
+
+  // Calculate offset for content (to make room for label on left)
+  SI content_offset= 0;
+  if (has_label && label_left) content_offset= label_w + label_sp;
+
+  // Position premises at the top, centered within total_w (line + label)
+  // This ensures children's "line + label" center aligns with parent's center
+  // Use baseline alignment: all premises share the same baseline y-coordinate
+  SI prem_start_x = (total_w - prem_w) >> 1;
+  SI prem_baseline= max (bs[conc_idx]->y2, fn->y2) + sep + vsep - min_y1;
+
+  for (SI x= prem_start_x, i= prem_start; i < n; i++) {
+    SI x_i= x - bs[i]->x1;
+    SI y_i= prem_baseline; // Align at baseline (y=0 in box coords)
+    insert (bs[i], x_i, y_i);
+    x+= bs[i]->w () + hsep;
+  }
+
+  // Draw the horizontal inference line, centered within total_w
+  SI line_y = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
+  SI line_x1= (total_w - line_w_total) >> 1;
+  SI line_x2= line_x1 + line_w_total;
+  pencil tpen= pen->set_width (line_w);
+  insert (line_box (decorate_middle (ip), line_x1, 0, line_x2, 0, tpen), 0,
+          line_y);
+
+  // Position label if present (relative to the inference line)
+  if (has_label) {
+    SI label_x, label_y;
+    label_y= line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
+    if (label_left) {
+      // Left label: right edge at line_x1 - label_sp
+      label_x= line_x1 - label_sp - bs[0]->x2;
+    }
+    else {
+      // Right label: left edge at line_x2 + label_sp
+      label_x= line_x2 + label_sp - bs[0]->x1;
+    }
+    insert (bs[0], label_x, label_y);
+  }
+
+  // Position conclusion at the bottom, centered within total_w
+  insert (bs[conc_idx],
+          (total_w >> 1) - ((bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1),
+          0);
+
+  position ();
+  border= line_y;
+  finalize ();
+}
+
+box
+proof_tree_box_rep::adjust_kerning (int mode, double factor) {
+  (void) mode;
+  int        n   = N (bs);
+  int        skip= has_label ? 1 : 0; // skip line box
+  int        m   = n - skip;
+  array<box> adj (m);
+  for (int i= 0; i < m; i++)
+    adj[i]= bs[i]->adjust_kerning (0, factor);
+  return proof_tree_box (ip, adj, fn, pen, has_label, label_left);
+}
+
+box
+proof_tree_box_rep::expand_glyphs (int mode, double factor) {
+  (void) mode;
+  int        n   = N (bs);
+  int        skip= has_label ? 1 : 0;
+  int        m   = n - skip;
+  array<box> adj (m);
+  for (int i= 0; i < m; i++)
+    adj[i]= bs[i]->expand_glyphs (0, factor);
+  return proof_tree_box (ip, adj, fn, pen, has_label, label_left);
+}
+
+int
+proof_tree_box_rep::find_child (SI x, SI y, SI delta, bool force) {
+  if (outside (x, delta, x1, x2) && (is_accessible (ip) || force)) return -1;
+  int conc_idx= has_label ? 1 : 0;
+  int i       = conc_idx;
+  // Conclusion is below the border, premises above
+  if (y > border) {
+    int prem_start= has_label ? 2 : 1;
+    int j, d= MAX_SI;
+    for (j= prem_start; j < N (bs); j++)
+      if (distance (j, x, y, delta) < d)
+        if (bs[j]->accessible () || force) {
+          d= distance (j, x, y, delta);
+          i= j;
+        }
+  }
+  // Check if clicking on label
+  if (has_label && distance (0, x, y, delta) < distance (i, x, y, delta))
+    if (bs[0]->accessible () || force) i= 0;
+  if (bs[i]->decoration () && (!force)) return -1;
+  return i;
+}
+
+box
+proof_tree_box (path ip, array<box> bs, font fn, pencil pen, bool has_label,
+                bool label_left) {
+  return tm_new<proof_tree_box_rep> (ip, bs, fn, pen, has_label, label_left);
+}
+
 box
 wide_box (path ip, box ref, string s, font fn, pencil pen, bool wf, bool af) {
   return tm_new<wide_box_rep> (ip, ref, s, fn, pen, wf, af);
diff --git a/src/Typeset/Boxes/construct.hpp b/src/Typeset/Boxes/construct.hpp
index 28b665394d..92cb139f51 100644
--- a/src/Typeset/Boxes/construct.hpp
+++ b/src/Typeset/Boxes/construct.hpp
@@ -151,6 +151,8 @@ box frac_box (path ip, box b1, box b2, font fn, font sfn, pencil pen,
 box sqrt_box (path ip, box b1, box b2, box sqrtb, font fn, pencil pen);
 box neg_box (path ip, box b, font fn, pencil pen);
 box tree_box (path ip, array<box> bs, font fn, pencil pen);
+box proof_tree_box (path ip, array<box> bs, font fn, pencil pen,
+                    bool has_label= false, bool label_left= false);
 box wide_box (path ip, box ref, string s, font fn, pencil p, bool wf, bool af);
 box repeat_box (path ip, box ref, box repeat, SI xoff= 0, bool under= false);
 box limit_box (path ip, box ref, box lo, box hi, font fn, bool glued);
diff --git a/src/Typeset/Concat/concat_math.cpp b/src/Typeset/Concat/concat_math.cpp
index 48a24619c1..46bd9f9feb 100644
--- a/src/Typeset/Concat/concat_math.cpp
+++ b/src/Typeset/Concat/concat_math.cpp
@@ -619,6 +619,23 @@ concater_rep::typeset_tree (tree t, path ip) {
   print (tree_box (ip, bs, env->fn, env->pen));
 }
 
+void
+concater_rep::typeset_proof_tree (tree t, path ip, bool has_label,
+                                  bool label_left) {
+  int min_children= has_label ? 3 : 2;
+  if (N (t) < min_children) {
+    typeset_error (t, ip);
+    return;
+  }
+  int        i, n= N (t);
+  array<box> bs (n);
+  // For labeled: t[0] is label, t[1] is conclusion, t[2..n-1] are premises
+  // For unlabeled: t[0] is conclusion, t[1..n-1] are premises
+  for (i= 0; i < n; i++)
+    bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
+  print (proof_tree_box (ip, bs, env->fn, env->pen, has_label, label_left));
+}
+
 void
 concater_rep::typeset_table (tree t, path ip) {
   box b= typeset_as_table (env, t, ip);
diff --git a/src/Typeset/Concat/concater.cpp b/src/Typeset/Concat/concater.cpp
index bad56a8569..02fbf83599 100644
--- a/src/Typeset/Concat/concater.cpp
+++ b/src/Typeset/Concat/concater.cpp
@@ -440,6 +440,15 @@ concater_rep::typeset (tree t, path ip) {
   case TREE:
     typeset_tree (t, ip);
     break;
+  case PROOF_TREE:
+    typeset_proof_tree (t, ip);
+    break;
+  case VAR_PROOF_TREE:
+    typeset_proof_tree (t, ip, true, false);
+    break;
+  case VAR_VAR_PROOF_TREE:
+    typeset_proof_tree (t, ip, true, true);
+    break;
   case SYNTAX:
     typeset_syntax (t, ip);
     break;
diff --git a/src/Typeset/Concat/concater.hpp b/src/Typeset/Concat/concater.hpp
index 2c8a769169..818df16ea0 100644
--- a/src/Typeset/Concat/concater.hpp
+++ b/src/Typeset/Concat/concater.hpp
@@ -91,6 +91,8 @@ class concater_rep {
   void typeset_wide (tree t, path ip, bool above);
   void typeset_neg (tree t, path ip);
   void typeset_tree (tree t, path ip);
+  void typeset_proof_tree (tree t, path ip, bool has_label= false,
+                           bool label_left= false);
   void typeset_wide_table (tree t, path ip);
   void typeset_table (tree t, path ip);
   void print_semantic (box b, tree sem);

From 301074995b85a5cf82fd989a843f0ad793e7e12f Mon Sep 17 00:00:00 2001
From: fallensky2077 <mercur1al@outlook.com>
Date: Fri, 19 Dec 2025 19:15:14 +0000
Subject: [PATCH 2/7] fix math box

---
 src/Typeset/Boxes/Composite/math_boxes.cpp | 55 +++++++++++++---------
 1 file changed, 33 insertions(+), 22 deletions(-)

diff --git a/src/Typeset/Boxes/Composite/math_boxes.cpp b/src/Typeset/Boxes/Composite/math_boxes.cpp
index 69a026b280..97300e2eaf 100644
--- a/src/Typeset/Boxes/Composite/math_boxes.cpp
+++ b/src/Typeset/Boxes/Composite/math_boxes.cpp
@@ -807,21 +807,18 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   // Calculate label width if present
   SI label_w= has_label ? bs[0]->w () : 0;
 
-  // Calculate total width for the inference line
+  // Calculate inference line width
   SI line_margin  = fn->spc->def;
   SI line_w_total = max (prem_w, conc_w) + 2 * line_margin;
-  SI content_w    = max (line_w_total, max (prem_w, conc_w));
-  SI total_w      = content_w;
 
-  // Add space for label if present
-  if (has_label) total_w= content_w + label_sp + label_w;
+  // Calculate "line + label" unit width (treated as a whole)
+  SI line_label_w = line_w_total;
+  if (has_label) line_label_w = line_w_total + label_sp + label_w;
 
-  // Calculate offset for content (to make room for label on left)
-  SI content_offset= 0;
-  if (has_label && label_left) content_offset= label_w + label_sp;
+  // Total width is max of premises, conclusion, and "line + label" unit
+  SI total_w = max (line_label_w, max (prem_w, conc_w));
 
-  // Position premises at the top, centered within total_w (line + label)
-  // This ensures children's "line + label" center aligns with parent's center
+  // Position premises at the top, centered within total_w
   // Use baseline alignment: all premises share the same baseline y-coordinate
   SI prem_start_x = (total_w - prem_w) >> 1;
   SI prem_baseline= max (bs[conc_idx]->y2, fn->y2) + sep + vsep - min_y1;
@@ -833,32 +830,46 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
     x+= bs[i]->w () + hsep;
   }
 
-  // Draw the horizontal inference line, centered within total_w
+  // Draw the horizontal inference line
+  // "Line + label" unit is centered within total_w
+  SI line_label_start = (total_w - line_label_w) >> 1;
   SI line_y = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
-  SI line_x1= (total_w - line_w_total) >> 1;
-  SI line_x2= line_x1 + line_w_total;
-  pencil tpen= pen->set_width (line_w);
+  SI line_x1, line_x2;
+  if (has_label && label_left) {
+    // Left label: [label][space][line]
+    line_x1 = line_label_start + label_w + label_sp;
+    line_x2 = line_x1 + line_w_total;
+  }
+  else {
+    // No label or right label: [line][space][label]
+    line_x1 = line_label_start;
+    line_x2 = line_x1 + line_w_total;
+  }
+  pencil tpen = pen->set_width (line_w);
   insert (line_box (decorate_middle (ip), line_x1, 0, line_x2, 0, tpen), 0,
           line_y);
 
-  // Position label if present (relative to the inference line)
+  // Position label if present
   if (has_label) {
     SI label_x, label_y;
-    label_y= line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
+    // Label vertical center aligned with the line
+    label_y = line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
+
     if (label_left) {
-      // Left label: right edge at line_x1 - label_sp
-      label_x= line_x1 - label_sp - bs[0]->x2;
+      // Left label: starts at line_label_start
+      label_x = line_label_start - bs[0]->x1;
     }
     else {
-      // Right label: left edge at line_x2 + label_sp
-      label_x= line_x2 + label_sp - bs[0]->x1;
+      // Right label: starts after line + space
+      label_x = line_x2 + label_sp - bs[0]->x1;
     }
     insert (bs[0], label_x, label_y);
   }
 
-  // Position conclusion at the bottom, centered within total_w
+  // Position conclusion at the bottom, centered under the LINE only
+  SI line_center = (line_x1 + line_x2) >> 1;
   insert (bs[conc_idx],
-          (total_w >> 1) - ((bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1),
+          line_center - ((bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1),
           0);
 
   position ();

From 253e6489f13c7552c912485477e7c960c24a17ae Mon Sep 17 00:00:00 2001
From: fallensky2077 <mercur1al@outlook.com>
Date: Fri, 19 Dec 2025 23:25:52 +0000
Subject: [PATCH 3/7] fix navigation

---
 TeXmacs/progs/generic/generic-edit.scm     | 149 +++------------------
 src/Typeset/Boxes/Composite/math_boxes.cpp |  87 ++++++------
 2 files changed, 62 insertions(+), 174 deletions(-)

diff --git a/TeXmacs/progs/generic/generic-edit.scm b/TeXmacs/progs/generic/generic-edit.scm
index a7d0a091ef..4920aff136 100644
--- a/TeXmacs/progs/generic/generic-edit.scm
+++ b/TeXmacs/progs/generic/generic-edit.scm
@@ -797,16 +797,6 @@
   ;; Return the index of the conclusion
   (if (proof-tree-labeled? t) 1 0))
 
-;; Find the proof-tree when cursor might be in a child
-(define (proof-tree-active t)
-  (with i (tree-down-index t)
-    (if (and (proof-tree-tag? t)
-             (or (not (proof-tree-labeled? t))
-                 (> i 0)))
-        t
-        (if (and (tree-up t) (proof-tree-tag? (tree-up t)))
-            (tree-up t)
-            t))))
 
 ;; Override variant-set for proof-tree to handle structure changes
 (tm-define (variant-set t new-tag)
@@ -834,164 +824,59 @@
   (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
   '(proof-tree proof-tree* proof-tree**))
 
-;; Cursor navigation for proof-tree:
-;; - In conclusion: up → first premise, left/right → do nothing (stay)
-;; - In premise: down → conclusion
-;; - In last premise: right → exit proof-tree
-;; - In non-last premise: right → next premise
-;; - In first premise: left → exit backward
-;; - In non-first premise: left → previous premise
+;; Navigation for proof-tree:
+;; - kbd-left/kbd-right: use default behavior (works correctly now)
+;; - kbd-up/kbd-down: jump between conclusion and premises
+;; - structured-left/right: move between premises only
+;; - structured-up/down: same as kbd-up/down
 
 ;; Helper to get cursor position within proof-tree
 (define (proof-tree-cursor-child-index pt)
-  "Get the index of the child containing the cursor within proof-tree pt"
-  (let* ((p (tree->path pt))
-         (c (cursor-path))
-         (plen (length p)))
-    (if (and (>= (length c) (+ plen 1))
-             (== (sublist c 0 plen) p))
-        (list-ref c plen)
-        #f)))
-
-;; Structured horizontal navigation for proof-tree
-;; Only moves between premises, does not jump to/from conclusion
+  (tree-down-index pt))
+
+;; Structured horizontal navigation: only moves between premises
 (define (proof-tree-navigate-horizontal pt forwards?)
   (let* ((prem-start (proof-tree-premise-start pt))
          (i (proof-tree-cursor-child-index pt))
          (n (tree-arity pt)))
-    (when (and i (>= i prem-start))  ;; Only act when in premises
+    (when (and i (>= i prem-start))
       (cond
-        ;; Moving right from last premise: exit proof-tree
         ((and forwards? (== i (- n 1)))
          (tree-go-to pt :end))
-        ;; Moving right to next premise
         ((and forwards? (< i (- n 1)))
          (tree-go-to pt (+ i 1) :start))
-        ;; Moving left from first premise: do nothing (stay in first premise)
         ((and (not forwards?) (== i prem-start))
          (noop))
-        ;; Moving left to previous premise
         ((and (not forwards?) (> i prem-start))
          (tree-go-to pt (- i 1) :end))))))
 
+;; Simple vertical navigation: jump between conclusion and premises
 (define (proof-tree-navigate-vertical pt to-premises?)
-  ;; Visual layout: premises at TOP, conclusion at BOTTOM
-  ;; Tree structure: (proof-tree conclusion premise1 premise2 ...)
-  ;; to-premises? = #t means go to premises (visual UP)
-  ;; to-premises? = #f means go to conclusion (visual DOWN)
   (let* ((prem-start (proof-tree-premise-start pt))
          (conc-idx (proof-tree-conclusion-idx pt))
          (i (proof-tree-cursor-child-index pt)))
     (when i
       (cond
-        ;; In conclusion, want to go to premises (UP key)
+        ;; In conclusion, go UP to first premise
         ((and to-premises? (== i conc-idx))
          (tree-go-to pt prem-start :start))
-        ;; In premise, want to go to conclusion (DOWN key)
+        ;; In premise, go DOWN to conclusion
         ((and (not to-premises?) (>= i prem-start))
          (tree-go-to pt conc-idx :start))
-        ;; In label, want to go to premises (UP key)
-        ((and to-premises? (proof-tree-labeled? pt) (== i 0))
-         (tree-go-to pt prem-start :start))
-        ;; In label, want to go to conclusion (DOWN key)
-        ((and (not to-premises?) (proof-tree-labeled? pt) (== i 0))
-         (tree-go-to pt conc-idx :start))))))
-
-;; Override kbd-left for proof-tree
-;; Only intercept when crossing field boundary within proof-tree
-(tm-define (kbd-left)
-  (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (let* ((old-idx (proof-tree-cursor-child-index pt))
-           (prem-start (proof-tree-premise-start pt))
-           (conc-idx (proof-tree-conclusion-idx pt))
-           (old-path (cursor-path)))
-      ;; Try default movement
-      (go-left)
-      ;; Check where we ended up
-      (let ((new-idx (proof-tree-cursor-child-index pt)))
-        (cond
-          ;; Stayed in same field - keep the movement
-          ((and old-idx new-idx (== old-idx new-idx))
-           (noop))
-          ;; Left proof-tree entirely - that's fine, keep it
-          ((not new-idx)
-           (noop))
-          ;; Crossed from conclusion to a premise - not allowed, exit left instead
-          ;; Must restore cursor first to avoid double-movement
-          ((and old-idx (== old-idx conc-idx) new-idx (>= new-idx prem-start))
-           (go-to old-path)
-           (tree-go-to pt :start))
-          ;; Crossed from first premise to conclusion - not allowed, exit left instead
-          ;; Must restore cursor first to avoid double-movement
-          ((and old-idx (== old-idx prem-start) new-idx (== new-idx conc-idx))
-           (go-to old-path)
-           (tree-go-to pt :start))
-          ;; Crossed from one premise to another premise - that's fine for left movement
-          ;; (moving left from premise N should go to premise N-1)
-          ((and old-idx (> old-idx prem-start) new-idx (>= new-idx prem-start) (< new-idx old-idx))
-           (noop))  ;; Keep the movement
-          ;; Crossed from premise to conclusion - not allowed, go to previous premise instead
-          ;; Must restore cursor first to avoid double-movement
-          ((and old-idx (> old-idx prem-start) new-idx (== new-idx conc-idx))
-           (go-to old-path)
-           (tree-go-to pt (- old-idx 1) :end))
-          ;; Any other unexpected crossing - keep the movement
-          (else (noop)))))))
-
-;; Override kbd-right for proof-tree
-;; Only intercept when crossing field boundary within proof-tree
-(tm-define (kbd-right)
-  (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (let* ((old-idx (proof-tree-cursor-child-index pt))
-           (prem-start (proof-tree-premise-start pt))
-           (conc-idx (proof-tree-conclusion-idx pt))
-           (n (tree-arity pt))
-           (old-path (cursor-path)))
-      ;; Try default movement
-      (go-right)
-      ;; Check where we ended up
-      (let ((new-idx (proof-tree-cursor-child-index pt)))
-        (cond
-          ;; Stayed in same field - keep the movement
-          ((and old-idx new-idx (== old-idx new-idx))
-           (noop))
-          ;; Left proof-tree entirely - that's fine, keep it
-          ((not new-idx)
-           (noop))
-          ;; Crossed from conclusion to a premise - not allowed, exit right instead
-          ;; Must restore cursor first to avoid double-movement
-          ((and old-idx (== old-idx conc-idx) new-idx (>= new-idx prem-start))
-           (go-to old-path)
-           (tree-go-to pt :end))
-          ;; Crossed from last premise to conclusion - not allowed, exit right instead
-          ;; Must restore cursor first to avoid double-movement
-          ((and old-idx (== old-idx (- n 1)) new-idx (== new-idx conc-idx))
-           (go-to old-path)
-           (tree-go-to pt :end))
-          ;; Crossed from one premise to another premise - that's fine for right movement
-          ;; (moving right from premise N should go to premise N+1)
-          ((and old-idx (>= old-idx prem-start) (< old-idx (- n 1)) new-idx (> new-idx old-idx) (>= new-idx prem-start))
-           (noop))  ;; Keep the movement
-          ;; Crossed from premise to conclusion - not allowed, go to next premise instead
-          ;; Must restore cursor first to avoid double-movement
-          ((and old-idx (>= old-idx prem-start) (< old-idx (- n 1)) new-idx (== new-idx conc-idx))
-           (go-to old-path)
-           (tree-go-to pt (+ old-idx 1) :start))
-          ;; Any other unexpected crossing - keep the movement
-          (else (noop)))))))
+        ;; In label, go to premises (UP) or conclusion (DOWN)
+        ((and (proof-tree-labeled? pt) (== i 0))
+         (if to-premises?
+             (tree-go-to pt prem-start :start)
+             (tree-go-to pt conc-idx :start)))))))
 
 (tm-define (kbd-up)
   (:require (inside-proof-tree?))
   (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    ;; UP key = go to premises (which are at top visually)
     (proof-tree-navigate-vertical pt #t)))
 
 (tm-define (kbd-down)
   (:require (inside-proof-tree?))
   (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    ;; DOWN key = go to conclusion (which is at bottom visually)
     (proof-tree-navigate-vertical pt #f)))
 
 ;; Override structured-left/right/up/down to find proof-tree ancestor
diff --git a/src/Typeset/Boxes/Composite/math_boxes.cpp b/src/Typeset/Boxes/Composite/math_boxes.cpp
index 97300e2eaf..bb7800b962 100644
--- a/src/Typeset/Boxes/Composite/math_boxes.cpp
+++ b/src/Typeset/Boxes/Composite/math_boxes.cpp
@@ -764,6 +764,7 @@ struct proof_tree_box_rep : public composite_box_rep {
   SI     border;
   bool   has_label;
   bool   label_left;
+  int    n_children;  // Store original child count before adding decorations
   proof_tree_box_rep (path ip, array<box> bs, font fn, pencil pen,
                       bool has_label, bool label_left);
   operator tree () { return "proof-tree box"; }
@@ -776,9 +777,14 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
                                         pencil pen2, bool has_label2,
                                         bool label_left2)
     : composite_box_rep (ip), fn (fn2), pen (pen2), has_label (has_label2),
-      label_left (label_left2) {
+      label_left (label_left2), n_children (N (bs)) {
   // For labeled: bs[0] is label, bs[1] is conclusion, bs[2..n-1] are premises
   // For unlabeled: bs[0] is conclusion, bs[1..n-1] are premises
+  // n_children stores original count before adding decoration line box
+  //
+  // IMPORTANT: Insert boxes in ORIGINAL ORDER (0, 1, 2, ..., n-1) first,
+  // then add line box LAST. This ensures internal bs array indices match
+  // original indices for find_child to work correctly.
   SI sep     = fn->sep;
   SI hsep    = 2 * fn->spc->def;
   SI vsep    = 2 * fn->spc->def;
@@ -818,59 +824,59 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   // Total width is max of premises, conclusion, and "line + label" unit
   SI total_w = max (line_label_w, max (prem_w, conc_w));
 
-  // Position premises at the top, centered within total_w
-  // Use baseline alignment: all premises share the same baseline y-coordinate
+  // Calculate all positions first
   SI prem_start_x = (total_w - prem_w) >> 1;
   SI prem_baseline= max (bs[conc_idx]->y2, fn->y2) + sep + vsep - min_y1;
 
-  for (SI x= prem_start_x, i= prem_start; i < n; i++) {
-    SI x_i= x - bs[i]->x1;
-    SI y_i= prem_baseline; // Align at baseline (y=0 in box coords)
-    insert (bs[i], x_i, y_i);
-    x+= bs[i]->w () + hsep;
-  }
-
-  // Draw the horizontal inference line
-  // "Line + label" unit is centered within total_w
+  // Calculate line position
   SI line_label_start = (total_w - line_label_w) >> 1;
   SI line_y = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
   SI line_x1, line_x2;
   if (has_label && label_left) {
-    // Left label: [label][space][line]
     line_x1 = line_label_start + label_w + label_sp;
     line_x2 = line_x1 + line_w_total;
   }
   else {
-    // No label or right label: [line][space][label]
     line_x1 = line_label_start;
     line_x2 = line_x1 + line_w_total;
   }
-  pencil tpen = pen->set_width (line_w);
-  insert (line_box (decorate_middle (ip), line_x1, 0, line_x2, 0, tpen), 0,
-          line_y);
 
-  // Position label if present
-  if (has_label) {
-    SI label_x, label_y;
-    // Label vertical center aligned with the line
-    label_y = line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
+  // Store positions for each child box
+  array<SI> pos_x (n);
+  array<SI> pos_y (n);
 
+  // Calculate label position (index 0 for labeled)
+  if (has_label) {
+    pos_y[0] = line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
     if (label_left) {
-      // Left label: starts at line_label_start
-      label_x = line_label_start - bs[0]->x1;
+      pos_x[0] = line_label_start - bs[0]->x1;
     }
     else {
-      // Right label: starts after line + space
-      label_x = line_x2 + label_sp - bs[0]->x1;
+      pos_x[0] = line_x2 + label_sp - bs[0]->x1;
     }
-    insert (bs[0], label_x, label_y);
   }
 
-  // Position conclusion at the bottom, centered under the LINE only
+  // Calculate conclusion position
   SI line_center = (line_x1 + line_x2) >> 1;
-  insert (bs[conc_idx],
-          line_center - ((bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1),
-          0);
+  pos_x[conc_idx] = line_center - ((bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1);
+  pos_y[conc_idx] = 0;
+
+  // Calculate premise positions
+  for (SI x= prem_start_x, i= prem_start; i < n; i++) {
+    pos_x[i] = x - bs[i]->x1;
+    pos_y[i] = prem_baseline;
+    x += bs[i]->w () + hsep;
+  }
+
+  // Now insert boxes in ORIGINAL ORDER (0, 1, 2, ..., n-1)
+  for (i= 0; i < n; i++) {
+    insert (bs[i], pos_x[i], pos_y[i]);
+  }
+
+  // Insert line box LAST (so it doesn't interfere with child indices)
+  pencil tpen = pen->set_width (line_w);
+  insert (line_box (decorate_middle (ip), line_x1, 0, line_x2, 0, tpen), 0,
+          line_y);
 
   position ();
   border= line_y;
@@ -880,11 +886,9 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
 box
 proof_tree_box_rep::adjust_kerning (int mode, double factor) {
   (void) mode;
-  int        n   = N (bs);
-  int        skip= has_label ? 1 : 0; // skip line box
-  int        m   = n - skip;
-  array<box> adj (m);
-  for (int i= 0; i < m; i++)
+  // Use n_children to exclude the decoration line box
+  array<box> adj (n_children);
+  for (int i= 0; i < n_children; i++)
     adj[i]= bs[i]->adjust_kerning (0, factor);
   return proof_tree_box (ip, adj, fn, pen, has_label, label_left);
 }
@@ -892,11 +896,9 @@ proof_tree_box_rep::adjust_kerning (int mode, double factor) {
 box
 proof_tree_box_rep::expand_glyphs (int mode, double factor) {
   (void) mode;
-  int        n   = N (bs);
-  int        skip= has_label ? 1 : 0;
-  int        m   = n - skip;
-  array<box> adj (m);
-  for (int i= 0; i < m; i++)
+  // Use n_children to exclude the decoration line box
+  array<box> adj (n_children);
+  for (int i= 0; i < n_children; i++)
     adj[i]= bs[i]->expand_glyphs (0, factor);
   return proof_tree_box (ip, adj, fn, pen, has_label, label_left);
 }
@@ -910,7 +912,8 @@ proof_tree_box_rep::find_child (SI x, SI y, SI delta, bool force) {
   if (y > border) {
     int prem_start= has_label ? 2 : 1;
     int j, d= MAX_SI;
-    for (j= prem_start; j < N (bs); j++)
+    // Use n_children (not N(bs)) to exclude decoration line box
+    for (j= prem_start; j < n_children; j++)
       if (distance (j, x, y, delta) < d)
         if (bs[j]->accessible () || force) {
           d= distance (j, x, y, delta);

From a7b2fb60309a946386ade8f0f19d3bdc5053d35d Mon Sep 17 00:00:00 2001
From: fallensky2077 <mercur1al@outlook.com>
Date: Sat, 20 Dec 2025 01:40:17 +0000
Subject: [PATCH 4/7] add a convenient navigation logic

---
 TeXmacs/progs/generic/generic-edit.scm     |  79 +++++++++++-----
 src/Typeset/Boxes/Composite/math_boxes.cpp | 100 +++++++++++++--------
 2 files changed, 118 insertions(+), 61 deletions(-)

diff --git a/TeXmacs/progs/generic/generic-edit.scm b/TeXmacs/progs/generic/generic-edit.scm
index 4920aff136..6ece198307 100644
--- a/TeXmacs/progs/generic/generic-edit.scm
+++ b/TeXmacs/progs/generic/generic-edit.scm
@@ -850,7 +850,42 @@
         ((and (not forwards?) (> i prem-start))
          (tree-go-to pt (- i 1) :end))))))
 
-;; Simple vertical navigation: jump between conclusion and premises
+;; Helper: find the innermost proof-tree within a tree (for drilling down)
+(define (find-innermost-proof-tree-conclusion t)
+  ;; If t is a proof-tree, go to its conclusion and recurse
+  ;; Otherwise return #f
+  (cond
+    ((proof-tree-tag? t)
+     (let* ((conc-idx (proof-tree-conclusion-idx t))
+            (conc (tree-ref t conc-idx)))
+       ;; Check if conclusion itself contains a proof-tree
+       (or (find-innermost-proof-tree-conclusion conc)
+           ;; Otherwise return this conclusion path
+           (begin (tree-go-to t conc-idx :start) #t))))
+    ((and (tree? t) (> (tree-arity t) 0))
+     ;; Search children for proof-tree
+     (let loop ((i 0))
+       (if (>= i (tree-arity t))
+           #f
+           (or (find-innermost-proof-tree-conclusion (tree-ref t i))
+               (loop (+ i 1))))))
+    (else #f)))
+
+;; Helper: find parent proof-tree that contains current pt as a premise
+(define (find-parent-proof-tree pt)
+  ;; Go up the tree to find a proof-tree ancestor where pt is a premise
+  (and-with parent (tree-up pt)
+    (if (proof-tree-tag? parent)
+        (let* ((prem-start (proof-tree-premise-start parent))
+               (idx (tree-index pt)))
+          (if (and idx (>= idx prem-start))
+              parent  ;; pt is a premise of parent
+              #f))    ;; pt is conclusion or label, not a premise
+        (find-parent-proof-tree parent))))
+
+;; Enhanced vertical navigation:
+;; UP in conclusion -> go to closest premise, drill into nested proof-tree conclusions
+;; DOWN in conclusion -> if we're a premise of parent, go to parent's conclusion
 (define (proof-tree-navigate-vertical pt to-premises?)
   (let* ((prem-start (proof-tree-premise-start pt))
          (conc-idx (proof-tree-conclusion-idx pt))
@@ -859,25 +894,31 @@
       (cond
         ;; In conclusion, go UP to first premise
         ((and to-premises? (== i conc-idx))
-         (tree-go-to pt prem-start :start))
+         (let ((prem (tree-ref pt prem-start)))
+           ;; If premise is/contains a proof-tree, drill into its conclusion
+           (if (not (find-innermost-proof-tree-conclusion prem))
+               ;; No nested proof-tree, just go to the premise
+               (tree-go-to pt prem-start :start))))
         ;; In premise, go DOWN to conclusion
         ((and (not to-premises?) (>= i prem-start))
          (tree-go-to pt conc-idx :start))
+        ;; In conclusion, go DOWN to parent's conclusion (if we're a premise)
+        ((and (not to-premises?) (== i conc-idx))
+         (and-with parent-pt (find-parent-proof-tree pt)
+           (let ((parent-conc-idx (proof-tree-conclusion-idx parent-pt)))
+             (tree-go-to parent-pt parent-conc-idx :start))))
         ;; In label, go to premises (UP) or conclusion (DOWN)
         ((and (proof-tree-labeled? pt) (== i 0))
          (if to-premises?
              (tree-go-to pt prem-start :start)
              (tree-go-to pt conc-idx :start)))))))
 
-(tm-define (kbd-up)
-  (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (proof-tree-navigate-vertical pt #t)))
-
-(tm-define (kbd-down)
-  (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (proof-tree-navigate-vertical pt #f)))
+;; Override kbd-vertical for proof-tree nodes
+;; This is called when traversing up from focus-tree
+(tm-define (kbd-vertical t downwards?)
+  (:require (proof-tree-tag? t))
+  ;; downwards? means DOWN key, so to-premises? = (not downwards?)
+  (proof-tree-navigate-vertical t (not downwards?)))
 
 ;; Override structured-left/right/up/down to find proof-tree ancestor
 (tm-define (structured-left)
@@ -890,17 +931,11 @@
   (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
     (proof-tree-navigate-horizontal pt #t)))
 
-(tm-define (structured-up)
-  (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    ;; UP visually = go to premises (which are at top)
-    (proof-tree-navigate-vertical pt #t)))
-
-(tm-define (structured-down)
-  (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    ;; DOWN visually = go to conclusion (which is at bottom)
-    (proof-tree-navigate-vertical pt #f)))
+;; Override structured-vertical for proof-tree nodes
+(tm-define (structured-vertical t downwards?)
+  (:require (proof-tree-tag? t))
+  ;; downwards? means DOWN, so to-premises? = (not downwards?)
+  (proof-tree-navigate-vertical t (not downwards?)))
 
 ;; Insert/remove helpers for proof-tree
 (define (proof-tree-insert-horizontal pt forwards?)
diff --git a/src/Typeset/Boxes/Composite/math_boxes.cpp b/src/Typeset/Boxes/Composite/math_boxes.cpp
index bb7800b962..5460e6afc4 100644
--- a/src/Typeset/Boxes/Composite/math_boxes.cpp
+++ b/src/Typeset/Boxes/Composite/math_boxes.cpp
@@ -765,12 +765,14 @@ struct proof_tree_box_rep : public composite_box_rep {
   bool   has_label;
   bool   label_left;
   int    n_children;  // Store original child count before adding decorations
+  SI     line_center; // X-coordinate of line center (for alignment with parent)
   proof_tree_box_rep (path ip, array<box> bs, font fn, pencil pen,
                       bool has_label, bool label_left);
   operator tree () { return "proof-tree box"; }
   box adjust_kerning (int mode, double factor);
   box expand_glyphs (int mode, double factor);
   int find_child (SI x, SI y, SI delta, bool force);
+  SI  get_leaf_offset (string search);
 };
 
 proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
@@ -785,8 +787,13 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   // IMPORTANT: Insert boxes in ORIGINAL ORDER (0, 1, 2, ..., n-1) first,
   // then add line box LAST. This ensures internal bs array indices match
   // original indices for find_child to work correctly.
+  //
+  // KEY ALIGNMENT PRINCIPLE: The box is centered on its inference line center.
+  // This means x=0 corresponds to the line center, so when this box is used
+  // as a premise in a parent proof-tree, the parent will align by line centers.
   SI sep     = fn->sep;
-  SI hsep    = 2 * fn->spc->def;
+  SI min_hsep= fn->wfn;                  // minimum horizontal space between premises
+  SI hsep    = max (2 * fn->spc->def, min_hsep);
   SI vsep    = 2 * fn->spc->def;
   SI line_w  = fn->wline;
   SI label_sp= fn->spc->def; // space between line and label
@@ -796,9 +803,10 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   int prem_start = has_label ? 2 : 1;
 
   // Calculate premises total width and baseline alignment info
+  // For proof-tree premises, use their line width (x2-x1) which is centered on 0
   SI prem_w  = 0;
-  SI max_y2  = MIN_SI; // max ascent (height above baseline)
-  SI min_y1  = MAX_SI; // min descent (depth below baseline, negative value)
+  SI max_y2  = MIN_SI;
+  SI min_y1  = MAX_SI;
   for (i= prem_start; i < n; i++)
     prem_w+= bs[i]->w ();
   for (i= prem_start; i < n; i++) {
@@ -813,61 +821,59 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   // Calculate label width if present
   SI label_w= has_label ? bs[0]->w () : 0;
 
-  // Calculate inference line width
+  // Calculate inference line width (covers premises and conclusion)
   SI line_margin  = fn->spc->def;
   SI line_w_total = max (prem_w, conc_w) + 2 * line_margin;
 
-  // Calculate "line + label" unit width (treated as a whole)
-  SI line_label_w = line_w_total;
-  if (has_label) line_label_w = line_w_total + label_sp + label_w;
-
-  // Total width is max of premises, conclusion, and "line + label" unit
-  SI total_w = max (line_label_w, max (prem_w, conc_w));
+  // Line extends from -line_w_total/2 to +line_w_total/2 (centered on 0)
+  SI line_half = line_w_total >> 1;
+  SI line_x1   = -line_half;
+  SI line_x2   = line_half;
+  SI line_y    = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
 
-  // Calculate all positions first
-  SI prem_start_x = (total_w - prem_w) >> 1;
+  // Calculate premise baseline
   SI prem_baseline= max (bs[conc_idx]->y2, fn->y2) + sep + vsep - min_y1;
 
-  // Calculate line position
-  SI line_label_start = (total_w - line_label_w) >> 1;
-  SI line_y = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
-  SI line_x1, line_x2;
-  if (has_label && label_left) {
-    line_x1 = line_label_start + label_w + label_sp;
-    line_x2 = line_x1 + line_w_total;
-  }
-  else {
-    line_x1 = line_label_start;
-    line_x2 = line_x1 + line_w_total;
-  }
-
   // Store positions for each child box
   array<SI> pos_x (n);
   array<SI> pos_y (n);
 
-  // Calculate label position (index 0 for labeled)
+  // Position premises centered on line, spaced by their centers
+  // For proof-tree children, use their line_center as alignment point
+  // For other boxes, use the geometric center (x1+x2)/2
+  SI prem_half = prem_w >> 1;
+  for (SI x= -prem_half, i= prem_start; i < n; i++) {
+    SI half_w = bs[i]->w () >> 1;
+    // Try to get line_center offset for proof-tree children
+    // Default get_leaf_offset returns w(), so if != w(), it's a valid offset
+    SI align_offset = bs[i]->get_leaf_offset ("line_center");
+    if (align_offset == bs[i]->w ()) {
+      // Default return - not a proof-tree, use geometric center
+      align_offset = (bs[i]->x1 + bs[i]->x2) >> 1;
+    }
+    pos_x[i] = x + half_w - align_offset;
+    pos_y[i] = prem_baseline;
+    x += bs[i]->w () + hsep;
+  }
+
+  // Position conclusion centered on line (0 point)
+  SI conc_center = (bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1;
+  pos_x[conc_idx] = -conc_center;
+  pos_y[conc_idx] = 0;
+
+  // Position label if present
   if (has_label) {
     pos_y[0] = line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
     if (label_left) {
-      pos_x[0] = line_label_start - bs[0]->x1;
+      // Label is to the left of line: ends at line_x1 - label_sp
+      pos_x[0] = line_x1 - label_sp - bs[0]->x2;
     }
     else {
+      // Label is to the right of line: starts at line_x2 + label_sp
       pos_x[0] = line_x2 + label_sp - bs[0]->x1;
     }
   }
 
-  // Calculate conclusion position
-  SI line_center = (line_x1 + line_x2) >> 1;
-  pos_x[conc_idx] = line_center - ((bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1);
-  pos_y[conc_idx] = 0;
-
-  // Calculate premise positions
-  for (SI x= prem_start_x, i= prem_start; i < n; i++) {
-    pos_x[i] = x - bs[i]->x1;
-    pos_y[i] = prem_baseline;
-    x += bs[i]->w () + hsep;
-  }
-
   // Now insert boxes in ORIGINAL ORDER (0, 1, 2, ..., n-1)
   for (i= 0; i < n; i++) {
     insert (bs[i], pos_x[i], pos_y[i]);
@@ -880,6 +886,15 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
 
   position ();
   border= line_y;
+
+  // Store line center position before left_justify
+  // Since we centered on x=0, line_center is currently 0
+  // After left_justify(), line_center becomes -old_x1
+  SI old_x1   = x1;
+  line_center = 0;
+  left_justify ();
+  line_center = -old_x1; // Now relative to x1=0
+
   finalize ();
 }
 
@@ -927,6 +942,13 @@ proof_tree_box_rep::find_child (SI x, SI y, SI delta, bool force) {
   return i;
 }
 
+SI
+proof_tree_box_rep::get_leaf_offset (string search) {
+  // Return the line center as alignment point for parent proof-trees
+  if (search == "line_center") return line_center;
+  return composite_box_rep::get_leaf_offset (search);
+}
+
 box
 proof_tree_box (path ip, array<box> bs, font fn, pencil pen, bool has_label,
                 bool label_left) {

From ce95e1472dfe97d3852cbba617df733712162eaa Mon Sep 17 00:00:00 2001
From: fallensky2077 <mercur1al@outlook.com>
Date: Sat, 20 Dec 2025 02:19:43 +0000
Subject: [PATCH 5/7] format the cpp code by offical script

---
 moebius/moebius/tree_label.hpp             |  2 +-
 src/Typeset/Boxes/Composite/math_boxes.cpp | 59 +++++++++++-----------
 2 files changed, 31 insertions(+), 30 deletions(-)

diff --git a/moebius/moebius/tree_label.hpp b/moebius/moebius/tree_label.hpp
index a24ad3c195..f29e6d9465 100644
--- a/moebius/moebius/tree_label.hpp
+++ b/moebius/moebius/tree_label.hpp
@@ -108,7 +108,7 @@ enum tree_label : int {
   NEG,
   TREE,
   PROOF_TREE,
-  VAR_PROOF_TREE,    // proof-tree* (label on right)
+  VAR_PROOF_TREE,     // proof-tree* (label on right)
   VAR_VAR_PROOF_TREE, // proof-tree** (label on left)
   SYNTAX,
 
diff --git a/src/Typeset/Boxes/Composite/math_boxes.cpp b/src/Typeset/Boxes/Composite/math_boxes.cpp
index 5460e6afc4..ea951e9fce 100644
--- a/src/Typeset/Boxes/Composite/math_boxes.cpp
+++ b/src/Typeset/Boxes/Composite/math_boxes.cpp
@@ -792,21 +792,22 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   // This means x=0 corresponds to the line center, so when this box is used
   // as a premise in a parent proof-tree, the parent will align by line centers.
   SI sep     = fn->sep;
-  SI min_hsep= fn->wfn;                  // minimum horizontal space between premises
+  SI min_hsep= fn->wfn; // minimum horizontal space between premises
   SI hsep    = max (2 * fn->spc->def, min_hsep);
   SI vsep    = 2 * fn->spc->def;
   SI line_w  = fn->wline;
   SI label_sp= fn->spc->def; // space between line and label
 
   int i, n= N (bs);
-  int conc_idx   = has_label ? 1 : 0;
-  int prem_start = has_label ? 2 : 1;
+  int conc_idx  = has_label ? 1 : 0;
+  int prem_start= has_label ? 2 : 1;
 
   // Calculate premises total width and baseline alignment info
-  // For proof-tree premises, use their line width (x2-x1) which is centered on 0
-  SI prem_w  = 0;
-  SI max_y2  = MIN_SI;
-  SI min_y1  = MAX_SI;
+  // For proof-tree premises, use their line width (x2-x1) which is centered on
+  // 0
+  SI prem_w= 0;
+  SI max_y2= MIN_SI;
+  SI min_y1= MAX_SI;
   for (i= prem_start; i < n; i++)
     prem_w+= bs[i]->w ();
   for (i= prem_start; i < n; i++) {
@@ -822,14 +823,14 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   SI label_w= has_label ? bs[0]->w () : 0;
 
   // Calculate inference line width (covers premises and conclusion)
-  SI line_margin  = fn->spc->def;
-  SI line_w_total = max (prem_w, conc_w) + 2 * line_margin;
+  SI line_margin = fn->spc->def;
+  SI line_w_total= max (prem_w, conc_w) + 2 * line_margin;
 
   // Line extends from -line_w_total/2 to +line_w_total/2 (centered on 0)
-  SI line_half = line_w_total >> 1;
-  SI line_x1   = -line_half;
-  SI line_x2   = line_half;
-  SI line_y    = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
+  SI line_half= line_w_total >> 1;
+  SI line_x1  = -line_half;
+  SI line_x2  = line_half;
+  SI line_y   = max (bs[conc_idx]->y2, fn->y2) + (vsep >> 1);
 
   // Calculate premise baseline
   SI prem_baseline= max (bs[conc_idx]->y2, fn->y2) + sep + vsep - min_y1;
@@ -841,36 +842,36 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   // Position premises centered on line, spaced by their centers
   // For proof-tree children, use their line_center as alignment point
   // For other boxes, use the geometric center (x1+x2)/2
-  SI prem_half = prem_w >> 1;
+  SI prem_half= prem_w >> 1;
   for (SI x= -prem_half, i= prem_start; i < n; i++) {
-    SI half_w = bs[i]->w () >> 1;
+    SI half_w= bs[i]->w () >> 1;
     // Try to get line_center offset for proof-tree children
     // Default get_leaf_offset returns w(), so if != w(), it's a valid offset
-    SI align_offset = bs[i]->get_leaf_offset ("line_center");
+    SI align_offset= bs[i]->get_leaf_offset ("line_center");
     if (align_offset == bs[i]->w ()) {
       // Default return - not a proof-tree, use geometric center
-      align_offset = (bs[i]->x1 + bs[i]->x2) >> 1;
+      align_offset= (bs[i]->x1 + bs[i]->x2) >> 1;
     }
-    pos_x[i] = x + half_w - align_offset;
-    pos_y[i] = prem_baseline;
-    x += bs[i]->w () + hsep;
+    pos_x[i]= x + half_w - align_offset;
+    pos_y[i]= prem_baseline;
+    x+= bs[i]->w () + hsep;
   }
 
   // Position conclusion centered on line (0 point)
   SI conc_center = (bs[conc_idx]->x1 + bs[conc_idx]->x2) >> 1;
-  pos_x[conc_idx] = -conc_center;
-  pos_y[conc_idx] = 0;
+  pos_x[conc_idx]= -conc_center;
+  pos_y[conc_idx]= 0;
 
   // Position label if present
   if (has_label) {
-    pos_y[0] = line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
+    pos_y[0]= line_y - ((bs[0]->y1 + bs[0]->y2) >> 1);
     if (label_left) {
       // Label is to the left of line: ends at line_x1 - label_sp
-      pos_x[0] = line_x1 - label_sp - bs[0]->x2;
+      pos_x[0]= line_x1 - label_sp - bs[0]->x2;
     }
     else {
       // Label is to the right of line: starts at line_x2 + label_sp
-      pos_x[0] = line_x2 + label_sp - bs[0]->x1;
+      pos_x[0]= line_x2 + label_sp - bs[0]->x1;
     }
   }
 
@@ -880,7 +881,7 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   }
 
   // Insert line box LAST (so it doesn't interfere with child indices)
-  pencil tpen = pen->set_width (line_w);
+  pencil tpen= pen->set_width (line_w);
   insert (line_box (decorate_middle (ip), line_x1, 0, line_x2, 0, tpen), 0,
           line_y);
 
@@ -890,10 +891,10 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   // Store line center position before left_justify
   // Since we centered on x=0, line_center is currently 0
   // After left_justify(), line_center becomes -old_x1
-  SI old_x1   = x1;
-  line_center = 0;
+  SI old_x1  = x1;
+  line_center= 0;
   left_justify ();
-  line_center = -old_x1; // Now relative to x1=0
+  line_center= -old_x1; // Now relative to x1=0
 
   finalize ();
 }

From 2950653f29f3740fe6bba10e033a9bae3ef9f9bb Mon Sep 17 00:00:00 2001
From: fallensky2077 <mercur1al@outlook.com>
Date: Sun, 21 Dec 2025 15:31:49 +0000
Subject: [PATCH 6/7] refactor so no new primitive

---
 TeXmacs/packages/standard/std-math.ts      |  19 ++
 TeXmacs/progs/generic/generic-edit.scm     | 290 ++++++++++++++++-----
 TeXmacs/progs/math/math-drd.scm            |   5 +-
 TeXmacs/progs/math/math-menu.scm           |  67 +++--
 TeXmacs/progs/math/math-sem-edit.scm       |   2 +
 TeXmacs/progs/utils/library/cpp-wrap.scm   |  10 +-
 moebius/moebius/drd/drd_std.cpp            |   7 +-
 moebius/moebius/tree_label.hpp             |   3 -
 moebius/moebius/vars.cpp                   |   3 +
 moebius/moebius/vars.hpp                   |   3 +
 src/Edit/Interface/edit_footer.cpp         |   8 -
 src/Edit/Modify/edit_delete.cpp            |   3 -
 src/Edit/Modify/edit_math.cpp              |  16 +-
 src/Edit/Modify/edit_math.hpp              |   1 -
 src/Edit/editor.hpp                        |   1 -
 src/Scheme/Glue/build-glue-editor.scm      |   1 -
 src/Scheme/Glue/glue_editor.lua            |   5 -
 src/Typeset/Boxes/Composite/math_boxes.cpp |  73 ++++--
 src/Typeset/Concat/concat_math.cpp         |  48 ++--
 src/Typeset/Concat/concater.cpp            |   9 -
 src/Typeset/Concat/concater.hpp            |   2 -
 src/Typeset/Env/env_default.cpp            |   3 +
 22 files changed, 400 insertions(+), 179 deletions(-)

diff --git a/TeXmacs/packages/standard/std-math.ts b/TeXmacs/packages/standard/std-math.ts
index a7254f41d4..df9b70f66e 100644
--- a/TeXmacs/packages/standard/std-math.ts
+++ b/TeXmacs/packages/standard/std-math.ts
@@ -161,6 +161,25 @@
 
   <assign|cfrac|<macro|x|y|<with|mode|math|<dfrac|<arg|x>|<resize|<arg|y>|||<plus|1r|-1sep>|>>>>>
 
+  <\comment>
+    Proof tree macros: wrap tree primitive with tree-mode=proof
+    - proof-tree: no label
+    - proof-tree*: label on right
+    - proof-tree**: label on left
+  </comment>
+
+  <assign|proof-tree|<macro|body|<with|tree-mode|proof|<arg|body>>>>
+
+  <assign|proof-tree*|<macro|body|<with|tree-mode|proof|tree-label-pos|right|<arg|body>>>>
+
+  <assign|proof-tree**|<macro|body|<with|tree-mode|proof|tree-label-pos|left|<arg|body>>>>
+
+  <drd-props|proof-tree|arity|1>
+
+  <drd-props|proof-tree*|arity|1>
+
+  <drd-props|proof-tree**|arity|1>
+
   <assign|frac*|<macro|x|y|<move|<lsup|<arg|x>><resize|/|<plus|1l|0.15em>|<plus|1b|0.5em>|<minus|1r|0.15em>|<minus|1t|0.5em>><rsub|<arg|y>>||0.05em>>>
 
   <drd-props|frac*|arity|2|syntax|<macro|x|y|<arg|x>/<arg|y>>>
diff --git a/TeXmacs/progs/generic/generic-edit.scm b/TeXmacs/progs/generic/generic-edit.scm
index 6ece198307..0e41e99377 100644
--- a/TeXmacs/progs/generic/generic-edit.scm
+++ b/TeXmacs/progs/generic/generic-edit.scm
@@ -338,13 +338,6 @@
   (or (tree-in? t '(tree))
       (table-markup-context? t)))
 
-(tm-define (structured-vertical? t)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
-  #t)
-
-(tm-define (structured-horizontal? t)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
-  #t)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Focus predicates
@@ -777,17 +770,54 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Proof tree editing
+;; Note: proof-tree is now a macro that wraps tree with tree-mode=proof
+;; The structure is: (with tree-mode proof (tree conclusion premise1 premise2 ...))
+;; For labeled: (with tree-mode proof tree-label-pos right (tree label conclusion premise1 ...))
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
+;; Find the enclosing 'with' tag that sets tree-mode=proof
+(tm-define (find-proof-tree-with t)
+  (cond
+    ((not (tree? t)) #f)
+    ((and (tree-is? t 'with)
+          (>= (tree-arity t) 3)
+          (tm-equal? (tree-ref t 0) "tree-mode")
+          (tm-equal? (tree-ref t 1) "proof"))
+     t)
+    (else (find-proof-tree-with (tree-up t)))))
+
+(tm-define (get-proof-tree-label-pos with-t)
+  ;; Get the current label position from the with tag
+  ;; Returns "none", "right", or "left"
+  ;; Empty string "" is treated as "none" for consistency
+  (if (and (>= (tree-arity with-t) 5)
+           (tm-equal? (tree-ref with-t 2) "tree-label-pos"))
+      (let ((pos (tm->string (tree-ref with-t 3))))
+        (if (== pos "") "none" pos))
+      "none"))
+
+;; Check if t is a tree in proof-tree mode
 (tm-define (proof-tree-tag? t)
-  (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  (and (tree-is? t 'tree)
+       (find-proof-tree-with t)))
 
+;; Check if the proof-tree has a label
 (define (proof-tree-labeled? t)
-  (tree-in? t '(proof-tree* proof-tree**)))
+  (and (proof-tree-tag? t)
+       (and-with with-t (find-proof-tree-with t)
+         (let ((pos (get-proof-tree-label-pos with-t)))
+           (or (== pos "left") (== pos "right"))))))
+
+;; Check if label is on the left
+(define (proof-tree-label-left? t)
+  (and-with with-t (find-proof-tree-with t)
+    (== (get-proof-tree-label-pos with-t) "left")))
 
 ;; Predicate: are we inside a proof-tree?
+;; Uses get-env-tree to check cursor's environment
 (define (inside-proof-tree?)
-  (and (tree-innermost '(proof-tree proof-tree* proof-tree**)) #t))
+  (and (tree-innermost 'tree)
+       (tm-equal? (get-env-tree "tree-mode") "proof")))
 
 (define (proof-tree-premise-start t)
   ;; Return the index of the first premise
@@ -797,32 +827,54 @@
   ;; Return the index of the conclusion
   (if (proof-tree-labeled? t) 1 0))
 
-
-;; Override variant-set for proof-tree to handle structure changes
-(tm-define (variant-set t new-tag)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
-  (with-focus-after t
-    (let* ((old-lab (tree-label t))
-           (old-labeled? (in? old-lab '(proof-tree* proof-tree**)))
-           (new-labeled? (in? new-tag '(proof-tree* proof-tree**)))
-           (idx (or (tree-down-index t) 0)))
+(define (proof-tree-cycle-label-pos current forward?)
+  ;; Return the next label position in the cycle
+  (let ((order (if forward?
+                   '("none" "right" "left")
+                   '("none" "left" "right"))))
+    (let loop ((l order))
       (cond
-        ;; Adding label: insert empty label at position 0
-        ((and (not old-labeled?) new-labeled?)
-         (tree-insert! t 0 '(""))
-         (tree-assign-node! t new-tag))
-        ;; Removing label: remove label at position 0
-        ((and old-labeled? (not new-labeled?))
-         (tree-remove! t 0 1)
-         (tree-assign-node! t new-tag))
-        ;; Just changing between proof-tree* and proof-tree**, or no change
-        (else
-         (tree-assign-node! t new-tag))))))
-
-;; Define variants for proof-tree
-(tm-define (focus-variants-of t)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
-  '(proof-tree proof-tree* proof-tree**))
+        ((null? l) "none")
+        ((null? (cdr l)) (car order))
+        ((== (car l) current) (cadr l))
+        (else (loop (cdr l)))))))
+
+(tm-define (proof-tree-set-variant with-t new-pos)
+  ;; Set the proof-tree variant by modifying with tag and tree structure
+  ;; All proof-trees have tree-label-pos (either "", "left", or "right")
+  ;; Tree is always at index 4 in the with tag
+  (let* ((current-pos (get-proof-tree-label-pos with-t))
+         (tree-t (tree-ref with-t 4)))
+    (when (tree-is? tree-t 'tree)
+      (cond
+        ;; From no label to labeled: add label child to tree, set position value
+        ((and (== current-pos "none") (!= new-pos "none"))
+         (tree-insert! tree-t 0 '(""))
+         (tree-set (tree-ref with-t 3) new-pos))
+        ;; From labeled to no label: remove label child, set position to ""
+        ((and (!= current-pos "none") (== new-pos "none"))
+         (tree-remove! tree-t 0 1)
+         (tree-set (tree-ref with-t 3) ""))
+        ;; Change label side (left <-> right): just change the value
+        ((and (!= current-pos "none") (!= new-pos "none"))
+         (tree-set (tree-ref with-t 3) new-pos))))))
+
+;; Helper function to set proof-tree label from the focused tree
+(tm-define (proof-tree-set-label-pos t new-pos)
+  (and-with with-t (find-proof-tree-with t)
+    (proof-tree-set-variant with-t new-pos)))
+
+;; Get current label position from focused tree
+(tm-define (proof-tree-current-label-pos t)
+  (and-with with-t (find-proof-tree-with t)
+    (get-proof-tree-label-pos with-t)))
+
+(tm-define (variant-circulate t forward?)
+  (:require (proof-tree-tag? t))
+  (and-with with-t (find-proof-tree-with t)
+    (let* ((current-pos (get-proof-tree-label-pos with-t))
+           (new-pos (proof-tree-cycle-label-pos current-pos forward?)))
+      (proof-tree-set-variant with-t new-pos))))
 
 ;; Navigation for proof-tree:
 ;; - kbd-left/kbd-right: use default behavior (works correctly now)
@@ -923,12 +975,12 @@
 ;; Override structured-left/right/up/down to find proof-tree ancestor
 (tm-define (structured-left)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+  (with pt (tree-innermost 'tree)
     (proof-tree-navigate-horizontal pt #f)))
 
 (tm-define (structured-right)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+  (with pt (tree-innermost 'tree)
     (proof-tree-navigate-horizontal pt #t)))
 
 ;; Override structured-vertical for proof-tree nodes
@@ -967,50 +1019,172 @@
   (let* ((prem-start (proof-tree-premise-start pt))
          (i (proof-tree-cursor-child-index pt)))
     ;; Insert sub-proof: wrap current premise in a new proof-tree
+    ;; Must explicitly set tree-label-pos to "" to override any inherited value from parent
     (when (and i (>= i prem-start))
-      (if downwards?
-          ;; Insert down: add empty conclusion below, current stays as premise
-          ;; This creates a sub-tree where current is premise, "" is conclusion
-          (begin
-            (tree-set! pt i `(proof-tree "" ,(tree-ref pt i)))
-            (tree-go-to pt i 0 0))
-          ;; Insert up: wrap current as conclusion of new sub-tree with empty premise above
-          ;; This creates a sub-tree where current becomes conclusion, "" is new premise
-          (begin
-            (tree-set! pt i `(proof-tree ,(tree-ref pt i) ""))
-            (tree-go-to pt i 1 0))))))
+      (let* ((child-t (tree-ref pt i))
+             (content (tree->stree child-t)))
+        (if downwards?
+            ;; Insert down: add empty conclusion below, current stays as premise
+            (begin
+              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "" (tree "" ,content)))
+              (tree-go-to child-t 4 0 0))
+            ;; Insert up: wrap current as conclusion of new sub-tree with empty premise above
+            (begin
+              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "" (tree ,content "")))
+              (tree-go-to child-t 4 1 0)))))))
 
 ;; Override structured-insert/remove for proof-tree
 (tm-define (structured-insert-left)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (proof-tree-insert-horizontal pt #f)))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-insert-horizontal pt #f))))
 
 (tm-define (structured-insert-right)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (proof-tree-insert-horizontal pt #t)))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-insert-horizontal pt #t))))
 
 (tm-define (structured-remove-left)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (proof-tree-remove-horizontal pt #f)))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-remove-horizontal pt #f))))
 
 (tm-define (structured-remove-right)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
-    (proof-tree-remove-horizontal pt #t)))
+  (with pt (tree-innermost 'tree)
+    (when (proof-tree-tag? pt)
+      (proof-tree-remove-horizontal pt #t))))
 
 (tm-define (structured-insert-up)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+  (with pt (tree-innermost 'tree)
     (proof-tree-insert-vertical pt #f)))
 
 (tm-define (structured-insert-down)
   (:require (inside-proof-tree?))
-  (with pt (tree-innermost '(proof-tree proof-tree* proof-tree**))
+  (with pt (tree-innermost 'tree)
     (proof-tree-insert-vertical pt #t)))
 
+;; Helper: check if all children of proof-tree are empty
+(define (proof-tree-all-empty? pt)
+  (let loop ((i 0))
+    (cond
+      ((>= i (tree-arity pt)) #t)
+      ((not (tree-empty? (tree-ref pt i))) #f)
+      (else (loop (+ i 1))))))
+
+;; Helper: get visual order of indices for proof-tree horizontal navigation
+;; Visual order follows the layout: left-label → premises → right-label
+;; Conclusion is excluded (accessed via up/down navigation)
+(define (proof-tree-visual-order pt)
+  (let* ((labeled? (proof-tree-labeled? pt))
+         (label-left? (and labeled? (proof-tree-label-left? pt)))
+         (prem-start (proof-tree-premise-start pt))
+         (n (tree-arity pt))
+         (premises (let loop ((i prem-start) (acc '()))
+                     (if (>= i n) (reverse acc) (loop (+ i 1) (cons i acc))))))
+    (cond
+      ((not labeled?) premises)                    ;; non-labeled: just premises
+      (label-left? (cons 0 premises))              ;; left-label: label first, then premises
+      (else (append premises (list 0))))))         ;; right-label: premises, then label
+
+;; Helper: move to adjacent field in proof-tree using visual order
+(define (proof-tree-move-to-adjacent-field pt i forwards?)
+  (let* ((order (proof-tree-visual-order pt))
+         (pos (list-find-index order (lambda (x) (== x i)))))
+    (if pos
+        (let* ((new-pos (if forwards? (+ pos 1) (- pos 1)))
+               (new-i (and (>= new-pos 0) (< new-pos (length order))
+                           (list-ref order new-pos))))
+          (cond
+            ((and new-i forwards?)
+             (tree-go-to pt new-i :start))
+            ((and new-i (not forwards?))
+             (tree-go-to pt new-i :end))
+            (else (noop))))
+        (noop))))
+
+;; Helper: check if index is a premise in the proof-tree
+(define (proof-tree-premise? pt i)
+  (let ((prem-start (proof-tree-premise-start pt)))
+    (and i (>= i prem-start))))
+
+;; Helper: count number of premises in proof-tree
+(define (proof-tree-premise-count pt)
+  (let ((prem-start (proof-tree-premise-start pt)))
+    (- (tree-arity pt) prem-start)))
+
+;; Helper: remove a premise from proof-tree and move cursor appropriately
+(define (proof-tree-remove-premise pt i forwards?)
+  (let* ((prem-start (proof-tree-premise-start pt))
+         (n (tree-arity pt)))
+    (tree-remove! pt i 1)
+    ;; Move cursor to adjacent premise
+    (cond
+      (forwards?
+       (if (>= i (tree-arity pt))
+           (tree-go-to pt (- i 1) :end)
+           (tree-go-to pt i :start)))
+      (else
+       (if (> i prem-start)
+           (tree-go-to pt (- i 1) :end)
+           (tree-go-to pt prem-start :start))))))
+
+;; Override kbd-remove for proof-tree fields
+;; When at field boundary: move to adjacent field instead of deleting structure
+;; Visual order: left-label → premises → right-label (conclusion excluded)
+;; Conclusion uses up/down navigation, so delete at its boundaries does nothing
+;; Empty premise with multiple premises: remove the premise
+;; Only delete the entire proof-tree when all fields are empty
+(tm-define (kbd-remove t forwards?)
+  (:require (and (inside-proof-tree?)
+                 (not (selection-active-any?))))
+  (with pt (tree-innermost 'tree)
+    (let* ((i (tree-down-index pt))
+           (child (and i (tree-ref pt i)))
+           (at-start (and child (tree-cursor-at? child :start)))
+           (at-end (and child (tree-cursor-at? child :end)))
+           (child-empty (and child (tree-empty? child)))
+           (is-premise (proof-tree-premise? pt i))
+           (prem-count (proof-tree-premise-count pt)))
+      (cond
+        ;; If all fields are empty and we're trying to delete, remove the whole with structure
+        ((and child-empty (proof-tree-all-empty? pt))
+         (with with-t (find-proof-tree-with pt)
+           (when with-t
+             (tree-cut with-t))))
+        ;; Empty premise with more than one premise: remove this premise
+        ((and child-empty is-premise (> prem-count 1))
+         (proof-tree-remove-premise pt i forwards?))
+        ;; Backspace at start of field: move to previous field in visual order
+        ;; (does nothing if in conclusion, as it's not in visual order)
+        ((and (not forwards?) at-start)
+         (proof-tree-move-to-adjacent-field pt i #f))
+        ;; Delete at end of field: move to next field in visual order
+        ;; (does nothing if in conclusion, as it's not in visual order)
+        ((and forwards? at-end)
+         (proof-tree-move-to-adjacent-field pt i #t))
+        ;; Otherwise, do normal text removal
+        (else (remove-text forwards?))))))
+
+;; Override remove-structure-upwards for proof-tree
+;; When inside a proof-tree, remove the entire with structure, not just the tree tag
+(tm-define (remove-structure-upwards)
+  (:require (inside-proof-tree?))
+  (with pt (tree-innermost 'tree)
+    (with with-t (find-proof-tree-with pt)
+      (if with-t
+          ;; Replace the with structure with the conclusion content
+          (let* ((conc-idx (proof-tree-conclusion-idx pt))
+                 (conclusion (tree-ref pt conc-idx)))
+            (tree-set! with-t (tree-copy conclusion))
+            (tree-go-to with-t :end))
+          ;; Fallback to default behavior
+          (former)))))
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Extra editing functions
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/TeXmacs/progs/math/math-drd.scm b/TeXmacs/progs/math/math-drd.scm
index bdd61618b5..625ba9388e 100644
--- a/TeXmacs/progs/math/math-drd.scm
+++ b/TeXmacs/progs/math/math-drd.scm
@@ -16,10 +16,7 @@
 
 (define-group variant-tag
   (fraction-tag) (vertical-script-tag)
-  (textual-operator-tag) (proof-tree-tag))
-
-(define-group proof-tree-tag
-  proof-tree proof-tree* proof-tree**)
+  (textual-operator-tag))
 
 (define-group fraction-tag
   frac tfrac dfrac frac* cfrac)
diff --git a/TeXmacs/progs/math/math-menu.scm b/TeXmacs/progs/math/math-menu.scm
index a8584d45fe..a3e0f4f128 100644
--- a/TeXmacs/progs/math/math-menu.scm
+++ b/TeXmacs/progs/math/math-menu.scm
@@ -1069,8 +1069,8 @@
       ("Tree" (make-tree))
       ---
       ("Proof tree" (make-proof-tree))
-      ("Proof tree (right label)" (make 'proof-tree*))
-      ("Proof tree (left label)" (make 'proof-tree**)))
+      ("Proof tree (right label)" (make-proof-tree*))
+      ("Proof tree (left label)" (make-proof-tree**)))
   ---
   (-> "Script"
       ("Left subscript" (make-script #f #f))
@@ -1478,31 +1478,62 @@
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Proof tree focus menus
+;; Note: proof-tree is now a macro wrapping tree with tree-mode=proof
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (tm-define (focus-can-insert-remove? t)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  (:require (proof-tree-tag? t))
   #t)
 
+;; For proof-tree, we use symbolic variant names for the focus menu
+;; These don't correspond to actual tags but allow the dropdown to work
 (tm-define (focus-tag-name l)
-  (:require (in? l '(proof-tree proof-tree* proof-tree**)))
-  (cond ((== l 'proof-tree) "No label")
-        ((== l 'proof-tree*) "Right label")
-        ((== l 'proof-tree**) "Left label")))
+  (:require (== l 'proof-tree-none))
+  "Proof tree")
+
+(tm-define (focus-tag-name l)
+  (:require (== l 'proof-tree-right))
+  "Proof tree (right label)")
+
+(tm-define (focus-tag-name l)
+  (:require (== l 'proof-tree-left))
+  "Proof tree (left label)")
+
+;; Return the current variant symbol based on label position
+(define (proof-tree-current-variant t)
+  (let ((pos (proof-tree-current-label-pos t)))
+    (cond ((== pos "right") 'proof-tree-right)
+          ((== pos "left") 'proof-tree-left)
+          (else 'proof-tree-none))))
+
+;; Override focus-tag-name for tree when in proof mode
+(tm-define (focus-tag-name l)
+  (:require (and (== l 'tree) (tm-equal? (get-env-tree "tree-mode") "proof")))
+  (let ((pos (get-env-tree "tree-label-pos")))
+    (cond ((tm-equal? pos "right") "Proof tree (right label)")
+          ((tm-equal? pos "left") "Proof tree (left label)")
+          (else "Proof tree"))))
+
+;; Return 3 variants so dropdown appears
+(tm-define (focus-variants-of t)
+  (:require (proof-tree-tag? t))
+  '(proof-tree-none proof-tree-right proof-tree-left))
 
-;; Custom variant menu for proof-tree
-;; Note: t is already the proof-tree when :require matches
 (tm-menu (focus-variant-menu t)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
-  ((check "No label" "v" (tree-is? t 'proof-tree))
-   (variant-set t 'proof-tree))
-  ((check "Right label" "v" (tree-is? t 'proof-tree*))
-   (variant-set t 'proof-tree*))
-  ((check "Left label" "v" (tree-is? t 'proof-tree**))
-   (variant-set t 'proof-tree**)))
+  (:require (proof-tree-tag? t))
+  (let ((current (proof-tree-current-variant t)))
+    ((check (eval (focus-tag-name 'proof-tree-none)) "v"
+            (== current 'proof-tree-none))
+     (proof-tree-set-label-pos t "none"))
+    ((check (eval (focus-tag-name 'proof-tree-right)) "v"
+            (== current 'proof-tree-right))
+     (proof-tree-set-label-pos t "right"))
+    ((check (eval (focus-tag-name 'proof-tree-left)) "v"
+            (== current 'proof-tree-left))
+     (proof-tree-set-label-pos t "left"))))
 
 (tm-menu (focus-insert-menu t)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  (:require (proof-tree-tag? t))
   ("Insert premise before" (structured-insert-left))
   ("Insert premise after" (structured-insert-right))
   ---
@@ -1510,7 +1541,7 @@
   ("Remove premise" (structured-remove-right)))
 
 (tm-menu (focus-insert-icons t)
-  (:require (tree-in? t '(proof-tree proof-tree* proof-tree**)))
+  (:require (proof-tree-tag? t))
   ((balloon (icon "tm_insert_left.xpm") "Insert premise before")
    (structured-insert-left))
   ((balloon (icon "tm_insert_right.xpm") "Insert premise after")
diff --git a/TeXmacs/progs/math/math-sem-edit.scm b/TeXmacs/progs/math/math-sem-edit.scm
index ad5ba2582f..9acc04ea96 100644
--- a/TeXmacs/progs/math/math-sem-edit.scm
+++ b/TeXmacs/progs/math/math-sem-edit.scm
@@ -435,6 +435,8 @@
 (wrap-inserter make-neg)
 (wrap-inserter make-tree)
 (wrap-inserter make-proof-tree)
+(wrap-inserter make-proof-tree*)
+(wrap-inserter make-proof-tree**)
 (wrap-inserter make-long-arrow)
 (wrap-inserter make-long-arrow*)
 
diff --git a/TeXmacs/progs/utils/library/cpp-wrap.scm b/TeXmacs/progs/utils/library/cpp-wrap.scm
index 3c59f4433e..c009dbc2cc 100644
--- a/TeXmacs/progs/utils/library/cpp-wrap.scm
+++ b/TeXmacs/progs/utils/library/cpp-wrap.scm
@@ -108,7 +108,15 @@
 (tm-define (make-wide-under s) (cpp-make-wide-under s))
 (tm-define (make-neg) (cpp-make-neg))
 (tm-define (make-tree) (cpp-make-tree))
-(tm-define (make-proof-tree) (cpp-make-proof-tree))
+
+(tm-define (make-proof-tree)
+  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "" (tree "" "")) '(4 0 0)))
+
+(tm-define (make-proof-tree*)
+  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "right" (tree "" "" "")) '(4 0 0)))
+
+(tm-define (make-proof-tree**)
+  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "left" (tree "" "" "")) '(4 0 0)))
 
 (tm-define (clipboard-copy cb) (cpp-clipboard-copy cb))
 (tm-define (clipboard-cut cb) (cpp-clipboard-cut cb))
diff --git a/moebius/moebius/drd/drd_std.cpp b/moebius/moebius/drd/drd_std.cpp
index f441e0c8f0..eca47fda69 100644
--- a/moebius/moebius/drd/drd_std.cpp
+++ b/moebius/moebius/drd/drd_std.cpp
@@ -281,12 +281,7 @@ init_std_drd () {
             ->name ("wide under")
             ->name (1, "accent"));
   init (NEG, "neg", fixed (1)->accessible (0)->name ("negation"));
-  init (TREE, "tree", repeat (2, 1)->accessible (0));
-  init (PROOF_TREE, "proof-tree", repeat (2, 1)->accessible (0));
-  init (VAR_PROOF_TREE, "proof-tree*",
-        repeat (3, 1)->accessible (0)->name (0, "label"));
-  init (VAR_VAR_PROOF_TREE, "proof-tree**",
-        repeat (3, 1)->accessible (0)->name (0, "label"));
+  init (TREE, "tree", repeat (2, 1)->accessible (0)->name ("tree"));
   init (SYNTAX, "syntax",
         fixed (1, 1, BIFORM)
             ->accessible (0)
diff --git a/moebius/moebius/tree_label.hpp b/moebius/moebius/tree_label.hpp
index f29e6d9465..70dd417f27 100644
--- a/moebius/moebius/tree_label.hpp
+++ b/moebius/moebius/tree_label.hpp
@@ -107,9 +107,6 @@ enum tree_label : int {
   VAR_WIDE,
   NEG,
   TREE,
-  PROOF_TREE,
-  VAR_PROOF_TREE,     // proof-tree* (label on right)
-  VAR_VAR_PROOF_TREE, // proof-tree** (label on left)
   SYNTAX,
 
   // tabular material
diff --git a/moebius/moebius/vars.cpp b/moebius/moebius/vars.cpp
index 223f0c8b27..bbcdd7a74e 100644
--- a/moebius/moebius/vars.cpp
+++ b/moebius/moebius/vars.cpp
@@ -93,6 +93,9 @@ string MATH_TOP_SWELL_END ("math-top-swell-end");
 string MATH_BOT_SWELL_START ("math-bot-swell-start");
 string MATH_BOT_SWELL_END ("math-bot-swell-end");
 
+string TREE_MODE ("tree-mode");
+string TREE_LABEL_POS ("tree-label-pos");
+
 string PROG_LANGUAGE ("prog-language");
 string PROG_SCRIPTS ("prog-scripts");
 string PROG_FONT ("prog-font");
diff --git a/moebius/moebius/vars.hpp b/moebius/moebius/vars.hpp
index 4c1e62a559..ce0da1636d 100644
--- a/moebius/moebius/vars.hpp
+++ b/moebius/moebius/vars.hpp
@@ -87,6 +87,9 @@ extern string MATH_TOP_SWELL_END;
 extern string MATH_BOT_SWELL_START;
 extern string MATH_BOT_SWELL_END;
 
+extern string TREE_MODE;
+extern string TREE_LABEL_POS;
+
 extern string PROG_LANGUAGE;
 extern string PROG_SCRIPTS;
 extern string PROG_FONT;
diff --git a/src/Edit/Interface/edit_footer.cpp b/src/Edit/Interface/edit_footer.cpp
index f6849a000c..461d9e11e9 100644
--- a/src/Edit/Interface/edit_footer.cpp
+++ b/src/Edit/Interface/edit_footer.cpp
@@ -363,14 +363,6 @@ edit_interface_rep::compute_compound_footer (tree t, path p) {
   case TREE:
     if (l == 0) return concat (up, "root ");
     else return concat (up, "branch(" * as_string (l) * ") ");
-  case PROOF_TREE:
-    if (l == 0) return concat (up, "conclusion ");
-    else return concat (up, "premise(" * as_string (l) * ") ");
-  case VAR_PROOF_TREE:
-  case VAR_VAR_PROOF_TREE:
-    if (l == 0) return concat (up, "label ");
-    else if (l == 1) return concat (up, "conclusion ");
-    else return concat (up, "premise(" * as_string (l - 1) * ") ");
   case TFORMAT:
     return up;
   case TABLE:
diff --git a/src/Edit/Modify/edit_delete.cpp b/src/Edit/Modify/edit_delete.cpp
index 4b56207c05..90a0b133e4 100644
--- a/src/Edit/Modify/edit_delete.cpp
+++ b/src/Edit/Modify/edit_delete.cpp
@@ -233,9 +233,6 @@ edit_text_rep::remove_text_sub (bool forward) {
       back_in_wide (u, p, forward);
       return;
     case TREE:
-    case PROOF_TREE:
-    case VAR_PROOF_TREE:
-    case VAR_VAR_PROOF_TREE:
       back_in_tree (u, p, forward);
       return;
     case TFORMAT:
diff --git a/src/Edit/Modify/edit_math.cpp b/src/Edit/Modify/edit_math.cpp
index 4663b8f7ec..919c5efdc7 100644
--- a/src/Edit/Modify/edit_math.cpp
+++ b/src/Edit/Modify/edit_math.cpp
@@ -331,18 +331,6 @@ edit_math_rep::make_tree () {
   }
 }
 
-void
-edit_math_rep::make_proof_tree () {
-  if (selection_active_small ())
-    insert_tree (tree (PROOF_TREE, selection_get_cut (), ""), path (1, 0));
-  else {
-    insert_tree (tree (PROOF_TREE, "", ""), path (0, 0));
-    set_message (concat (kbd_shortcut ("(structured-insert-right)"),
-                         ": insert a new premise"),
-                 "proof-tree");
-  }
-}
-
 void
 edit_math_rep::back_in_tree (tree t, path p, bool forward) {
   int i= last_item (p);
@@ -366,9 +354,7 @@ edit_math_rep::back_in_tree (tree t, path p, bool forward) {
     else go_to_start (path_up (p) * (i + 1));
   }
   else {
-    if (t == tree (TREE, "", "") || t == tree (PROOF_TREE, "", "") ||
-        t == tree (VAR_PROOF_TREE, "", "", "") ||
-        t == tree (VAR_VAR_PROOF_TREE, "", "", "")) {
+    if (t == tree (TREE, "", "")) {
       p= path_up (p);
       assign (p, "");
       correct (path_up (p));
diff --git a/src/Edit/Modify/edit_math.hpp b/src/Edit/Modify/edit_math.hpp
index 01f98562e4..6891572a9d 100644
--- a/src/Edit/Modify/edit_math.hpp
+++ b/src/Edit/Modify/edit_math.hpp
@@ -31,7 +31,6 @@ class edit_math_rep : virtual public editor_rep {
   void make_wide_under (string wide);
   void make_neg ();
   void make_tree ();
-  void make_proof_tree ();
   void back_around (tree t, path p, bool forward);
   void back_prime (tree t, path p, bool forward);
   void back_in_around (tree t, path p, bool forward);
diff --git a/src/Edit/editor.hpp b/src/Edit/editor.hpp
index 53f5dc04f2..1e44f9cef9 100644
--- a/src/Edit/editor.hpp
+++ b/src/Edit/editor.hpp
@@ -417,7 +417,6 @@ class editor_rep : public simple_widget_rep {
   virtual void make_wide_under (string wide)     = 0;
   virtual void make_neg ()                       = 0;
   virtual void make_tree ()                      = 0;
-  virtual void make_proof_tree ()                = 0;
 
   /* public routines from edit_table */
   virtual void       make_table (int nr_rows= 1, int nr_cols= 1)         = 0;
diff --git a/src/Scheme/Glue/build-glue-editor.scm b/src/Scheme/Glue/build-glue-editor.scm
index 471f1d22ac..21d1b40a3c 100644
--- a/src/Scheme/Glue/build-glue-editor.scm
+++ b/src/Scheme/Glue/build-glue-editor.scm
@@ -142,7 +142,6 @@
   (cpp-make-var-sqrt make_var_sqrt (void))
   (cpp-make-neg make_neg (void))
   (cpp-make-tree make_tree (void))
-  (cpp-make-proof-tree make_proof_tree (void))
 
   ;; modify tables
   (make-subtable make_subtable (void))
diff --git a/src/Scheme/Glue/glue_editor.lua b/src/Scheme/Glue/glue_editor.lua
index 8e6a804a8f..1afc80ed7f 100644
--- a/src/Scheme/Glue/glue_editor.lua
+++ b/src/Scheme/Glue/glue_editor.lua
@@ -852,11 +852,6 @@ function main()
                 cpp_name = "make_tree",
                 ret_type = "void"
             },
-            {
-                scm_name = "cpp-make-proof-tree",
-                cpp_name = "make_proof_tree",
-                ret_type = "void"
-            },
 
             -- modify tables
             {
diff --git a/src/Typeset/Boxes/Composite/math_boxes.cpp b/src/Typeset/Boxes/Composite/math_boxes.cpp
index ea951e9fce..1cd0729e7e 100644
--- a/src/Typeset/Boxes/Composite/math_boxes.cpp
+++ b/src/Typeset/Boxes/Composite/math_boxes.cpp
@@ -802,19 +802,44 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   int conc_idx  = has_label ? 1 : 0;
   int prem_start= has_label ? 2 : 1;
 
-  // Calculate premises total width and baseline alignment info
-  // For proof-tree premises, use their line width (x2-x1) which is centered on
-  // 0
-  SI prem_w= 0;
+  // Calculate premises layout info
+  // For proper spacing with alignment, we need left/right extents from
+  // alignment point This prevents overlap when child proof-trees have labels
+  // extending beyond their lines
   SI max_y2= MIN_SI;
   SI min_y1= MAX_SI;
-  for (i= prem_start; i < n; i++)
-    prem_w+= bs[i]->w ();
+
+  // Calculate align offsets (line center or geometric center) for all premises
+  array<SI> align_offsets (n);
+  array<SI> left_extents (n);  // distance from box x1 to alignment point
+  array<SI> right_extents (n); // distance from alignment point to box x2
   for (i= prem_start; i < n; i++) {
-    max_y2= max (max_y2, bs[i]->y2);
-    min_y1= min (min_y1, bs[i]->y1);
+    SI offset= bs[i]->get_leaf_offset ("line_center");
+    if (offset == bs[i]->w ()) {
+      // Default return - not a proof-tree, use geometric center
+      offset= (bs[i]->x1 + bs[i]->x2) >> 1;
+    }
+    align_offsets[i]= offset;
+    left_extents[i] = offset;
+    right_extents[i]= bs[i]->w () - offset;
+    max_y2          = max (max_y2, bs[i]->y2);
+    min_y1          = min (min_y1, bs[i]->y1);
+  }
+
+  // Calculate total premises width based on proper spacing:
+  // Total = left_ext[first] + sum(right_ext[i] + hsep + left_ext[i+1]) +
+  // right_ext[last]
+  SI prem_w= 0;
+  for (i= prem_start; i < n; i++) {
+    if (i == prem_start) {
+      prem_w+= left_extents[i]; // First premise: count left extent
+    }
+    prem_w+= right_extents[i]; // Count right extent
+    if (i < n - 1) {
+      prem_w+= hsep;                // Add spacing between premises
+      prem_w+= left_extents[i + 1]; // Next premise's left extent
+    }
   }
-  if (n > prem_start) prem_w+= (n - prem_start - 1) * hsep;
 
   // Calculate conclusion dimensions
   SI conc_w= bs[conc_idx]->w ();
@@ -839,22 +864,22 @@ proof_tree_box_rep::proof_tree_box_rep (path ip, array<box> bs, font fn2,
   array<SI> pos_x (n);
   array<SI> pos_y (n);
 
-  // Position premises centered on line, spaced by their centers
-  // For proof-tree children, use their line_center as alignment point
-  // For other boxes, use the geometric center (x1+x2)/2
-  SI prem_half= prem_w >> 1;
-  for (SI x= -prem_half, i= prem_start; i < n; i++) {
-    SI half_w= bs[i]->w () >> 1;
-    // Try to get line_center offset for proof-tree children
-    // Default get_leaf_offset returns w(), so if != w(), it's a valid offset
-    SI align_offset= bs[i]->get_leaf_offset ("line_center");
-    if (align_offset == bs[i]->w ()) {
-      // Default return - not a proof-tree, use geometric center
-      align_offset= (bs[i]->x1 + bs[i]->x2) >> 1;
+  // Position premises centered on line, aligned by their line centers
+  // Use pre-calculated align_offsets and extents for proper spacing
+  if (n > prem_start) {
+    SI prem_half= prem_w >> 1;
+    // align_x tracks where the current premise's alignment point should be
+    SI align_x= -prem_half + left_extents[prem_start];
+    for (i= prem_start; i < n; i++) {
+      // Position box so its alignment point is at align_x
+      pos_x[i]= align_x - align_offsets[i];
+      pos_y[i]= prem_baseline;
+      // Advance to next alignment point: current right extent + hsep + next
+      // left extent
+      if (i < n - 1) {
+        align_x+= right_extents[i] + hsep + left_extents[i + 1];
+      }
     }
-    pos_x[i]= x + half_w - align_offset;
-    pos_y[i]= prem_baseline;
-    x+= bs[i]->w () + hsep;
   }
 
   // Position conclusion centered on line (0 point)
diff --git a/src/Typeset/Concat/concat_math.cpp b/src/Typeset/Concat/concat_math.cpp
index 46bd9f9feb..c89da5b0b4 100644
--- a/src/Typeset/Concat/concat_math.cpp
+++ b/src/Typeset/Concat/concat_math.cpp
@@ -612,28 +612,36 @@ concater_rep::typeset_tree (tree t, path ip) {
     typeset_error (t, ip);
     return;
   }
-  int        i, n= N (t);
-  array<box> bs (n);
-  for (i= 0; i < n; i++)
-    bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
-  print (tree_box (ip, bs, env->fn, env->pen));
-}
 
-void
-concater_rep::typeset_proof_tree (tree t, path ip, bool has_label,
-                                  bool label_left) {
-  int min_children= has_label ? 3 : 2;
-  if (N (t) < min_children) {
-    typeset_error (t, ip);
-    return;
+  // Check tree-mode environment variable
+  string mode= as_string (env->read (TREE_MODE));
+
+  if (mode == "proof") {
+    // Proof tree mode: check for label position
+    string label_pos = as_string (env->read (TREE_LABEL_POS));
+    bool   has_label = (label_pos == "left" || label_pos == "right");
+    bool   label_left= (label_pos == "left");
+
+    int min_children= has_label ? 3 : 2;
+    if (N (t) < min_children) {
+      typeset_error (t, ip);
+      return;
+    }
+
+    int        i, n= N (t);
+    array<box> bs (n);
+    for (i= 0; i < n; i++)
+      bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
+    print (proof_tree_box (ip, bs, env->fn, env->pen, has_label, label_left));
+  }
+  else {
+    // Normal tree mode (default)
+    int        i, n= N (t);
+    array<box> bs (n);
+    for (i= 0; i < n; i++)
+      bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
+    print (tree_box (ip, bs, env->fn, env->pen));
   }
-  int        i, n= N (t);
-  array<box> bs (n);
-  // For labeled: t[0] is label, t[1] is conclusion, t[2..n-1] are premises
-  // For unlabeled: t[0] is conclusion, t[1..n-1] are premises
-  for (i= 0; i < n; i++)
-    bs[i]= typeset_as_concat (env, t[i], descend (ip, i));
-  print (proof_tree_box (ip, bs, env->fn, env->pen, has_label, label_left));
 }
 
 void
diff --git a/src/Typeset/Concat/concater.cpp b/src/Typeset/Concat/concater.cpp
index 02fbf83599..bad56a8569 100644
--- a/src/Typeset/Concat/concater.cpp
+++ b/src/Typeset/Concat/concater.cpp
@@ -440,15 +440,6 @@ concater_rep::typeset (tree t, path ip) {
   case TREE:
     typeset_tree (t, ip);
     break;
-  case PROOF_TREE:
-    typeset_proof_tree (t, ip);
-    break;
-  case VAR_PROOF_TREE:
-    typeset_proof_tree (t, ip, true, false);
-    break;
-  case VAR_VAR_PROOF_TREE:
-    typeset_proof_tree (t, ip, true, true);
-    break;
   case SYNTAX:
     typeset_syntax (t, ip);
     break;
diff --git a/src/Typeset/Concat/concater.hpp b/src/Typeset/Concat/concater.hpp
index 818df16ea0..2c8a769169 100644
--- a/src/Typeset/Concat/concater.hpp
+++ b/src/Typeset/Concat/concater.hpp
@@ -91,8 +91,6 @@ class concater_rep {
   void typeset_wide (tree t, path ip, bool above);
   void typeset_neg (tree t, path ip);
   void typeset_tree (tree t, path ip);
-  void typeset_proof_tree (tree t, path ip, bool has_label= false,
-                           bool label_left= false);
   void typeset_wide_table (tree t, path ip);
   void typeset_table (tree t, path ip);
   void print_semantic (box b, tree sem);
diff --git a/src/Typeset/Env/env_default.cpp b/src/Typeset/Env/env_default.cpp
index 04cd67794e..b6a8730d64 100644
--- a/src/Typeset/Env/env_default.cpp
+++ b/src/Typeset/Env/env_default.cpp
@@ -110,6 +110,9 @@ initialize_default_env () {
   env (MATH_BOT_SWELL_START)= "-0.7ex";   // start padding below this level
   env (MATH_BOT_SWELL_END)  = "-2.5ex";   // maximal padding reached here
 
+  env (TREE_MODE)     = "normal"; // tree rendering mode: "normal" or "proof"
+  env (TREE_LABEL_POS)= "none"; // tree label position: "none", "left", "right"
+
   env (PROG_LANGUAGE)   = "scheme";  // the default programming language
   env (PROG_SCRIPTS)    = "none";    // the scripting language
   env (PROG_FONT)       = "roman";   // the font name in prog mode

From 411df1c6f54e28d6bf941e75b7142827373ef51a Mon Sep 17 00:00:00 2001
From: fallensky2077 <mercur1al@outlook.com>
Date: Sun, 21 Dec 2025 15:56:51 +0000
Subject: [PATCH 7/7] use "none" consistently for unlabeled proof-trees

Previously tree-label-pos used "" in document and "none" in code logic.
Now consistently use "none" everywhere for clarity.
---
 TeXmacs/progs/generic/generic-edit.scm   | 16 +++++++---------
 TeXmacs/progs/utils/library/cpp-wrap.scm |  2 +-
 2 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/TeXmacs/progs/generic/generic-edit.scm b/TeXmacs/progs/generic/generic-edit.scm
index 0e41e99377..86eda335a6 100644
--- a/TeXmacs/progs/generic/generic-edit.scm
+++ b/TeXmacs/progs/generic/generic-edit.scm
@@ -789,11 +789,9 @@
 (tm-define (get-proof-tree-label-pos with-t)
   ;; Get the current label position from the with tag
   ;; Returns "none", "right", or "left"
-  ;; Empty string "" is treated as "none" for consistency
   (if (and (>= (tree-arity with-t) 5)
            (tm-equal? (tree-ref with-t 2) "tree-label-pos"))
-      (let ((pos (tm->string (tree-ref with-t 3))))
-        (if (== pos "") "none" pos))
+      (tm->string (tree-ref with-t 3))
       "none"))
 
 ;; Check if t is a tree in proof-tree mode
@@ -841,7 +839,7 @@
 
 (tm-define (proof-tree-set-variant with-t new-pos)
   ;; Set the proof-tree variant by modifying with tag and tree structure
-  ;; All proof-trees have tree-label-pos (either "", "left", or "right")
+  ;; All proof-trees have tree-label-pos (either "none", "left", or "right")
   ;; Tree is always at index 4 in the with tag
   (let* ((current-pos (get-proof-tree-label-pos with-t))
          (tree-t (tree-ref with-t 4)))
@@ -851,10 +849,10 @@
         ((and (== current-pos "none") (!= new-pos "none"))
          (tree-insert! tree-t 0 '(""))
          (tree-set (tree-ref with-t 3) new-pos))
-        ;; From labeled to no label: remove label child, set position to ""
+        ;; From labeled to no label: remove label child, set position to "none"
         ((and (!= current-pos "none") (== new-pos "none"))
          (tree-remove! tree-t 0 1)
-         (tree-set (tree-ref with-t 3) ""))
+         (tree-set (tree-ref with-t 3) "none"))
         ;; Change label side (left <-> right): just change the value
         ((and (!= current-pos "none") (!= new-pos "none"))
          (tree-set (tree-ref with-t 3) new-pos))))))
@@ -1019,18 +1017,18 @@
   (let* ((prem-start (proof-tree-premise-start pt))
          (i (proof-tree-cursor-child-index pt)))
     ;; Insert sub-proof: wrap current premise in a new proof-tree
-    ;; Must explicitly set tree-label-pos to "" to override any inherited value from parent
+    ;; Must explicitly set tree-label-pos to "none" to override any inherited value from parent
     (when (and i (>= i prem-start))
       (let* ((child-t (tree-ref pt i))
              (content (tree->stree child-t)))
         (if downwards?
             ;; Insert down: add empty conclusion below, current stays as premise
             (begin
-              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "" (tree "" ,content)))
+              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "none" (tree "" ,content)))
               (tree-go-to child-t 4 0 0))
             ;; Insert up: wrap current as conclusion of new sub-tree with empty premise above
             (begin
-              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "" (tree ,content "")))
+              (tree-set! child-t `(with "tree-mode" "proof" "tree-label-pos" "none" (tree ,content "")))
               (tree-go-to child-t 4 1 0)))))))
 
 ;; Override structured-insert/remove for proof-tree
diff --git a/TeXmacs/progs/utils/library/cpp-wrap.scm b/TeXmacs/progs/utils/library/cpp-wrap.scm
index c009dbc2cc..f2643b86e7 100644
--- a/TeXmacs/progs/utils/library/cpp-wrap.scm
+++ b/TeXmacs/progs/utils/library/cpp-wrap.scm
@@ -110,7 +110,7 @@
 (tm-define (make-tree) (cpp-make-tree))
 
 (tm-define (make-proof-tree)
-  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "" (tree "" "")) '(4 0 0)))
+  (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "none" (tree "" "")) '(4 0 0)))
 
 (tm-define (make-proof-tree*)
   (insert-go-to '(with "tree-mode" "proof" "tree-label-pos" "right" (tree "" "" "")) '(4 0 0)))