From 22aa194e3b3b6588e14918234bbf0eed3534d18b Mon Sep 17 00:00:00 2001 From: Gennady Uraltsev Date: Mon, 19 Oct 2026 11:38:48 -0500 Subject: [PATCH 1/3] [NNNN] Import \begin{proof}[Title] as a titled proof The importer parsed the optional argument (turning the environment into "proof*") but finalize_layout never emitted a matching begin/end, so the whole proof environment, its title and its markers, was lost and only the body text remained. Emit render-proof with the title as its first argument and close it at the matching \end{proof}. Co-Authored-By: Claude Sonnet 5.5 --- TeXmacs/tests/7003.scm | 67 ++++++++++++++++++++++++++++++++ src/Plugins/Tex/fromtex_post.cpp | 30 ++++++++++++-- 2 files changed, 93 insertions(+), 4 deletions(-) create mode 100644 TeXmacs/tests/7003.scm diff --git a/TeXmacs/tests/7003.scm b/TeXmacs/tests/7003.scm new file mode 100644 index 0000000000..af40971149 --- /dev/null +++ b/TeXmacs/tests/7003.scm @@ -0,0 +1,67 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; 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 . +;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(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}") + ) ;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 + +(define (test-nested) + (with t (import-body + "\\begin{proof}[Outer]a\\begin{proof}b\\end{proof}c\\end{proof}") + (check (contains? t 'render-proof) => #t) + (check (contains? t 'proof) => #t) + ) ;with +) ;define + +(tm-define (test_7003) + (test-titled) + (test-plain) + (test-nested) + (check-report) +) ;tm-define diff --git a/src/Plugins/Tex/fromtex_post.cpp b/src/Plugins/Tex/fromtex_post.cpp index b28f0eb927..fe5639d093 100644 --- a/src/Plugins/Tex/fromtex_post.cpp +++ b/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 titled_proofs; for (i= 0; i < n; i++) { tree v= u[i]; @@ -639,6 +640,27 @@ finalize_layout (tree t) { continue; } + // \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; + } + } + if (is_func (v, BEGIN, 2) && is_enunciation (v) && v[0] != "proof*") { string s= as_string (v[0]); s = s (0, N (s) - 1); From 2f72bb345fc5d33d056aaf6f389693cc2e47d652 Mon Sep 17 00:00:00 2001 From: Gennady Uraltsev Date: Mon, 19 Oct 2026 13:03:23 -0500 Subject: [PATCH 2/3] [NNNN] LaTeX export: write a titled proof as \begin{proof}[Title] render-proof (the tag a titled proof has in Mogan, and what the importer now produces for \begin{proof}[Title]) was exported as a custom proof* environment defined in the preamble, instead of the amsthm proof environment that the untitled proof already uses. Emit \begin{proof}[Title] directly, and a plain \begin{proof} when the title is empty. Tests extended with export and import->export checks. Co-Authored-By: Claude Sonnet 5.5 --- .../latex/progs/latex/convert-latex-tmtex.scm | 10 +++- TeXmacs/tests/7003.scm | 59 +++++++++++++++---- 2 files changed, 57 insertions(+), 12 deletions(-) diff --git a/TeXmacs/plugins/latex/progs/latex/convert-latex-tmtex.scm b/TeXmacs/plugins/latex/progs/latex/convert-latex-tmtex.scm index 60b7f47d82..023d7c2cf0 100644 --- a/TeXmacs/plugins/latex/progs/latex/convert-latex-tmtex.scm +++ b/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) diff --git a/TeXmacs/tests/7003.scm b/TeXmacs/tests/7003.scm index af40971149..1d71240661 100644 --- a/TeXmacs/tests/7003.scm +++ b/TeXmacs/tests/7003.scm @@ -18,13 +18,12 @@ (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}") - ) ;parse-latex-document - ) ;latex->texmacs + (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 @@ -36,7 +35,8 @@ ) ;define (define (test-titled) - (with t (import-body "\\begin{proof}[Proof of Theorem 1]Body.\\end{proof}") + (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) @@ -45,21 +45,58 @@ ) ;define (define (test-plain) - (with t (import-body "\\begin{proof}Body.\\end{proof}") + (with t + (import-body "\\begin{proof}Body.\\end{proof}") (check (contains? t 'proof) => #t) (check (contains? t 'render-proof) => #f) ) ;with ) ;define (define (test-nested) - (with t (import-body - "\\begin{proof}[Outer]a\\begin{proof}b\\end{proof}c\\end{proof}") + (with t + (import-body "\\begin{proof}[Outer]a\\begin{proof}b\\end{proof}c\\end{proof}") (check (contains? t 'render-proof) => #t) (check (contains? t 'proof) => #t) ) ;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) From d1d201eea7daf20e930937592f072d79816dfde1 Mon Sep 17 00:00:00 2001 From: pigmagicfly <2831850183@qq.com> Date: Wed, 21 Oct 2026 15:23:58 +0800 Subject: [PATCH 3/3] [6226] Simplify proof import and strengthen nested tests --- TeXmacs/tests/7003.scm | 21 +++++++++++++++++++-- src/Plugins/Tex/fromtex_post.cpp | 4 +++- 2 files changed, 22 insertions(+), 3 deletions(-) diff --git a/TeXmacs/tests/7003.scm b/TeXmacs/tests/7003.scm index 1d71240661..f38f4448ba 100644 --- a/TeXmacs/tests/7003.scm +++ b/TeXmacs/tests/7003.scm @@ -52,11 +52,28 @@ ) ;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 (contains? t 'render-proof) => #t) - (check (contains? t 'proof) => #t) + (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 diff --git a/src/Plugins/Tex/fromtex_post.cpp b/src/Plugins/Tex/fromtex_post.cpp index fe5639d093..748019cd4f 100644 --- a/src/Plugins/Tex/fromtex_post.cpp +++ b/src/Plugins/Tex/fromtex_post.cpp @@ -661,7 +661,9 @@ finalize_layout (tree t) { } } - if (is_func (v, BEGIN, 2) && is_enunciation (v) && v[0] != "proof*") { + // 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]);