From 577a0cb5d8cbc0a07b9716221bca18754f32c391 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Fri, 27 Sep 2024 04:39:43 -0400
Subject: [PATCH] Fix style

---
 Makefile                            |  2 +-
 README.md                           |  2 +-
 assets/extra/resources/coqdocjs.js  |  2 +-
 assets/extra/resources/depgraph.css | 12 ++++++++++++
 scripts/generate_dep.py             |  2 +-
 scripts/post_process_dep.py         |  2 ++
 6 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 28bccf0d..508adc9e 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-.PHONY: all pretty-timed test coqdoc clean depgraph
+.PHONY: all pretty-timed test coqdoc clean depgraphdoc
 
 all:
 	@$(MAKE) -C theories
diff --git a/README.md b/README.md
index f3541f3b..7cffdec5 100644
--- a/README.md
+++ b/README.md
@@ -11,7 +11,7 @@ elementary) and serves as a basis for future extensions.
 
 ## Online Documentation
 
-We have generated a [Coqdoc](toc.html) for browsing our Coq proof.
+We have generated a [Coqdoc](https://beluga-lang.github.io/McLTT/dep.html) for browsing our Coq proof.
 
 ## Architecture
 
diff --git a/assets/extra/resources/coqdocjs.js b/assets/extra/resources/coqdocjs.js
index 7ff56988..503cc870 100644
--- a/assets/extra/resources/coqdocjs.js
+++ b/assets/extra/resources/coqdocjs.js
@@ -168,7 +168,7 @@ function repairDom(){
 function fixTitle(){
   var url = "/" + window.location.pathname;
   var basename = url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.'));
-  if (basename === "toc") {document.title = "Table of Contents";}
+  if (basename === "dep") {document.title = "Table of Contents";}
   else if (basename === "indexpage") {document.title = "Index";}
   else {document.title = basename;}
 }
diff --git a/assets/extra/resources/depgraph.css b/assets/extra/resources/depgraph.css
index ecdcada7..7f27329a 100644
--- a/assets/extra/resources/depgraph.css
+++ b/assets/extra/resources/depgraph.css
@@ -1,3 +1,15 @@
+div.#main {
+    max-width: unset;
+}
+
+svg.depgraph {
+    max-width: 100%;
+}
+
+svg.depgraph > text:first-of-type {
+    font-weight: bold;
+}
+
 .text-highlight-edges text {
     opacity: 1 !important;
     stroke-width: 3;
diff --git a/scripts/generate_dep.py b/scripts/generate_dep.py
index 33e46892..0c4c8d21 100644
--- a/scripts/generate_dep.py
+++ b/scripts/generate_dep.py
@@ -89,7 +89,7 @@ def gen_graph() -> str:
     newline = "\n"
     return textwrap.dedent(f"""
       digraph Mcltt {{
-        graph [cluster=true,fontsize=28,label="Mcltt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
+        graph [center=true,class="depgraph",cluster=true,fontname="Open Sans",fontsize=28,label="Mcltt",labeljust=l,labelloc=t,penwidth=2,size=15,splines=true,tooltip=""];
         node [fontsize=18,shape=note,style=filled,URL="https://beluga-lang.github.io/McLTT/\\N.html"];
         {default_subgraph_decl("Algorithmic")}
         {default_subgraph_decl("Core")}
diff --git a/scripts/post_process_dep.py b/scripts/post_process_dep.py
index 8e476bf1..1de4b20e 100644
--- a/scripts/post_process_dep.py
+++ b/scripts/post_process_dep.py
@@ -5,6 +5,8 @@
 PROJECT_ROOT = Path(__file__).resolve().parents[1]
 SVG = parse(sys.stdin)
 SVG_ELEMENT = SVG.getElementsByTagName("svg")[0]
+ENTIRE_GRAPH_ELEMENT = SVG_ELEMENT.getElementsByTagName("g")[0]
+ENTIRE_GRAPH_ELEMENT.removeChild(ENTIRE_GRAPH_ELEMENT.getElementsByTagName("title")[0])
 SVG_ELEMENT.setAttribute("onload", "addInteractivity(evt)")
 for line in io.open(PROJECT_ROOT / "assets" / "extra" / "header.html"):
     print(line, end='')