Deploying to gh-pages from @ 06e8744 🚀

404.html

@@ -225,6 +225,8 @@ <h1><a class="header" href="#document-not-found-404" id="document-not-found-404"
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

axioms_and_computation.html

@@ -1185,6 +1185,8 @@ <h2><a class="header" href="#the-law-of-the-excluded-middle" id="the-law-of-the-
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

book.toml

@@ -11,7 +11,7 @@ build-dir = "out"
 
 [output.html]
 # additional-css = ["custom.css", "pygments.css"]
-# additional-js = ["custom.js"]
+additional-js = ["custom.js"]
 mathjax-support = true
 site-url = "/tp-lean-zh/"
 git-repository-url = "https://github.com/Lean-zh/tp-lean-zh"

conv.html

@@ -409,6 +409,8 @@ <h2><a class="header" href="#other-tactics-inside-conversion-mode" id="other-tac
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

custom.js

@@ -0,0 +1,7 @@
+const newline = /(?<=[，。、：」）])\n(?!\n)/g;
+const space = /\s+(<.+?>\p{Script=Han}.+?<\/.+?>)\s+/g
+const paras = document.querySelectorAll("#content > main > p");
+for (const p of paras) {
+  p.innerHTML = p.innerHTML.replace(newline, "");
+  p.innerHTML = p.innerHTML.replace(space, "$1");
+}

dependent_type_theory.html

@@ -1494,6 +1494,8 @@ <h2><a class="header" href="#隐参数" id="隐参数">隐参数</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

induction_and_recursion.html

@@ -1557,6 +1557,8 @@ <h2><a class="header" href="#exercises" id="exercises">Exercises</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

inductive_types.html

@@ -1631,6 +1631,8 @@ <h2><a class="header" href="#exercises" id="exercises">Exercises</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

interacting_with_lean.html

@@ -1354,6 +1354,8 @@ <h2><a class="header" href="#命名参数" id="命名参数">命名参数</a></h
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

introduction.html

@@ -361,6 +361,8 @@ <h2><a class="header" href="#致谢" id="致谢">致谢</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

propositions_and_proofs.html

@@ -1393,6 +1393,8 @@ <h2><a class="header" href="#练习" id="练习">练习</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

quantifiers_and_equality.html

@@ -1316,6 +1316,8 @@ <h2><a class="header" href="#练习" id="练习">练习</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

structures_and_records.html

@@ -480,6 +480,8 @@ <h2><a class="header" href="#inheritance" id="inheritance">Inheritance</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+
 
 
 

tactics.html

@@ -1945,6 +1945,8 @@ <h2><a class="header" href="#练习" id="练习">练习</a></h2>
 
         <!-- Custom JS scripts -->
 
+        <script type="text/javascript" src="custom.js"></script>
+