Prevent line breaks in blueprint inside math environments

PrimeNumberTheoremAnd/MellinCalculus.lean

@@ -279,10 +279,10 @@ lemma limitOfConstant {a : ℝ → ℂ} {σ : ℝ} (σpos : 0 < σ)
     (ha' : Tendsto a atTop (𝓝 0)) : a σ = 0 := by
 /-%%
 \begin{proof}\leanok\begin{align*}
-\lim_{\sigma'\to\infty}a(\sigma) &= \lim_{\sigma'\to\infty}a(\sigma') \\
+\lim_{\sigma'\to\infty}a(\sigma) &= \lim_{\sigma'\to\infty}a(\sigma') \\%nobreak%
 %%-/
   have := eventuallyEq_of_mem (mem_atTop σ) fun σ' h ↦ ha σ' σ (σpos.trans_le h) σpos
---%% &= 0
+--%% &= 0%nobreak%
   exact tendsto_const_nhds_iff.mp (ha'.congr' this)
 --%%\end{align*}\end{proof}
 
@@ -559,10 +559,10 @@ lemma limitOfConstantLeft {a : ℝ → ℂ} {σ : ℝ} (σlt : σ ≤ -3/2)
 /-%%
 \begin{proof}\leanok
 \begin{align*}
-\lim_{\sigma'\to-\infty}a(\sigma) &= \lim_{\sigma'\to-\infty}a(\sigma') \\
+\lim_{\sigma'\to-\infty}a(\sigma) &= \lim_{\sigma'\to-\infty}a(\sigma') \\%nobreak%
 %%-/
   have := eventuallyEq_of_mem (mem_atBot (-3/2)) fun σ' h ↦ ha σ' σ h σlt
---%% &= 0
+--%% &= 0%nobreak%
   exact tendsto_const_nhds_iff.mp (ha'.congr' this)
 --%%\end{align*}\end{proof}
 

leanblueprint-extract/extract_blueprint

@@ -181,7 +181,7 @@ def extract_blueprint(text):
     matches=re.finditer(r'^'+line_delimiter+r'(.*)$', text, flags=re.MULTILINE)
     for match in matches:
         # add to extracted dict
-        extracted[match.start(1)]=match.group(1)
+        extracted[match.start(1)]=match.group(1)+"\n"
 
     # text without blueprint
     text_without=re.sub(start_delimiter+r'.*?'+end_delimiter,'', text, flags=re.DOTALL)
@@ -192,7 +192,10 @@ def extract_blueprint(text):
     # combine entries
     out=""
     for item in extracted:
-        out=out+item[1]+"\n\n"
+        out=out+item[1]+"\n"
+
+    # remove newlines when they are explicitly prevented
+    out=re.sub(r'%nobreak%\s\s*','\n',out)
 
     # return the blueprint and the lean file without the blueprint
     return (out,text_without)