From 97a489c259f5cc281aa1fea25910ab5911427314 Mon Sep 17 00:00:00 2001
From: "Hagb (Junyu Guo)" <hagb@hagb.name>
Date: Wed, 18 Jun 2025 22:20:15 +0800
Subject: [PATCH] add `\nodetitle` command to specify titles of nodes in
 dependency graph

The plastexdepgraph part is submitted in
https://github.com/PatrickMassot/plastexdepgraph/pull/9.
---
 README.md                                | 9 +++++++++
 leanblueprint/templates/macros/print.tex | 1 +
 2 files changed, 10 insertions(+)

diff --git a/README.md b/README.md
index 0cf9773..eee832e 100644
--- a/README.md
+++ b/README.md
@@ -146,6 +146,15 @@ The main TeX macros that relate your TeX code to your Lean code are:
   an environment could be either a definition/statement or a proof, depending on
   whether the referenced labels are necessary to state the definition/theorem
   or only in the proof.
+* `\nodetitle` that specifies the name in text or [HTML-like labels of graphviz](https://graphviz.org/doc/inrfo/shapes.html#html)
+  displayed on the node in dependency graph. Without this macro, the label
+  specified in `\label` with prefix stripped will be displayed. This macro can
+  be used for custom content or style specially for nodes in dependency graph,
+  independent from their names in pdf and other web pages. For example, long
+  names can be splitted into multiple lines with HTML-like labels (such as
+  `\nodetitle{<the_very-<BR\>long-name-<BR\>of-a-theorem}`) to avoid badly
+  displayed graph caused by long names, and main theorems can be bolded
+  (such as `\nodetitle{<<B>An Important Theorem</B>>}`).
 
 The example below show those essential macros in action, assuming the existence of
 LaTeX labels `def:immersion`, `thm:open_ample` and `lem:open_ample_immersion` and
diff --git a/leanblueprint/templates/macros/print.tex b/leanblueprint/templates/macros/print.tex
index 7870834..c3d9359 100644
--- a/leanblueprint/templates/macros/print.tex
+++ b/leanblueprint/templates/macros/print.tex
@@ -16,6 +16,7 @@
 \newcommand{\leanok}{}
 \newcommand{\mathlibok}{}
 \newcommand{\notready}{}
+\newcommand{\nodetitle}{}
 % Make sure that arguments of \uses and \proves are real labels, by using invisible refs:
 % latex prints a warning if the label is not defined, but nothing is shown in the pdf file.
 % It uses LaTeX3 programming, this is why we use the expl3 package.