.

awueth · May 6, 2024 · f003e0c · f003e0c
1 parent 1a3e790
commit f003e0c
Show file tree

Hide file tree

Showing 5 changed files with 75 additions and 4 deletions.
diff --git a/blueprint/lean_decls b/blueprint/lean_decls
@@ -0,0 +1 @@
+volume
diff --git a/blueprint/src/macros/web.tex b/blueprint/src/macros/web.tex
@@ -2,4 +2,4 @@
 % the web version. Of course they should have a corresponding
 % version in macros/print.tex.
 % Typically the printed version could have more fancy decorations.
-% This will probably be a very short file.
+% This will probably be a very short file.
diff --git a/blueprint/src/web.paux b/blueprint/src/web.paux
diff --git a/blueprint/web/dep_graph_document.html b/blueprint/web/dep_graph_document.html
@@ -58,7 +58,37 @@ <h1 id="doc_title">Dependencies</h1>
     </dl>
   </div>
     <div id="graph"></div>
-<div id="statements"></div>
+<div id="statements">
+
+
+    <div class="dep-modal-container" id="def:volume_modal">
+      <div class="dep-modal-content">
+          <button class="dep-closebtn">
+<svg  class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
+</button>
+
+  <div class="thm" id="def:volume" style="display: none">
+    <div class="thm_thmheading">
+      <span class="definition_thmcaption">
+      Definition
+      </span>
+      <span class="definition_thmlabel">0.1</span></div>
+    <div class="thm_thmcontent"><p>  test </p>
+</div>
+
+    <a class="latex_link" href="index.html#def:volume">LaTeX</a>
+
+
+  <a class="lean_link lean_decl" href="https://awueth.github.io/mathlib4/docs/find/#doc/volume">Lean</a>
+
+
+
+
+  </div>
+
+      </div>
+    </div>
+</div>
 </div> <!-- content -->
 </div> <!-- wrapper -->
 <script src="js/jquery.min.js" type="text/javascript"></script>
@@ -77,7 +107,7 @@ <h1 id="doc_title">Dependencies</h1>
     .width(width)
     .height(height)
     .fit(true)
-    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [penwidth=1.8];	edge [arrowhead=vee];}`)
+    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [label="\N",		penwidth=1.8	];	edge [arrowhead=vee];	"def:volume"	[color=blue,		fillcolor="#A3D6FF",		label=volume,		shape=box,		style=filled];}`)
     .on("end", interactive);
 
 latexLabelEscaper = function(label) {

diff --git a/blueprint/web/index.html b/blueprint/web/index.html
@@ -36,7 +36,47 @@ <h1>Formalising Cheeger’s inequality</h1>
 </p>
 </div>
 <p>Hello this is a test </p>
-<p>\( \frac{\sum _{u \tilde v} (f(u) - f(v))^2}{\sum _{v} f(v)^2 d_v} \)  </p>
+<div class="definition_thmwrapper theorem-style-plain" id="def:volume">
+  <div class="definition_thmheading">
+    <span class="definition_thmcaption">
+    Definition
+    </span>
+    <span class="definition_thmlabel">0.1</span>
+    <div class="thm_header_extras">
+
+        </div>
+    <div class="thm_header_hidden_extras">
+
+    <a class="icon proof" href="index.html#def:volume">#</a>
+
+
+
+    <button class="modal lean">L∃∀N</button>
+        <div class="modal-container">
+      <div class="modal-content">
+        <header>
+          <h1>Lean declarations</h1>
+          <button class="closebtn"><svg  class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
+</button>
+        </header>
+
+        <ul class="uses">
+
+          <li><a href="https://awueth.github.io/mathlib4/docs/find/#doc/volume" class="lean_decl">volume</a></li>
+
+        </ul>
+
+      </div>
+    </div>
+
+
+        </div>
+  </div>
+  <div class="definition_thmcontent">
+  <p>  test </p>
+
+  </div>
+</div>
 
 </div> <!--main-text -->
 </div> <!-- content-wrapper -->