Proof editing with Emacs
Proof editing is how I correct a $\mathrm{\LaTeX}$ manuscript, and how co-authors and I correct each other's: nothing is changed outright, every change is written into the source as a mark—struck text that should go, red text that should come in, a blue note to be settled—so that the author sees each correction in the PDF and accepts or rejects it, one by one or all at once. This page gathers everything I have for it in Emacs: the marks themselves and their $\mathrm{\LaTeX}$ definitions, proof-track-mode to write them while editing, proof.el to settle them, the keys, the $\mathrm{\TeX}$ traps, and how it all started.
Both files live in ~/comp/emacs/lisp/ and are written with the help of Claude. proof.el is at version 1.9, proof-track.el at 1.2 as of 23 October (2026).
The marks
Three kinds of mark, each with several spellings so that the same keys settle a hand-proofread file, a machine-generated diff (the bosoc2.tex kind) and the co-author colours of the third edition of Microcavities:
| Mark | Spellings | Accepted | Rejected |
|---|---|---|---|
| strike-out | \sout{...}, \del{...}, \delmath{...} (a formula or a whole removed equation set in gray, which ulem cannot strike), soul's \st{...}; for Microcavities \delAVK{} \delGM{} \delJJB{}, \delblock{} (whole paragraphs or sections) and \movedout{} (the old place of moved text) | deleted | unwrapped |
| addition | \textcolor{red}{...}, \add{...}, \addsec{...} (a section title added in red); for Microcavities \addAVK{} \addGM{} \addJJB{} (one colour per co-author) and \movedin{} (text moved here) | unwrapped | deleted |
| note | \textcolor{blue}{[Note: ...]}, \note{...} | deleted | deleted |
The lists are proof-strike-cmds, proof-add-cmds and proof-note-cmds in proof.el; adding a spelling there is all it takes for both the writing and the settling side to know it. The definitions my papers carry in their preamble (M-x proof-track-preamble puts them into a document that lacks them):
\usepackage{xcolor}
\usepackage[normalem]{ulem}
\DeclareRobustCommand{\add}[1]{{\color{red}#1}}
\DeclareRobustCommand{\addsec}[1]{{\color{red}#1}}
\DeclareRobustCommand{\del}[1]{{\color{black!55}\csname sout\endcsname{#1}}}
\DeclareRobustCommand{\delmath}[1]{{\color{black!55}#1}}
\DeclareRobustCommand{\note}[1]{{\color{blue}\itshape[#1]}}
\csname sout\endcsname rather than \sout so that accepting every mark of the document cannot eat the definition itself (see version 1°4 below).
Writing marks: proof-track-mode
C-c p t toggles proof-track-mode (" Track" in the mode line): from then on, editing the document body writes the marks instead of making the changes—Emacs' answer to Word's track changes, in plain $\mathrm{\TeX}$:
| I do | Before | After |
|---|---|---|
| type | foo |bar | foo \add{new }bar |
| DEL, C-d, C-w, C-k, M-DEL | foo old bar | foo \del{old} bar |
| select and type, or delete and type | old | \del{old}\add{new} |
| overwrite, query-replace | color | colo\add{u}r, only the characters that differ |
| change a control word | \alpha | \del{\alpha}\add{\beta} |
The marks follow the edit as it goes on. Typing on inside an \add{} adds to it, and a run of DEL (or C-d) grows one \del{old} rather than leaving \del{o}\del{l}\del{d}: touching deletions always coalesce, along the whole chain and across an addition—\del{a}\add{x}\del{b} is \del{ab}\add{x}, as what goes is ab and what comes x. M-x proof-track-merge does the same to the marks already in a file, written by hand or by a script. Text typed in front of or inside a \del{} is put after it, so a replacement always reads deletion-then-addition. Deleting text of an addition really deletes it—it was never the author's—and an \add{} emptied that way disappears; deleting across a \del{} steps over it; a \note{} is free text, edited normally. Undo takes back an edit and its marks in one go.
It keeps the file compiling:
- a deleted brace, control sequence or $ takes its whole construct along: DEL after \cite{x} gives \del{\cite{x}}, never \cite{x\del{}}; a selection that cuts a brace group in two is refused, and the text stays;
- deleted maths—from inside $...$, or holding \begin{equation} or \[—is marked \delmath{};
- a \cite (\citep, \citet[..]…) inside a \del{} is shielded as \mbox{\cite{...}}, which proof.el takes off again when the deletion is rejected;
- a mark never holds a paragraph break, being split around the blank line instead (a deleted paragraph break is simply kept), and never ends inside a % comment, which would comment out its own closing brace;
- leading blanks stay outside an \add{}, as \color eats a space at the start of its argument. In the middle of a sentence the addition takes the blank that follows it instead—" over" typed at jumps| the gives jumps \add{over }the, the same text—so that rejecting it leaves no double space. Before punctuation this cannot be done, and rejecting end \add{x}. leaves end .
Not tracked: the preamble (before \begin{document}), % comments, undo, proof.el's own commands, filling, indenting and commenting out, and any change that only moves blanks about.
Tested on 56 keystroke cases run through Emacs' own command loop, and on a session of edits under AUCTeX whose marked file compiles and whose every mark, rejected, gives back the original text, blank runs aside.
Settling marks: proof.el
proof.el settles the marks one at a time, or all at once, matching braces instead of trusting a regexp, so nested braces, \cite, maths and multi-line arguments all survive:
| Keys | Command | What it does |
|---|---|---|
| C-c p a or Ctrl+◯ | proof-accept-at-point | accept the innermost mark at point, or every mark the selection touches: the struck text goes, the red text stays, the blue note goes |
| C-c p r or Ctrl+✕ | proof-reject-at-point | reject it: the struck text comes back, the red text goes, the blue note goes as well |
| C-c p A | proof-accept-all | accept every mark in the buffer; with C-u first, ask at each one |
| C-c p t | proof-track-mode | write the marks while editing (above) |
| C-c p % | TeX-strip-comments | delete the % comments of the region or buffer (tex-strip-comments.el) |
A mark only partly inside the selection is split, the rest staying marked: rejecting a selection that covers the beginning of a long \sout{...} restores that beginning and leaves the rest struck. A selection boundary falling inside a brace group is refused rather than left unbalanced. Marks nested in one another are settled from the inside out, their bounds following the edits (version 1°8). Marks are only looked for after \begin{document}, where the preamble's own definitions cannot be mistaken for them.
The keys
◯ and ✕ are the round keys of the gaming keyboard, whose bare presses belong to xbindkeys—the AF tag and tex2uni—but whose Ctrl versions fall through to Emacs untouched, where they arrive as C-<XF86Tools> and C-<XF86Forward>. A proofing pass is thus one key for yes and one key for no, a pass one hand can do while the other holds the paper. C-c p is the typed equivalent, and the only free prefix left: C-c C-p belongs to preview-latex, C-c C-a runs the whole compile chain, and my own C-c letters were taken.
The keys sit in proof-marks-mode, a minor mode that proof.el turns on for every .tex, .ltx, .sty, .cls and .dtx file, whatever major mode the buffer ends up in—AUCTeX's, Emacs' built-in latex-mode, or even fundamental-mode when a file-local mode: latex trips AUCTeX's autoloads. They used to be bound on LaTeX-mode-map, which is empty unless AUCTeX claims the buffer (version 1°6).
Two traps met on the way: keymapper treats a held Control as an optional prefix, so a bare-key rule for ◯ there swallowed Ctrl+◯ too until a Control{F13} >> Control{F13} pass-through was written above it; and a running Emacs keeps the proof.el it loaded—M-x load-library RET proof after an update (and proof-track for the writing side).
TeX traps
What the marks themselves cannot do, learnt on real papers—proof-track-mode avoids the first five by itself:
- \add{ word} loses its leading space (\color's look-ahead gobbles it): write iff \add{Eq.} with the space outside.
- The marks are not \long: no blank line inside one. \delmath{} or \add{} around a whole \begin{equation}...\end{equation} works (it is only a colour group; the number is coloured too); $$...$$ inside \del{} does not.
- \sout cannot span a paragraph; \delmath takes anything.
- A multi-key ~\cite{a,b} inside \del{} stops the compile with natbib and hyperref ("Extra }, or forgotten \endgroup"), and only with the real .aux/.bbl: \mbox{\cite{a,b}} cures it, bare braces do not; \mbox{\ref{..}} likewise.
- Accept-all once ate the \sout{#1} of the preamble's \del definition, hence the \csname sout\endcsname spelling above.
- \del{} cannot break a line around a long inline formula (138 pt overfull): split it as \del{text}\delmath{$formula$}\del{text}.
- A \add{} or \note{} nested inside a \del{} becomes one unbreakable box: split the deletion around it.
And two rules of style for marking someone's text by hand: mark only the characters that change—Acknowledg\del{e}ments, not the whole sentence struck and retyped with one letter different—with the reason in a \note{} when the change is invisible at a glance; and before striking a definition, check where else it is used.
How it started
The first version, a [[Blog:Hacks/Emacs_Proofing_LaTeX|hack of 18 May (2024)]], cleaned out the proofing marks of our resubmission of Photon liquefaction in time with two regular expressions:
M-x query-replace-regexp or C-M-%
\\textcolor{red}{\(.*?\)} at first prompt
\1 at second prompt
with \\st{\([\a-z0-9_ C-q C-j]+\)} to remove the strike-outs, the newline entered as C-q C-j. It sorted a fair number of cases, but no regexp can match balanced braces, and a \cite{}, an \emph{} or a formula inside a mark—which is to say, most marks in a physics paper—defeated it. proof.el 1°0 replaced the regexps by brace matching (8 September (2026)), and proof-track.el came to write the marks as well as settle them (23 October (2026)).
Installation
.emacs only has to say:
(add-to-list 'load-path "/home/laussy/comp/emacs/lisp")
(require 'proof)
proof.el installs its own minor mode and keys, and autoloads proof-track.el the first time C-c p t is pressed.
Versions
proof.el:
- 1°0: 8 September (2026) balanced-brace rewrite of the 2024 hack, blue notes.
- 1°1: canonical home in ~/comp/emacs/lisp/ and LaTeX-mode keys.
- 1°2: 9 September (2026) the gaming keys.
- 1°3: 22 September (2026) several spellings per mark—\del{}, \add{}, \note{}, \delmath{}—checked by accepting every mark of a 437-mark generated diff and getting the clean file back.
- 1°4: 24 September (2026) marks are looked for after \begin{document} only: accept-all had eaten the \sout{#1} inside the preamble's own definition of \del, after which struck text printed as nothing at all.
- 1°5: 24 September (2026) \addsec{} counts as an addition.
- 1°6: 26 September (2026) self-installing: the keys live in a minor mode turned on for every $\mathrm{\TeX}$ file, whatever its major mode.
- 1°7: 13 October (2026) the marks of the third edition of Microcavities: \addAVK{} \addGM{} \addJJB{} \movedin{}, \delAVK{} \delGM{} \delJJB{} \delblock{} \movedout{}.
- 1°8: 13 October (2026) nested marks: their bounds are markers that follow the edits made inside them. They used to be positions computed once, so settling an inner mark first left the outer one's end stale, and a \note{} inside an \addsec{} made reject-all swallow the heading of the next section.
- 1°9: 23 October (2026) C-c p t for proof-track-mode; the \mbox{} shielding a cite in a strike-out comes off for \citep, \citet[..]… too, not only for a bare \cite{}.
proof-track.el:
- 1°0: 23 October (2026) typing is written as \add{}, deleting as \del{}.
- 1°1: 23 October (2026) touching deletions always coalesce, along the whole chain and across an addition: \del{a}\del{b} → \del{ab}, \del{a}\add{x}\del{b} → \del{ab}\add{x}; C-d at the start of a mark steps over it and deletes what follows; M-x proof-track-merge for marks already in a file.
- 1°2: 23 October (2026) reloads proof.el when the one in memory predates 1°9: with 1°8 still loaded, every edit stopped on a variable new in 1°9 between writing its mark and merging it, and backspacing over high left \del{h}\del{i}\del{g}\del{h}.
Code
;;; proof.el --- accept or reject \sout{...} / \textcolor{red}{...} proofing marks
;;
;; v°1.0 - balanced-brace rewrite, blue reviewer notes Tue Sep 8 2026
;; v°1.1 - canonical home + LaTeX-mode key bindings Wed Sep 9 2026
;; v°1.2 - accept/reject on the gaming keys Ctrl+◯ Ctrl+✕ Wed Sep 9 2026
;; v°1.3 - several spellings per mark: \del{} \add{} \note{} (the
;; bosoc2.tex / mkbosoc2.py marks) next to \sout{} and
;; \textcolor{red}{}; \delmath{} (gray math in a deletion) is a
;; strike-out too Tue Sep 22 2026
;; v°1.4 - marks are looked for AFTER \begin{document} only: accept-all
;; used to eat the \sout{#1} inside the preamble's own
;; \DeclareRobustCommand{\del}, after which \del{} printed
;; nothing at all Wed Sep 24 2026
;; v°1.5 - \addsec{} (a section title added in red) is an addition too
;; Wed Sep 24 2026
;; v°1.6 - self-installing: the keys now live here, in a minor mode turned
;; on for every .tex/.ltx/.sty/.cls/.dtx file, whatever its major
;; mode. They used to be defined in .emacs on LaTeX-mode-map,
;; which is empty when AUCTeX does not claim the buffer (a
;; file-local "mode: latex", a clash between two AUCTeX
;; installations) and the commands were then unreachable
;; Fri Sep 26 2026
;; v°1.7 - the marks of the 3rd edition of Microcavities (proofmarks.tex):
;; additions \addAVK{} \addGM{} \addJJB{} (one colour per
;; co-author) and \movedin{} (text moved here); strike-outs
;; \delAVK{} \delGM{} \delJJB{}, \delblock{} (whole paragraphs or
;; sections) and \movedout{} (the old place of moved text)
;; Tue Oct 13 2026
;; v°1.8 - nested marks: the bounds of every mark are now Emacs markers, so
;; they follow the edits made to the marks inside them. They used
;; to be buffer positions computed once, before any edit: accepting
;; or rejecting an inner mark first (marks go last to first) left
;; the enclosing mark's end stale, and it then ate, or left behind,
;; as many characters as the inner edit had removed -- e.g. a
;; \note{} inside an \addsec{} stub made reject-all swallow the
;; heading of the section after it Tue Oct 13 2026
;; v°1.9 - C-c p t toggles proof-track-mode (proof-track.el): typing is
;; written as \add{}, deleting as \del{}. The \mbox{} shielding a
;; cite in a strike-out is removed for \citep, \citet... too, with
;; their [..] options, not only for a bare \cite{} Fri Oct 23 2026
;;
;; Balanced-brace version of the recipe in Blog:Hacks/Emacs_Proofing_LaTeX:
;; the argument of a mark is found by brace matching, so nested braces,
;; \cite, math and multi-line arguments are handled.
;;
;; This file lives in ~/comp/emacs/lisp/, which is on the load-path, and
;; .emacs only has to (require 'proof). Everything else is here: opening any
;; .tex, .ltx, .sty, .cls or .dtx file turns on `proof-marks-mode', a minor
;; mode carrying the keys below, so they are there whatever major mode the
;; buffer ends up in -- AUCTeX's LaTeX-mode, the built-in latex-mode, or even
;; fundamental-mode. M-x proof-marks-mode toggles it by hand elsewhere.
;;
;; C-c p a or Ctrl + ◯ proof-accept-at-point
;; C-c p r or Ctrl + ✕ proof-reject-at-point
;; C-c p A proof-accept-all (C-u: ask at each mark)
;; C-c p t proof-track-mode: typing becomes \add{},
;; deleting \del{} (proof-track.el)
;;
;; proof-accept-all accept every mark in the buffer: delete the
;; \sout{...}, keep the text of \textcolor{red}{...},
;; delete the blue \textcolor{blue}{[Note: ...]}
;; C-u proof-accept-all same, asking y/n at each mark
;; proof-reject-at-point restore a \sout{...} (unwrap it) or delete a
;; \textcolor{red}{...}
;; proof-accept-at-point the opposite: delete a \sout{...}, keep the
;; text of a \textcolor{red}{...}
;;
;; The two at-point commands act on the innermost mark at point, or, with an
;; active region, on every mark the region touches. A mark only PARTLY
;; inside the region is split: the part inside is accepted/rejected and the
;; rest stays marked, e.g. rejecting a selection that covers
;; \sout{(e.g., higher male graduate admission at Berkeley
;; out of a longer \sout{...} gives
;; (e.g., higher male graduate admission at Berkeley\sout{, ...rest...}
;; The region boundaries must not fall inside a brace group of the mark
;; (an \emph{...} or a \cite{...}); the command refuses, rather than
;; leaving an unbalanced file. Splitting inside $...$ is not checked.
;;
;; A \cite inside a \sout{...} must be written \mbox{\cite{...}} (ulem and
;; natbib otherwise fail at a page break); the \mbox is removed when the
;; struck text is restored.
;;
;; The three kinds of mark each accept several spellings, listed in
;; `proof-strike-cmds', `proof-add-cmds' and `proof-note-cmds':
;; strike-out \sout{...} \del{...} \delmath{...} (\st{...} for soul)
;; \delAVK{...} \delGM{...} \delJJB{...} \delblock{...} \movedout{...}
;; addition \textcolor{red}{...} \add{...} \addsec{...} (a heading)
;; \addAVK{...} \addGM{...} \addJJB{...} \movedin{...}
;; note \textcolor{blue}{...} \note{...}
;; A split mark is re-wrapped with the spelling it was found with.
(defvar proof-cite-regexp "\\\\cite[a-zA-Z]*\\*?\\(?:\\[[^]]*\\]\\)*{[^}]*}"
"A citation command with its options and keys.")
(defvar proof-strike-cmds '("\\sout{" "\\del{" "\\delmath{" "\\st{"
"\\delAVK{" "\\delGM{" "\\delJJB{"
"\\delblock{" "\\movedout{")
"Strike-out commands, opening brace included.")
(defvar proof-add-cmds '("\\textcolor{red}{" "\\add{" "\\addsec{"
"\\addAVK{" "\\addGM{" "\\addJJB{" "\\movedin{")
"Addition commands, opening brace included.")
(defvar proof-note-cmds '("\\textcolor{blue}{" "\\note{")
"Reviewer-note commands, opening brace included; notes are deleted whether accepted or rejected.")
(defvar proof-syntax-table
(let ((st (make-syntax-table)))
(dolist (c '(?\( ?\) ?\[ ?\] ?\" ?$ ?')) (modify-syntax-entry c "." st))
(modify-syntax-entry ?{ "(}" st)
(modify-syntax-entry ?} "){" st)
(modify-syntax-entry ?\\ "\\" st)
st)
"Syntax table in which only braces pair, so that an unbalanced ( or [ inside
an argument does not derail `forward-sexp'; \\ escapes \\{ and \\}.")
(defun proof--close (open)
"Position just after the brace matching the one at OPEN."
(save-excursion
(with-syntax-table proof-syntax-table
(goto-char open) (forward-sexp) (point))))
(defun proof--body-start ()
"Position after \\begin{document}, or the start of the buffer if there is
none: the preamble defines the marks and must never be edited as one."
(save-excursion
(goto-char (point-min))
(if (re-search-forward "\\\\begin{document}" nil t) (point) (point-min))))
(defun proof--marks (cmd &optional beg end)
"Bounds (BEG OPEN CLOSE) of every CMD mark in the buffer, or, with BEG and
END, of every mark overlapping [BEG, END). BEG is the start of the command,
OPEN the position of its `{', CLOSE the position after the matching `}'."
(save-excursion
(let ((re (regexp-quote cmd)) out)
(goto-char (proof--body-start))
(while (re-search-forward re nil t)
(let* ((b (match-beginning 0)) (open (1- (point))) (close (proof--close open)))
(when (or (not beg) (and (< b end) (> close beg)))
(push (list b open close) out))
(goto-char (1+ open))))
(nreverse out))))
(defun proof--depth (from to)
"Brace depth at TO relative to FROM, escaped braces ignored."
(save-excursion
(let ((d 0))
(goto-char from)
(while (re-search-forward "\\\\.\\|[{}]" to t)
(let ((m (match-string 0)))
(cond ((string= m "{") (setq d (1+ d)))
((string= m "}") (setq d (1- d))))))
d)))
(defun proof--unbox-string (str)
"STR with the \\mbox{} that shields a \\cite inside a strike-out removed."
(replace-regexp-in-string (concat "\\\\mbox{\\(" proof-cite-regexp "\\)}") "\\1" str t))
(defun proof--unbox (from to)
"Same as `proof--unbox-string' on the buffer text between FROM and TO."
(save-excursion
(goto-char from)
(while (re-search-forward (concat "\\\\mbox{\\(" proof-cite-regexp "\\)}") to t)
(replace-match "\\1" t))))
(defun proof--edit (bounds cmd mode beg end)
"Apply MODE (`keep' = unwrap, `drop' = delete) to the part of the CMD mark
BOUNDS that lies in [BEG, END); whatever lies outside stays marked."
(let* ((b (nth 0 bounds)) (open (nth 1 bounds)) (close (nth 2 bounds))
(t0 (1+ open)) (t1 (1- close))
(lo (max beg t0)) (hi (min end t1)))
(if (and (<= beg b) (>= end close))
(progn ; the whole mark
(delete-region (1- close) close)
(delete-region b t0)
(if (eq mode 'drop)
(delete-region b (- t1 (- t0 b)))
(proof--unbox b (- t1 (- t0 b)))))
(unless (and (zerop (proof--depth t0 lo)) (zerop (proof--depth t0 hi)))
(user-error "A selection boundary falls inside a brace group of the mark"))
(let ((a (buffer-substring t0 lo)) (mid (buffer-substring lo hi))
(c (buffer-substring hi t1)) (out ""))
(unless (string= a "") (setq out (concat cmd a "}")))
(when (eq mode 'keep) (setq out (concat out (proof--unbox-string mid))))
(unless (string= c "") (setq out (concat out cmd c "}")))
(delete-region b close)
(goto-char b)
(insert out)))))
(defun proof--all-marks (specs &optional beg end)
"For SPECS, a list of (CMDS . MODE), the (CMD MODE BOUNDS) of every mark of
any spelling in CMDS, in the buffer or overlapping [BEG, END)."
(let (out)
(dolist (spec specs)
(dolist (cmd (car spec))
(dolist (m (proof--marks cmd beg end))
(push (list cmd (cdr spec) m) out))))
(nreverse out)))
(defun proof--markerize (m)
"M, a (CMD MODE BOUNDS) mark, with its BOUNDS turned into markers, so that
they follow the edits made inside the mark before it is itself processed."
(list (nth 0 m) (nth 1 m) (mapcar #'copy-marker (nth 2 m))))
(defun proof--positions (bounds)
"The positions of the markers BOUNDS."
(mapcar #'marker-position bounds))
(defun proof--unmarker (m)
"Free the markers of the mark M."
(dolist (x (nth 2 m)) (set-marker x nil)))
(defun proof--apply (strike-mode add-mode)
"Apply STRIKE-MODE to strike-outs and ADD-MODE to additions (`keep' or
`drop'): every mark touched by the active region, else the innermost mark
at point. Marks are processed from the last to the first."
(let* ((region (use-region-p))
(beg (if region (region-beginning) (point)))
(end (if region (region-end) (point)))
(end* (if region end (1+ end)))
(marks (proof--all-marks
(list (cons proof-strike-cmds strike-mode)
(cons proof-add-cmds add-mode)
(cons proof-note-cmds 'drop))
beg end*)))
(unless marks (user-error "No proofing mark here"))
(setq marks (sort marks (lambda (x y) (> (car (nth 2 x)) (car (nth 2 y))))))
(if region
(let ((marks (mapcar #'proof--markerize marks))
(end (copy-marker end)))
(dolist (m marks)
(proof--edit (proof--positions (nth 2 m)) (nth 0 m) (nth 1 m) beg end))
(mapc #'proof--unmarker marks)
(set-marker end nil)
(deactivate-mark)
(message "%d marks processed" (length marks)))
(let ((m (car marks))) ; innermost = latest start
(proof--edit (nth 2 m) (nth 0 m) (nth 1 m) (point-min) (point-max))))))
(defun proof-accept-at-point ()
"Accept the mark at point, or every mark the region touches: delete the
strike-outs, keep the text of the additions. A mark only partly inside the
region is split, the rest staying marked."
(interactive)
(proof--apply 'drop 'keep))
(defun proof-reject-at-point ()
"Reject the mark at point, or every mark the region touches: restore the
strike-outs (unwrap them), delete the additions. A mark only partly inside
the region is split, the rest staying marked."
(interactive)
(proof--apply 'keep 'drop))
(defun proof-accept-all (&optional ask)
"Accept every proofing mark in the buffer; with prefix ASK, confirm each."
(interactive "P")
(let ((n 0)
(marks (proof--all-marks
(list (cons proof-strike-cmds 'drop) (cons proof-add-cmds 'keep)
(cons proof-note-cmds 'drop)))))
(setq marks (mapcar #'proof--markerize
(sort marks (lambda (x y) (> (car (nth 2 x)) (car (nth 2 y)))))))
(dolist (m marks)
(let* ((bounds (proof--positions (nth 2 m))) (b (car bounds)))
(when (or (not ask)
(progn (goto-char b) (y-or-n-p (format "Accept mark at %d? " b))))
(proof--edit bounds (nth 0 m) (nth 1 m) (point-min) (point-max))
(setq n (1+ n)))))
(mapc #'proof--unmarker marks)
(message "%d marks accepted" n)))
;;; Making the commands reachable ------------------------------------------
;;
;; The keys used to be bound in .emacs on `LaTeX-mode-map', which exists only
;; once AUCTeX's latex.el is loaded and is consulted only if the buffer is in
;; `LaTeX-mode'. A .tex file that lands in the built-in `latex-mode', or in
;; `fundamental-mode' because the AUCTeX autoloads are broken, then has no
;; proofing keys at all. A minor mode installed from `find-file-hook' on the
;; file name is immune to all of this: its map takes precedence over whatever
;; the major mode provides.
(defvar proof-marks-mode-map
(let ((map (make-sparse-keymap)))
(define-key map (kbd "C-c p a") #'proof-accept-at-point)
(define-key map (kbd "C-c p r") #'proof-reject-at-point)
(define-key map (kbd "C-c p A") #'proof-accept-all)
(define-key map (kbd "C-c p t") #'proof-track-mode)
;; the gaming keyboard: Ctrl + ◯ accepts, Ctrl + ✕ rejects. xbindkeys
;; holds those two keys bare only (m:0x0), so the Ctrl forms reach Emacs.
(define-key map (kbd "C-<XF86Tools>") #'proof-accept-at-point) ; ◯
(define-key map (kbd "C-<XF86Forward>") #'proof-reject-at-point) ; ✕
map)
"Keymap of `proof-marks-mode'.")
(autoload 'proof-track-mode "proof-track"
"Track changes as \\add{} / \\del{} proofing marks." t)
;;;###autoload
(define-minor-mode proof-marks-mode
"Minor mode giving the keys that accept or reject \\del{}/\\add{}/\\note{}
proofing marks. See the commentary at the top of proof.el."
:lighter " Proof"
:keymap proof-marks-mode-map)
(defvar proof-file-regexp "\\.\\(tex\\|ltx\\|sty\\|cls\\|dtx\\)\\'"
"File names on which `proof-marks-mode' turns itself on.")
;;;###autoload
(defun proof-marks-maybe-enable ()
"Turn `proof-marks-mode' on if the buffer visits a TeX file."
(when (and buffer-file-name
(string-match-p proof-file-regexp buffer-file-name))
(proof-marks-mode 1)))
;;;###autoload
(add-hook 'find-file-hook #'proof-marks-maybe-enable)
;; and for TeX buffers that do not visit a file, or whose major mode is set
;; after the file is found (AUCTeX reparsing, a file-local "mode:" line).
(dolist (hook '(tex-mode-hook latex-mode-hook plain-tex-mode-hook
LaTeX-mode-hook TeX-mode-hook plain-TeX-mode-hook
docTeX-mode-hook))
(add-hook hook #'proof-marks-mode))
(provide 'proof)
;;; proof-track.el --- track changes in a .tex as \add{...} / \del{...} proof marks
;;
;; v°1.0 - typing is wrapped in \add{}, deleting in \del{} Fri Oct 23 2026
;; v°1.1 - touching deletions always coalesce, along the whole chain and
;; across an addition: \del{a}\del{b} -> \del{ab},
;; \del{a}\add{x}\del{b} -> \del{ab}\add{x}; C-d at the start of a
;; mark steps over it and deletes what follows; M-x
;; proof-track-merge does the same to marks already in a file
;; Fri Oct 23 2026
;; v°1.2 - reloads proof.el if the one in memory predates 1.9: with v1.8
;; still loaded, every edit stopped on the missing
;; `proof-cite-regexp' between writing its mark and merging it,
;; and backspacing over "high" left \del{h}\del{i}\del{g}\del{h}
;; Fri Oct 23 2026
;;
;; The writing side of proof.el: with `proof-track-mode' on (C-c p t), every
;; edit of the document body becomes a proofing mark instead of a change, so
;; that the author accepts or rejects it afterwards with proof.el's keys
;; (Ctrl+◯ / Ctrl+✕, C-c p a / C-c p r / C-c p A).
;;
;; typing foo bar -> foo \add{new }bar
;; DEL, C-d, C-w, C-k foo old bar -> foo \del{old} bar
;; overwrite, replace colour -> colo\add{u}r -- only the
;; characters that differ are marked
;; select + type old -> \del{old}\add{new}
;;
;; The marks follow the edit as it goes on: typing on inside an \add{} just
;; adds to it, and a run of DEL (or C-d) grows one \del{} rather than leaving
;; \del{d}\del{l}\del{o}: touching deletions always coalesce, also across
;; an addition -- \del{a}\add{x}\del{b} is \del{ab}\add{x}, and
;; M-x proof-track-merge does it to the marks already in a file. Text typed right before or inside a \del{} is put
;; after it, so a replacement reads \del{old}\add{new}. Deleting text of an
;; \add{} really deletes it (it was never the author's), an \add{} emptied that
;; way disappears, and deleting across a \del{} just steps over it. Text in a
;; \note{} is free text, edited normally.
;;
;; TeX is kept compilable:
;; - a deleted brace, control sequence or $ takes its whole construct with
;; it: DEL after \cite{x} gives \del{\cite{x}}, never \cite{x\del{}};
;; a region that cuts a brace group in two is refused (the text stays);
;; - an edit that cuts into a control word marks the whole word:
;; \alpha -> \beta gives \del{\alpha}\add{\beta};
;; - a mark never holds a paragraph break (\add and \del are not \long):
;; it is split around the blank line, and a deleted paragraph break is
;; simply kept;
;; - a mark never ends in a % comment (it would comment out its own brace):
;; comments are not proof material and are edited normally;
;; - deleted maths ($...$ from inside, \begin{equation}, \[ ) is struck as
;; \delmath{}, the grey no-strike mark, since ulem's \sout can't take it;
;; - a \cite in a \del{} is shielded as \mbox{\cite{..}} (ulem + natbib),
;; which proof.el removes again when the deletion is rejected;
;; - leading blanks stay outside an \add{}: {\color{red}#1} eats a space
;; at the start of its argument;
;; - the preamble (before \begin{document}) is never tracked.
;;
;; Not tracked either: changes made by undo, by proof.el's own accept/reject
;; commands, by filling, indenting and commenting, and changes that only
;; move blanks around (refilling). Undo takes back the edit and its marks in
;; one go. `proof-track-preamble' puts the definitions of the marks into a
;; document that lacks them.
(require 'proof)
(require 'seq)
;; An Emacs that loaded an older proof.el keeps it -- `require' does not
;; reload -- and proof-track then fails at every keystroke on what is new in
;; proof.el 1.9, after writing the mark but before merging it. Reload it.
(unless (boundp 'proof-cite-regexp) (load "proof" nil t))
(defvar proof-track-mode)
(defvar proof-track-add "\\add{" "Mark wrapped around inserted text.")
(defvar proof-track-del "\\del{" "Mark wrapped around deleted text.")
(defvar proof-track-delmath "\\delmath{"
"Mark wrapped around deleted maths, which ulem's \\sout cannot strike.")
(defvar proof-track-edit-commands
'(self-insert-command newline open-line TeX-newline electric-newline-and-maybe-indent
delete-char delete-forward-char delete-backward-char backward-delete-char
backward-delete-char-untabify kill-region kill-word backward-kill-word
kill-line kill-whole-line kill-sentence backward-kill-sentence kill-sexp
backward-kill-sexp zap-to-char zap-up-to-char clipboard-kill-region
yank yank-pop clipboard-yank mouse-yank-primary)
"Commands whose changes are tracked even when they only add or remove blanks.
Blanks moved by anything else -- filling, indenting -- are no edit.")
(defvar proof-track-ignore-commands
'(undo undo-only undo-redo undo-tree-undo undo-tree-redo revert-buffer
fill-paragraph fill-region fill-region-as-paragraph LaTeX-fill-paragraph
LaTeX-fill-region LaTeX-fill-environment LaTeX-fill-section
indent-region indent-for-tab-command indent-rigidly LaTeX-indent-line
comment-region uncomment-region comment-dwim comment-line
TeX-comment-or-uncomment-region TeX-comment-or-uncomment-paragraph
TeX-strip-comments proofread-my-latex)
"Commands whose changes are never tracked. So are all the proof-* commands.")
(defvar proof-track-comment-table
(let ((st (copy-syntax-table proof-syntax-table)))
(modify-syntax-entry ?% "<" st)
(modify-syntax-entry ?\n ">" st)
st)
"`proof-syntax-table' with % comments, to tell what is commented out.")
(defvar-local proof-track--before nil
"(BEG END TEXT POINT) recorded by `before-change-functions'.")
(defvar-local proof-track--cmd-point nil
"Point when the current command started: it tells DEL from C-d, and
where a refused edit puts point back. The point seen by the change hooks
will not do: `kill-region' moves it before deleting.")
(defvar-local proof-track--blank nil
"(BEG . END) markers of the last blanks typed outside any mark, which
`proof-track--wrap' may fold into the addition typed right after them.")
(defvar-local proof-track--goto nil
"Marker where point goes once the command is over: a command may restore
point after its edit (`kill-region' does), undoing where the hook put it.")
;;; Reading the marks ---------------------------------------------------------
(defun proof-track--escaped-p (pos)
"Non-nil if the character at POS is escaped by an odd run of backslashes."
(save-excursion
(goto-char pos)
(= 1 (% (- (skip-chars-backward "\\\\")) 2))))
(defun proof-track--para-start (pos)
"Start of the paragraph holding POS: no mark spans a blank line."
(save-excursion
(goto-char pos)
(if (re-search-backward "\n[ \t]*\n" nil t) (match-end 0) (point-min))))
(defun proof-track--in-comment (pos)
"Start of the % comment POS is in, or nil."
(save-excursion
(goto-char pos)
(with-syntax-table proof-track-comment-table
(let ((s (parse-partial-sexp (line-beginning-position) pos)))
(and (nth 4 s) (nth 8 s))))))
(defun proof-track--cmd-at-open (open cmds)
"The member of CMDS whose `{' is the brace at OPEN, or nil."
(seq-find (lambda (cmd)
(let ((b (- open (1- (length cmd)))))
(and (>= b (point-min))
(string= (buffer-substring-no-properties b (1+ open)) cmd))))
cmds))
(defun proof-track--mark-at-open (open)
"The mark whose `{' is at OPEN, as (KIND CMD BEG OPEN CLOSE), KIND being
`add', `del' or `note', BEG the start of CMD, CLOSE the position after the
matching `}' (nil if there is none); nil if OPEN opens no mark."
(when (eq (char-after open) ?{)
(let ((kind nil) (cmd nil))
(cond ((setq cmd (proof-track--cmd-at-open open proof-add-cmds)) (setq kind 'add))
((setq cmd (proof-track--cmd-at-open open proof-strike-cmds)) (setq kind 'del))
((setq cmd (proof-track--cmd-at-open open proof-note-cmds)) (setq kind 'note)))
(when kind
(list kind cmd (- open (1- (length cmd))) open
(condition-case nil (proof--close open) (scan-error nil)))))))
(defun proof-track--enclosing (pos)
"The innermost mark whose argument holds POS, or nil."
(let ((opens (with-syntax-table proof-syntax-table
(nth 9 (parse-partial-sexp (proof-track--para-start pos) pos)))))
(seq-some #'proof-track--mark-at-open (reverse opens))))
(defun proof-track--mark-ending-at (pos)
"The mark whose closing `}' is just before POS, or nil."
(when (and (> pos (point-min)) (eq (char-before pos) ?})
(not (proof-track--escaped-p (1- pos))))
(let ((open (save-excursion
(with-syntax-table proof-syntax-table
(goto-char pos)
(condition-case nil (progn (backward-sexp) (point)) (scan-error nil))))))
(and open (proof-track--mark-at-open open)))))
(defun proof-track--mark-starting-at (pos)
"The mark whose command starts at POS, or nil."
(save-excursion
(goto-char pos)
(when (looking-at (regexp-opt (append proof-add-cmds proof-strike-cmds proof-note-cmds)))
(proof-track--mark-at-open (1- (match-end 0))))))
(defun proof-track--own-p (m kind)
"Non-nil if M is a KIND mark with the spelling proof-track itself writes."
(and m (eq (car m) kind) (nth 4 m)
(member (nth 1 m) (if (eq kind 'add) (list proof-track-add)
(list proof-track-del proof-track-delmath)))))
(defun proof-track--balanced-string-p (s)
"Non-nil if the braces of S balance (escaped braces and comments aside)."
(with-temp-buffer
(insert s)
(with-syntax-table proof-track-comment-table
(let ((st (parse-partial-sexp (point-min) (point-max))))
(and (zerop (nth 0 st)) (>= (nth 6 st) 0))))))
(defun proof-track--lone-closer-p (s)
"Non-nil if S closes a brace it does not open."
(with-temp-buffer
(insert s)
(with-syntax-table proof-track-comment-table
(< (nth 6 (parse-partial-sexp (point-min) (point-max))) 0))))
(defun proof-track--blank-p (s)
(string-match-p "\\`[ \t\n]*\\'" s))
;;; Keeping the marks valid TeX ------------------------------------------------
(defun proof-track--split (m pt)
"Split the mark M around the blank lines of its argument, which a mark
cannot hold, uncomment its closing brace and drop the empty pieces. Only
marks of proof-track's own spellings are touched. Return where PT goes."
(let ((ptm (copy-marker pt)))
(when (and m (nth 4 m)
(member (nth 1 m) (list proof-track-add proof-track-del proof-track-delmath)))
(let* ((cmd (nth 1 m)) (open (nth 3 m)) (close (nth 4 m))
(bm (copy-marker (nth 2 m))) (em (copy-marker close t))
(c (proof-track--in-comment (1- close))) cuts)
;; a % typed in the argument comments out its brace: close before it
(when (and c (> c open))
(goto-char (1- close)) (delete-char 1)
(goto-char c) (insert "}")
(setq close (1+ c)))
(save-excursion
(goto-char (1+ open))
(while (re-search-forward "\n[ \t]*\n" (1- close) t)
(when (zerop (proof--depth (1+ open) (match-beginning 0)))
(push (cons (match-beginning 0) (match-end 0)) cuts))))
(dolist (cut cuts) ; the last one first
(goto-char (cdr cut)) (insert cmd)
(goto-char (car cut)) (insert "}"))
(goto-char bm) ; drop the empty pieces
(let ((empty (concat cmd "}")))
(while (search-forward empty em t)
(delete-region (match-beginning 0) (match-end 0))))
(set-marker bm nil) (set-marker em nil)))
(prog1 (marker-position ptm) (set-marker ptm nil))))
(defun proof-track--coalesce (d)
"Join the own deletion D with the deletions it touches, along the whole
chain and across an addition: \\del{a}\\del{b} -> \\del{ab}, and
\\del{a}\\add{x}\\del{b} -> \\del{ab}\\add{x}: what goes is a+b, what
comes x. A deletion after an addition moves before it, so that a mark
always reads deletion-then-addition. Return the resulting mark."
(let ((go t))
(while go
(let* ((cmd (nth 1 d))
(prev (proof-track--mark-ending-at (nth 2 d)))
(next (proof-track--mark-starting-at (nth 4 d))))
(cond
((and (proof-track--own-p prev 'del) (equal (nth 1 prev) cmd))
(delete-region (1- (nth 2 d)) (1+ (nth 3 d))) ; the "}\\del{" joint
(setq d (proof-track--mark-at-open (nth 3 prev))))
((and (proof-track--own-p next 'del) (equal (nth 1 next) cmd))
(delete-region (1- (nth 4 d)) (1+ (nth 3 next)))
(setq d (proof-track--mark-at-open (nth 3 d))))
((proof-track--own-p prev 'add) ; \\add{x}\\del{b}
(let ((text (buffer-substring (nth 2 d) (nth 4 d))))
(delete-region (nth 2 d) (nth 4 d))
(goto-char (nth 2 prev))
(insert text)
(setq d (proof-track--mark-at-open (+ (nth 2 prev) (length cmd) -1)))))
(t (setq go nil))))))
(proof-track--split d (nth 2 d))
d)
(defun proof-track--merge (from to)
"Coalesce every deletion of our own spelling between FROM and TO with
its neighbours; see `proof-track--coalesce'."
(let ((starts nil) (to (copy-marker to t)))
(save-excursion
(goto-char (max (point-min) (1- from)))
(while (re-search-forward (regexp-opt (list proof-track-del proof-track-delmath)) to t)
(push (copy-marker (match-beginning 0)) starts)))
(dolist (m (nreverse starts))
(let ((d (proof-track--mark-starting-at m)))
(when (proof-track--own-p d 'del) (proof-track--coalesce d)))
(set-marker m nil))
(set-marker to nil)))
;;;###autoload
(defun proof-track-merge (&optional beg end)
"Coalesce the touching deletions of the region, or of the whole document
body: \\del{a}\\del{b} -> \\del{ab}, \\del{a}\\add{x}\\del{b} ->
\\del{ab}\\add{x}. For marks written by hand or by an older version."
(interactive (if (use-region-p) (list (region-beginning) (region-end))))
(save-excursion
(proof-track--merge (or beg (proof--body-start)) (or end (point-max)))))
(defun proof-track--shield-cites (from to)
"Wrap each bare \\cite{...} (\\citep, \\citet[..]...) between FROM and
TO in \\mbox{}, which ulem needs and proof.el removes on rejection."
(save-excursion
(let ((to (copy-marker to t)))
(goto-char from)
(while (re-search-forward proof-cite-regexp to t)
(let ((b (match-beginning 0)) (e (match-end 0)))
(unless (save-excursion (goto-char b) (looking-back "\\\\mbox{" (max (point-min) (- b 6))))
(goto-char e) (insert "}")
(goto-char b) (insert "\\mbox{")
(goto-char (+ e 7)))))
(set-marker to nil))))
;;; Insertions ---------------------------------------------------------------
(defun proof-track--insert (beg end)
"Mark the text just inserted between BEG and END as an addition.
Return the position just after it, where point goes when typing."
(let ((m (proof-track--enclosing beg)) d)
(cond
((and m (eq (car m) 'add)) (proof-track--split m end))
((and m (eq (car m) 'note)) end)
((and m (nth 4 m)) ; typed into struck text: after it
(proof-track--move beg end (nth 4 m)))
((and (setq d (proof-track--mark-starting-at end)) (eq (car d) 'del) (nth 4 d))
(proof-track--move beg end (nth 4 d))) ; typed just before it: same
(t (proof-track--wrap beg end)))))
(defun proof-track--move (beg end to)
"Move the text between BEG and END to TO, after it, and mark it there."
(let ((text (buffer-substring beg end)) (n (- end beg)))
(delete-region beg end)
(goto-char (- to n))
(insert text)
(proof-track--insert (- to n) (point))))
(defun proof-track--wrap (beg end)
"Wrap the inserted text between BEG and END, outside any mark, in an
addition -- or glue it to the addition it touches."
(let ((text (buffer-substring beg end))
(prev (proof-track--mark-ending-at beg))
(next (proof-track--mark-starting-at end)))
(cond
((proof-track--own-p prev 'add) ; right after \add{...}: extend it
(delete-region beg end)
(goto-char (1- beg)) (insert text)
(proof-track--split (proof-track--mark-at-open (nth 3 prev)) (point)))
((and (proof-track--own-p next 'add) ; right before \add{...}: prepend
(not (string-match-p "\\`[ \t\n]" text)))
(delete-region beg end)
(goto-char (- (1+ (nth 3 next)) (length text))) (insert text)
(proof-track--split (proof-track--mark-at-open (- (nth 3 next) (length text))) (point)))
((proof-track--blank-p text) ; blanks alone are no material, yet
(setq proof-track--blank (cons (copy-marker beg) (copy-marker end)))
end)
((proof-track--lone-closer-p text)
(message "proof-track: a lone `}' is not marked") end)
(t
;; Leading blanks stay outside: \color eats a space at the start of its
;; argument. But " new" typed at "a| b" is "new " typed at "a |b":
;; the addition then takes the blank that follows it instead, so that
;; rejecting it leaves no double space.
(let* ((lead (progn (string-match "\\`[ \t\n]*" text) (match-string 0 text)))
(s (+ beg (length lead)))
(typed (and (string= lead "") proof-track--blank
(= (cdr proof-track--blank) beg)
(buffer-substring-no-properties (car proof-track--blank) beg)))
(lead (if (and typed (proof-track--blank-p typed)) typed lead))
(e (if (and (not (string= lead ""))
(<= (+ end (length lead)) (point-max))
(string= lead (buffer-substring-no-properties end (+ end (length lead)))))
(+ end (length lead))
end)))
(goto-char e) (insert "}")
(goto-char s) (insert proof-track-add)
(proof-track--split (proof-track--mark-at-open (1- (point)))
(+ end (length proof-track-add))))))))
;;; Deletions ----------------------------------------------------------------
(defun proof-track--kill-before (q)
(if (> q (point-min)) (proof-track--kill-char (1- q) t) q))
(defun proof-track--kill-after (q)
(if (< q (point-max)) (proof-track--kill-char q nil) q))
(defun proof-track--group-atom (p)
"Bounds (B . E) of the construct whose brace is at P: the group, the
groups glued to it and the control word heading them, as \\frac{a}{b}."
(save-excursion
(with-syntax-table proof-syntax-table
(condition-case nil
(let (b e)
(if (eq (char-after p) ?{)
(setq b p e (proof--close p))
(goto-char (1+ p)) (backward-sexp) (setq b (point) e (1+ p)))
(goto-char e)
(while (eq (char-after) ?{) (forward-sexp) (setq e (point)))
(goto-char b)
(while (and (eq (char-before) ?}) (not (proof-track--escaped-p (1- (point)))))
(backward-sexp) (setq b (point)))
(when (and (looking-back "\\\\[a-zA-Z@]+\\*?" (line-beginning-position) t)
(not (proof-track--escaped-p (match-beginning 0))))
(setq b (match-beginning 0)))
(cons b e))
(scan-error nil)))))
(defun proof-track--cs-atom (p)
"If the character at P belongs to a control sequence, its bounds (B . E)
together with the brace groups that follow it; else nil."
(save-excursion
(let ((c (char-after p)) b)
(cond
((and (eq c ?\\) (not (proof-track--escaped-p p))) (setq b p))
((and (> p (point-min)) (eq (char-before p) ?\\) (not (proof-track--escaped-p (1- p))))
(setq b (1- p)))
((and c (string-match-p "[a-zA-Z@]" (string c)))
(goto-char p) (skip-chars-backward "a-zA-Z@")
(when (and (eq (char-before) ?\\) (not (proof-track--escaped-p (1- (point)))))
(setq b (1- (point))))))
(when b
(goto-char (1+ b))
(if (zerop (skip-chars-forward "a-zA-Z@"))
(forward-char 1) ; a control symbol, \% or \\
(skip-chars-forward "*"))
(with-syntax-table proof-syntax-table
(condition-case nil
(while (eq (char-after) ?{) (forward-sexp))
(scan-error nil)))
(cons b (point))))))
(defun proof-track--math-atom (p)
"Bounds of the $...$ whose dollar sign is at P, or nil."
(save-excursion
(let ((start (proof-track--para-start p))
(stop (progn (goto-char p)
(if (re-search-forward "\n[ \t]*\n" nil t) (point) (point-max))))
dollars)
(goto-char start)
(while (search-forward "$" stop t)
(unless (proof-track--escaped-p (1- (point))) (push (1- (point)) dollars)))
(setq dollars (nreverse dollars))
(let* ((i (seq-position dollars p))
(j (and i (if (zerop (% i 2)) (1+ i) (1- i))))
(q (and j (>= j 0) (nth j dollars))))
(and q (cons (min p q) (1+ (max p q))))))))
(defun proof-track--kill-char (p backward)
"Mark the deletion of the character at P, BACKWARD meaning by DEL.
A brace, control sequence or $ takes its whole construct along, and the
braces of a mark are stepped over. Return where point goes, or nil."
(let ((c (char-after p)) m a)
(cond
((and (eq c ?}) (not (proof-track--escaped-p p))
(setq m (proof-track--mark-ending-at (1+ p))))
(cond ((and backward (eq (car m) 'add) (> p (1+ (nth 3 m))))
(proof-track--kill-char (1- p) t)) ; the last letter of the addition
(backward (proof-track--kill-before (nth 2 m)))
(t (proof-track--kill-after (1+ p)))))
((and (eq c ?{) (setq m (proof-track--mark-at-open p)))
(cond (backward (proof-track--kill-before (nth 2 m)))
((eq (car m) 'add) (proof-track--kill-after (1+ p)))
(t (proof-track--kill-after (nth 4 m)))))
((setq m (proof-track--mark-starting-at p)) ; C-d at a mark: step over it
(cond (backward (proof-track--kill-before p))
((eq (car m) 'add) (proof-track--kill-after (1+ (nth 3 m))))
(t (proof-track--kill-after (or (nth 4 m) (1+ p))))))
((and (memq c '(?{ ?})) (not (proof-track--escaped-p p)))
(if (setq a (proof-track--group-atom p))
(proof-track--kill-region (car a) (cdr a) backward)
(message "proof-track: unbalanced brace, not deleted") nil))
((setq a (proof-track--cs-atom p))
(proof-track--kill-region (car a) (cdr a) backward))
((and (eq c ?$) (not (proof-track--escaped-p p)))
(if (setq a (proof-track--math-atom p))
(proof-track--kill-region (car a) (cdr a) backward)
(message "proof-track: unmatched $, not deleted") nil))
(t (proof-track--kill-region p (1+ p) backward)))))
(defun proof-track--kill-region (beg end backward)
"Mark the deletion of the text between BEG and END. Return where point
goes (before the marks if BACKWARD, after them otherwise), or nil if the
deletion is refused, the text then staying as it is."
(let ((c (proof-track--in-comment end)))
(when (and c (> c beg)) ; the commented tail just goes
(delete-region c end) (setq end c)))
(if (not (proof-track--balanced-string-p (buffer-substring beg end)))
(progn (message "proof-track: the deletion cuts a brace group; select whole groups") nil)
(let ((m (proof-track--enclosing beg)))
(cond
((and m (memq (car m) '(add note))) ; added text, notes: really deleted
(delete-region beg end)
(let ((m (proof-track--mark-at-open (nth 3 m))))
(if (and (eq (car m) 'add) (= (nth 4 m) (+ (nth 3 m) 2)))
(progn (delete-region (nth 2 m) (nth 4 m)) (nth 2 m))
beg)))
((and m (nth 4 m)) (if backward (nth 2 m) (nth 4 m))) ; struck already
(t (proof-track--strike beg end backward))))))
(defun proof-track--strike (beg end backward)
"Strike the text between BEG and END, which is outside any mark: the
additions in it vanish, the deletions and notes in it stay, the rest is
wrapped in \\del{} (\\delmath{} for maths), one per paragraph."
(let ((bm (copy-marker beg)) (em (copy-marker end t))
(re (regexp-opt (append proof-add-cmds proof-strike-cmds proof-note-cmds)))
(pos beg) pieces)
(save-excursion
(goto-char beg)
(while (re-search-forward re end t)
(let ((m (proof-track--mark-at-open (1- (match-end 0)))))
(if (and m (nth 4 m) (<= (nth 4 m) end)
(zerop (proof--depth beg (nth 2 m))))
(progn (push (list 'plain pos (nth 2 m)) pieces)
(push m pieces)
(setq pos (nth 4 m))
(goto-char pos))
(goto-char (match-end 0))))))
(push (list 'plain pos end) pieces)
(dolist (pc pieces) ; the last one first
(pcase (car pc)
('plain (proof-track--strike-plain (nth 1 pc) (nth 2 pc)))
('add (delete-region (nth 2 pc) (nth 4 pc)))))
(proof-track--merge bm em)
(prog1 (if backward (marker-position bm) (marker-position em))
(set-marker bm nil) (set-marker em nil))))
(defun proof-track--strike-plain (beg end)
"Wrap each paragraph of the unmarked text between BEG and END in a strike."
(let ((chunks nil) (pos beg))
(save-excursion
(goto-char beg)
(while (re-search-forward "\n[ \t]*\n" end t)
(when (zerop (proof--depth beg (match-beginning 0)))
(push (cons pos (match-beginning 0)) chunks)
(setq pos (match-end 0))))
(push (cons pos end) chunks))
(dolist (ch chunks)
(let* ((a (car ch)) (b (cdr ch)) (text (buffer-substring-no-properties a b))
(math (or (string-match-p "\\\\begin{\\|\\\\\\[\\|\\$\\$" text)
(and (fboundp 'texmathp) (save-excursion (goto-char a) (texmathp)))))
(cmd (if math proof-track-delmath proof-track-del)))
(unless (string= text "")
(goto-char b) (insert "}")
(goto-char a) (insert cmd)
(unless math (proof-track--shield-cites a (+ b (length cmd)))))))))
;;; The change hooks ---------------------------------------------------------
(defun proof-track--skip-p (beg)
(or (not proof-track-mode) undo-in-progress
(bound-and-true-p revert-buffer-in-progress-p)
(null this-command)
(memq this-command proof-track-ignore-commands)
(and (symbolp this-command)
(string-prefix-p "proof-" (symbol-name this-command)))
(< beg (proof--body-start))
(proof-track--in-comment beg)))
(defun proof-track--before-change (beg end)
(setq proof-track--before
(list beg end (buffer-substring-no-properties beg end) (point))))
(defun proof-track--widen (beg end old new)
"Grow the changed span so that it does not cut a control word, nor
part a control word from its arguments. Return (BEG END OLD NEW)."
(let ((piece (if (string= new "") old new)))
;; a change that continues a control word starts at its backslash
(when (or (and (> beg (point-min)) (eq (char-before beg) ?\\)
(not (proof-track--escaped-p (1- beg))))
(and (string-match-p "\\`[a-zA-Z@]" piece)
(save-excursion
(goto-char beg) (skip-chars-backward "a-zA-Z@")
(and (eq (char-before) ?\\) (not (proof-track--escaped-p (1- (point))))))))
(let ((b (save-excursion
(goto-char beg) (skip-chars-backward "a-zA-Z@")
(if (eq (char-before) ?\\) (1- (point)) (point)))))
(let ((ctx (buffer-substring-no-properties b beg)))
(setq old (concat ctx old) new (concat ctx new) beg b))))
;; one that ends inside a control word ends with it, and its arguments
(when (or (string-match-p "\\\\[a-zA-Z@]*\\'" old) (string-match-p "\\\\[a-zA-Z@]*\\'" new))
(let ((e (save-excursion
(goto-char end) (skip-chars-forward "a-zA-Z@")
(with-syntax-table proof-syntax-table
(condition-case nil
(while (eq (char-after) ?{) (forward-sexp))
(scan-error nil)))
(point))))
(let ((ctx (buffer-substring-no-properties end e)))
(setq old (concat old ctx) new (concat new ctx) end e))))
(list beg end old new)))
(defun proof-track--after-change (beg end len)
(let ((before proof-track--before))
(setq proof-track--before nil)
(unless (or (proof-track--skip-p beg)
(not before) (> (nth 0 before) beg) (< (nth 1 before) (+ beg len)))
(let* ((old (substring (nth 2 before) (- beg (nth 0 before)) (+ (- beg (nth 0 before)) len)))
(at-end (= (point) end))
(opoint (or proof-track--cmd-point (nth 3 before)))
(in-span (<= beg opoint (+ beg len))))
(condition-case err
(let ((target (save-excursion
(proof-track--change beg end old (> opoint beg)))))
(when (eq target 'refused) (setq target opoint))
(when (and target (if (zerop len) at-end (or at-end in-span)))
(goto-char target)
(setq proof-track--goto (copy-marker target))))
(error (message "proof-track: %s" (error-message-string err))))))))
(defun proof-track--pre-command ()
(setq proof-track--cmd-point (point)))
(defun proof-track--post-command ()
(setq proof-track--cmd-point nil)
(when proof-track--goto
(when (marker-buffer proof-track--goto) (goto-char proof-track--goto))
(set-marker proof-track--goto nil)
(setq proof-track--goto nil)))
(defun proof-track--change (beg end old backward)
"The buffer holds between BEG and END the text that replaced OLD: turn
the change into marks. Return where point goes."
(let* ((new (buffer-substring-no-properties beg end))
(n (min (length old) (length new))) (p 0) (s 0))
(while (and (< p n) (eq (aref old p) (aref new p))) (setq p (1+ p)))
(while (and (< s (- n p))
(eq (aref old (- (length old) s 1)) (aref new (- (length new) s 1))))
(setq s (1+ s)))
(setq beg (+ beg p) end (- end s)
old (substring old p (- (length old) s))
new (substring new p (- (length new) s)))
(let ((m (proof-track--enclosing beg)))
(cond
((and (string= old "") (string= new "")) nil)
;; edits within an addition or a note are free
((and m (memq (car m) '(add note))
(proof-track--balanced-string-p old) (proof-track--balanced-string-p new))
(if (not (eq (car m) 'add)) end
(let ((m (proof-track--mark-at-open (nth 3 m))))
(if (= (nth 4 m) (+ (nth 3 m) 2)) ; emptied: it goes
(progn (delete-region (nth 2 m) (nth 4 m)) (nth 2 m))
(proof-track--split m end)))))
;; blanks moved about by filling or indenting
((and (proof-track--blank-p old) (proof-track--blank-p new)
(not (memq this-command proof-track-edit-commands)))
nil)
(t
(unless (or (and m (eq (car m) 'del))
(and (string= new "") (= (length old) 1))) ; `kill-char' sees to it
(pcase-setq `(,beg ,end ,old ,new) (proof-track--widen beg end old new)))
(goto-char beg) (insert old) ; the old text back, before the new
(let* ((ob (+ beg (length old)))
(nb (copy-marker ob t)) (ne (copy-marker (+ ob (length new)) t))
(r (cond ((string= old "") beg)
((and (string= new "") (= (length old) 1))
(proof-track--kill-char beg backward))
(t (proof-track--kill-region beg ob backward)))))
(prog1
(cond
((null r) ; refused: nothing changes
(delete-region nb ne) 'refused)
((string= new "")
(let ((m (proof-track--enclosing r)) ; never leave point in a \del{}
(a (and (not backward) (proof-track--mark-ending-at r))))
(cond ((and m (eq (car m) 'del) (nth 4 m))
(if backward (nth 2 m) (nth 4 m)))
;; C-d typed at the end of an addition moved its
;; \del{} before it: point stays where it was typing
((proof-track--own-p a 'add) (1- r))
(t r))))
(t (proof-track--insert (marker-position nb) (marker-position ne))))
(set-marker nb nil) (set-marker ne nil))))))))
;;; The mode -----------------------------------------------------------------
;;;###autoload
(define-minor-mode proof-track-mode
"Track changes as proofing marks: inserted text is wrapped in \\add{},
deleted text in \\del{}, to be accepted or rejected with proof.el.
See the commentary at the top of proof-track.el."
:lighter " Track"
(if proof-track-mode
(progn
(add-hook 'before-change-functions #'proof-track--before-change nil t)
(add-hook 'after-change-functions #'proof-track--after-change nil t)
(add-hook 'pre-command-hook #'proof-track--pre-command nil t)
(add-hook 'post-command-hook #'proof-track--post-command nil t)
(save-excursion
(goto-char (point-min))
(when (and (search-forward "\\begin{document}" nil t)
(not (search-backward "{\\add}" nil t)))
(message "proof-track: no \\add defined here -- M-x proof-track-preamble"))))
(remove-hook 'before-change-functions #'proof-track--before-change t)
(remove-hook 'after-change-functions #'proof-track--after-change t)
(remove-hook 'pre-command-hook #'proof-track--pre-command t)
(remove-hook 'post-command-hook #'proof-track--post-command t)))
(defun proof-track-preamble ()
"Put the definitions of the proofing marks just before \\begin{document}."
(interactive)
(save-excursion
(goto-char (point-min))
(unless (search-forward "\\begin{document}" nil t)
(user-error "No \\begin{document} in this buffer"))
(goto-char (match-beginning 0))
(let ((proof-track-mode nil) (pre (buffer-substring (point-min) (point))))
(unless (string-match-p "{\\(x\\)?color}" pre) (insert "\\usepackage{xcolor}\n"))
(unless (string-match-p "{ulem}" pre) (insert "\\usepackage[normalem]{ulem}\n"))
(unless (string-match-p "{\\\\add}" pre)
(insert "\\DeclareRobustCommand{\\add}[1]{{\\color{red}#1}}\n"
"\\DeclareRobustCommand{\\addsec}[1]{{\\color{red}#1}}\n"
"\\DeclareRobustCommand{\\del}[1]{{\\color{black!55}\\csname sout\\endcsname{#1}}}\n"
"\\DeclareRobustCommand{\\delmath}[1]{{\\color{black!55}#1}}\n"
"\\DeclareRobustCommand{\\note}[1]{{\\color{blue}\\itshape[#1]}}\n")))))
;; the key is in proof.el's map; set here too for an Emacs that loaded an
;; older proof.el, whose `defvar'ed map a reload would not renew
(define-key proof-marks-mode-map (kbd "C-c p t") #'proof-track-mode)
(provide 'proof-track)
See also
- Emacs, and its key bindings.
- The gaming keyboard.
- Strike-outs in LaTeX: ulem or soul.
- Emacs proofing $\mathrm{\LaTeX}$ (red and strike-throughs), the 2024 hack.