Fix style

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

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
 

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;}
 }

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;

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")}

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='')