[6226] LaTeX: round-trip \begin{proof}[Title] as a titled proof

TeXmacs/plugins/latex/progs/latex/convert-latex-tmtex.scm

@@ -3722,7 +3722,15 @@
 ) ;define
 
 (define (tmtex-render-proof s l)
-  (list (list '!begin "proof*" (tmtex (car l))) (tmtex (cadr l)))
+  ;; An empty title is what the editor leaves behind after making the title
+  ;; of a proof editable; it means the default heading.
+  (if (== (car l) "")
+    (list (list '!begin "proof") (tmtex (cadr l)))
+    (list
+      (list '!begin "proof" (list '!option (tmtex (car l))))
+      (tmtex (cadr l))
+    ) ;list
+  ) ;if
 ) ;define
 
 (define (tmtex-nbsp s l)

TeXmacs/tests/7003.scm

@@ -0,0 +1,121 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; MODULE      : 7003.scm
+;; DESCRIPTION : LaTeX import of \begin{proof}[Title]
+;; COPYRIGHT   : (C) 2026
+;;
+;; This software falls under the GNU general public license version 3 or later.
+;; It comes WITHOUT ANY WARRANTY WHATSOEVER. For details, see the file LICENSE
+;; in the root directory or <http://www.gnu.org/licenses/gpl-3.0.html>.
+;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(import (liii check))
+
+(check-set-mode! 'report-failed)
+
+(load "./TeXmacs/plugins/latex/progs/init-latex.scm")
+(import-from (latex latex-format))
+
+(define (import-body src)
+  (tree->stree (latex->texmacs (parse-latex-document (string-append "\\documentclass{article}\\begin{document}"
+                                                       src
+                                                       "\\end{document}"
+                                                     ) ;string-append
+                               ) ;parse-latex-document
+               ) ;latex->texmacs
+  ) ;tree->stree
+) ;define
+
+(define (contains? t x)
+  (cond ((== t x) #t)
+        ((pair? t) (or (contains? (car t) x) (contains? (cdr t) x)))
+        (else #f)
+  ) ;cond
+) ;define
+
+(define (test-titled)
+  (with t
+    (import-body "\\begin{proof}[Proof of Theorem 1]Body.\\end{proof}")
+    (check (contains? t 'render-proof) => #t)
+    (check (contains? t "Proof of Theorem 1") => #t)
+    (check (contains? t "Body.") => #t)
+    (check (contains? t 'proof) => #f)
+  ) ;with
+) ;define
+
+(define (test-plain)
+  (with t
+    (import-body "\\begin{proof}Body.\\end{proof}")
+    (check (contains? t 'proof) => #t)
+    (check (contains? t 'render-proof) => #f)
+  ) ;with
+) ;define
+
+;; 断言整棵树而非仅搜索标签：带标题的 proof 由 render-proof 承载标题，
+;; 无标题的保持 proof，两者嵌套时各自闭合到正确的标签上。
+
+(define (test-nested)
+  (with t
+    (import-body "\\begin{proof}[Outer]a\\begin{proof}b\\end{proof}c\\end{proof}")
+    (check t
+      =>
+      '(document (TeXmacs "2.1.4")
+         (style (tuple "article" "std-latex"))
+         (body (document (render-proof "Outer"
+                           (document "a" (proof (document "b")) "c")))))
+    ) ;check
+  ) ;with
+  (with t
+    (import-body "\\begin{proof}a\\begin{proof}[Inner]b\\end{proof}c\\end{proof}")
+    (check t
+      =>
+      '(document (TeXmacs "2.1.4")
+         (style (tuple "article" "std-latex"))
+         (body (document (proof (document "a" (render-proof "Inner" "b") "c")))))
+    ) ;check
+  ) ;with
+) ;define
+
+(define (export-doc stree)
+  (serialize-latex (texmacs->latex (stree->tree stree) '(("texmacs->latex:encoding"
+                                                          . "utf-8")))
+  ) ;serialize-latex
+) ;define
+
+(define (test-export)
+  (with s
+    (export-doc '(document (render-proof "Proof of Theorem 1"
+                             (document "Body."))))
+    (check (string-contains? s "\\begin{proof}[Proof of Theorem 1]") => #t)
+    (check (string-contains? s "\\end{proof}") => #t)
+    (check (string-contains? s "proof*") => #f)
+    (check (string-contains? s "newenvironment") => #f)
+  ) ;with
+  (with s
+    (export-doc '(document (render-proof "" (document "Body."))))
+    (check (string-contains? s "\\begin{proof}") => #t)
+    (check (string-contains? s "[") => #f)
+  ) ;with
+  (with s
+    (export-doc '(document (proof (document "Body."))))
+    (check (string-contains? s "\\begin{proof}") => #t)
+  ) ;with
+) ;define
+
+(define (test-round-trip)
+  (with s
+    (export-doc (import-body "\\begin{proof}[Proof of Theorem 1]Body.\\end{proof}"))
+    (check (string-contains? s "\\begin{proof}[Proof of Theorem 1]") => #t)
+    (check (string-contains? s "proof*") => #f)
+  ) ;with
+) ;define
+
+(tm-define (test_7003)
+  (test-export)
+  (test-round-trip)
+  (test-titled)
+  (test-plain)
+  (test-nested)
+  (check-report)
+) ;tm-define

src/Plugins/Tex/fromtex_post.cpp

@@ -624,10 +624,11 @@ finalize_layout (tree t) {
   for (i= 0; i < n; i++)
     u[i]= finalize_layout (t[i]);
   if (is_func (u, CONCAT)) {
-    string lang     = "code";
-    bool   spc_flag = false;
-    bool   item_flag= false;
-    tree   r (CONCAT);
+    string      lang     = "code";
+    bool        spc_flag = false;
+    bool        item_flag= false;
+    tree        r (CONCAT);
+    array<bool> titled_proofs;
     for (i= 0; i < n; i++) {
       tree v= u[i];
 
@@ -639,7 +640,30 @@ finalize_layout (tree t) {
         continue;
       }
 
-      if (is_func (v, BEGIN, 2) && is_enunciation (v) && v[0] != "proof*") {
+      // \begin{proof}[Title] replaces the "Proof" heading by Title, which is
+      // what render-proof does; a dueto would only append it to "Proof."
+      if (is_func (v, BEGIN, 2) && v[0] == "proof*") {
+        r << tree (BEGIN, "render-proof", v[1]);
+        titled_proofs << true;
+        continue;
+      }
+
+      if (is_func (v, BEGIN, 1) && v[0] == "proof") titled_proofs << false;
+
+      // \end{proof} carries no trace of the optional argument given at
+      // \begin, so remember which open proofs were titled.
+      if (is_func (v, END, 1) && v[0] == "proof" && N (titled_proofs) > 0) {
+        bool titled= titled_proofs[N (titled_proofs) - 1];
+        titled_proofs->resize (N (titled_proofs) - 1);
+        if (titled) {
+          r << tree (END, "render-proof");
+          continue;
+        }
+      }
+
+      // A titled proof was already rewritten to render-proof above; the rest
+      // get the heading kept and the option appended as a dueto.
+      if (is_func (v, BEGIN, 2) && is_enunciation (v)) {
         string s= as_string (v[0]);
         s       = s (0, N (s) - 1);
         r << tree (BEGIN, s) << compound ("dueto", v[1]);