diff --git a/frontend/src/copy-to-clipboard.ts b/frontend/src/copy-to-clipboard.ts
index 726fd03..bafb4e5 100644
--- a/frontend/src/copy-to-clipboard.ts
+++ b/frontend/src/copy-to-clipboard.ts
@@ -1,3 +1,4 @@
+// utility function to copy e.g. the LaTeX code into the user's clipboard
 // @ts-ignore
 window.copyToClipboard = (text: string) => {
 	const textarea = document.createElement("textarea");
diff --git a/frontend/src/input-bar-enhancements.ts b/frontend/src/input-bar-enhancements.ts
index a9dc2c1..6ba8bc0 100644
--- a/frontend/src/input-bar-enhancements.ts
+++ b/frontend/src/input-bar-enhancements.ts
@@ -1,5 +1,5 @@
 function changeEvent(element: HTMLElement, inputID: string) {
-	// notify Vaadin
+	// notify Vaadin about the text value change
 	// @ts-ignore
 	document.getElementById(inputID)!.__dataValue.value = element.value;
 	const evt = new Event("change", { bubbles: true });
@@ -8,6 +8,8 @@ function changeEvent(element: HTMLElement, inputID: string) {
 
 // @ts-ignore
 window.buttonListener = (buttonID: string, inputID: string) => {
+	// this function is called when the lambda button or the ∀ button is pressed
+	// the requested character is inserted at the cursor position
 	let replacement = (buttonID === "lambda-button") ? 'λ' : '∀';
 	const button = document.getElementById(buttonID)!;
 	const input = document.getElementById(inputID)!;
@@ -24,6 +26,7 @@ window.buttonListener = (buttonID: string, inputID: string) => {
 
 // @ts-ignore
 window.characterListener = (inputID: string) => {
+	// called when the user types in one of the input fields (see InputBar.java)
 	let toReplace = (inputID === "term-input-field") ? '\\' : '!';
 	let replacement = (inputID === "term-input-field") ? 'λ' : '∀';
 	document.getElementById(inputID)!.addEventListener('keyup', e => {
diff --git a/frontend/src/key-shortcuts.ts b/frontend/src/key-shortcuts.ts
index 433c75c..39822ad 100644
--- a/frontend/src/key-shortcuts.ts
+++ b/frontend/src/key-shortcuts.ts
@@ -1,10 +1,12 @@
+// register a global listener for key events
 document.onkeydown = handleKey;
 
 function handleKey(e: KeyboardEvent) {
 	if ((e.target! as HTMLElement).tagName.toLowerCase() === "vaadin-text-field") {
-		return;
+		return; // don't process text input
 	}
 	let element = null;
+	// these shortcuts are documented in the help dialog
 	if (e.code === "ArrowLeft") {
 		// left arrow
 		if (!e.ctrlKey) {
diff --git a/frontend/src/mathjax-adapter.ts b/frontend/src/mathjax-adapter.ts
index 82c87d8..a4daead 100644
--- a/frontend/src/mathjax-adapter.ts
+++ b/frontend/src/mathjax-adapter.ts
@@ -1,6 +1,7 @@
 import {LitElement, html} from 'lit-element';
 import {TemplateResult} from "lit-html";
 
+// TypeScript declarations, only used to typecheck the code
 declare let window: {
 	MathJax: {
 		typesetShadow: (shadowRoot: ShadowRoot, callback: () => void) => void,
@@ -9,6 +10,7 @@ declare let window: {
 	addEventListener: (event: string, listener: () => void) => void;
 };
 
+// base class that can typeset content added to it
 export abstract class MathjaxAdapter extends LitElement {
 	private execTypeset(shadowRoot: ShadowRoot, extraData: any) {
 		if (window.MathJax) {
diff --git a/frontend/src/mathjax-display.ts b/frontend/src/mathjax-display.ts
index 958ddf5..7e2f873 100644
--- a/frontend/src/mathjax-display.ts
+++ b/frontend/src/mathjax-display.ts
@@ -1,5 +1,6 @@
 import {MathjaxAdapter} from "./mathjax-adapter";
 
+// really basic class that only displays some static LaTeX code
 class MathjaxDisplay extends MathjaxAdapter {
 	connectedCallback() {
 		super.connectedCallback();
diff --git a/frontend/src/mathjax-explanation.ts b/frontend/src/mathjax-explanation.ts
index 99aeed8..0400cda 100644
--- a/frontend/src/mathjax-explanation.ts
+++ b/frontend/src/mathjax-explanation.ts
@@ -2,6 +2,8 @@ import {MathjaxAdapter} from "./mathjax-adapter";
 
 class MathjaxExplanation extends MathjaxAdapter {
 	private lastStepShown: number = 0
+	static readonly opacityInactive: string = "0.5"
+	static readonly opacityActive: string = "1.0"
 
 	connectedCallback() {
 		super.connectedCallback();
@@ -16,6 +18,7 @@ class MathjaxExplanation extends MathjaxAdapter {
 
 	protected calculateSteps(_extraData: any) {
 		let stepIdx = 0;
+		// find all of the rendered steps and register click listeners
 		for (let text of this.shadowRoot!.querySelectorAll<HTMLElement>(".tc-text")) {
 			let thisStepIdx = stepIdx;
 			stepIdx++;
@@ -28,20 +31,21 @@ class MathjaxExplanation extends MathjaxAdapter {
 				this.scrollToElementIfNeeded(text);
 				continue;
 			}
-			text.style.opacity = "0.5";
+			text.style.opacity = MathjaxExplanation.opacityInactive;
 		}
 	}
 
 	protected showStep(n: number): void {
+		// lower the opacity of the previously active step and show the next one
 		let lastEl = this.getElementForStep(this.lastStepShown);
 		if (lastEl) {
-			lastEl.style.opacity = "0.5";
+			lastEl.style.opacity = MathjaxExplanation.opacityInactive;
 		}
 		let el = this.getElementForStep(n);
 		this.lastStepShown = n;
 		if (el) {
 			this.scrollToElementIfNeeded(el);
-			el.style.opacity = "1.0";
+			el.style.opacity = MathjaxExplanation.opacityActive;
 		}
 	}
 
diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts
index 2b536b5..0ce2457 100644
--- a/frontend/src/mathjax-proof-tree.ts
+++ b/frontend/src/mathjax-proof-tree.ts
@@ -1,6 +1,7 @@
 import {MathjaxAdapter} from "./mathjax-adapter";
 import {hoverAreaAroundElements} from "./mathjax-style-hacks";
 
+// Typescript declaration of the svg-pan-zoom library used
 declare let window: {
     svgPanZoomFun: (svg: SVGElement, options: {
         fit: boolean;
@@ -28,11 +29,13 @@ declare global {
     }
 }
 
+// methods declared in the Java class
 interface ProofTreeServer {
     setStepCount: (count: number) => void;
 }
 
 class MathjaxProofTree extends MathjaxAdapter {
+    // list of the SVG elements that make up each step in the proof tree
     private steps: [SVGElement, SVGElement[]][] = [];
     private $server: ProofTreeServer | undefined;
     // the element used as tooltip background
@@ -43,7 +46,9 @@ class MathjaxProofTree extends MathjaxAdapter {
     // true if the user is currently moving the proof tree around
     private panningSvg: boolean = false;
     private hoveringOnElement: SVGGraphicsElement | null = null;
+    // CSS elements used to highlight types etc.
     private hoverStyles: HTMLElement | null = null;
+    // (in the unification element too)
     private hoverStylesUnification: HTMLElement | null = null;
 
     protected showStep(n: number): void {
@@ -62,6 +67,8 @@ class MathjaxProofTree extends MathjaxAdapter {
     }
 
     private analyzeSvgStructure() {
+        // this function process the MathJax output, performs some display corrections and finally determines which
+        // SVG elements belong to which step
         const semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
         const inferenceRuleSelector = 'g[semantics="bspr_inferenceRule:down"]';
         const labelSelector = 'g[semantics="bspr_prooflabel:left"]';
@@ -77,6 +84,7 @@ class MathjaxProofTree extends MathjaxAdapter {
             root = root.parentNode! as SVGElement;
         }
         // first, enumerate all of the steps
+        // and assign IDs
         let stepIdx = 0;
         for (const a of [root, ...root.querySelectorAll<SVGElement>("g[semantics]")]) {
             let semantics = a.getAttribute("semantics")!;
@@ -86,7 +94,7 @@ class MathjaxProofTree extends MathjaxAdapter {
                 stepIdx++;
             }
         }
-        // then create the steps
+        // then create the steps list
         let steps: [SVGElement, SVGElement[]][] = [];
         stepIdx = 0;
         for (const a of [root, ...root.querySelectorAll<SVGElement>("g[semantics]")]) {
@@ -150,7 +158,6 @@ class MathjaxProofTree extends MathjaxAdapter {
         // in each row, the elements are arranged to not overlap
         // 2. place inference conclusions under the center of their line
         const nodeIterator = [...root.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']," + inferenceRuleSelector)];
-        console.log(`working with ${nodeIterator.length} nodes`);
         // start layout fixes in the innermost part of the SVG
         nodeIterator.reverse();
         for (const row of nodeIterator) {
@@ -250,7 +257,7 @@ class MathjaxProofTree extends MathjaxAdapter {
 
         // svg-pan-zoom should not be used on empty SVGs
         if (nodeIterator.length >= 3) {
-            // a timeout is required, otherwise the proof tree is moved around
+            // a timeout is required, otherwise the proof tree is moved around..
             setTimeout(() => {
                 this.setupPanZoom(this.shadowRoot!, svg);
             }, 100);
@@ -280,7 +287,7 @@ class MathjaxProofTree extends MathjaxAdapter {
                     // Handle double tap
                     // @ts-ignore
                     this.hammer.on('doubletap', () => {
-                        options.instance.zoomIn()
+                        options.instance.zoomIn();
                     });
 
                     let pannedX = 0;
@@ -304,14 +311,9 @@ class MathjaxProofTree extends MathjaxAdapter {
                         if (explainer) {
                             const ctm1 = svg.getBoundingClientRect();
                             const ctm2 = this.defElBackground!.getBoundingClientRect();
-                            explainer.style.left = (ctm2.left - ctm1.left) + "px";
-                            explainer.style.top = (ctm2.bottom - ctm1.top) + "px";
-                            // TODO(performance): this should be more efficient, but somehow flickers
-                            /*
-							const dx = (ctm2.left - ctm1.left) - explainer.offsetLeft;
-							const dy = (ctm2.bottom - ctm1.top) - explainer.offsetTop;
-							explainer.style.transform = "translate(" + dx + "px," + dy + "px)";
-							 */
+                            const dx = (ctm2.left - ctm1.left) - explainer.offsetLeft;
+                            const dy = (ctm2.bottom - ctm1.top) - explainer.offsetTop;
+                            explainer.style.transform = "translate(" + dx + "px," + dy + "px)";
                         }
                     });
                     // @ts-ignore
@@ -423,6 +425,7 @@ class MathjaxProofTree extends MathjaxAdapter {
             }
             let typeTarget = e.target! as SVGGraphicsElement;
             let counter = 0;
+            // try to find a relevant element in the tree
             while (typeTarget.classList
             && !typeTarget.classList.contains("typicalc-type")
             && !typeTarget.classList.contains("typicalc-label")) {
@@ -435,6 +438,8 @@ class MathjaxProofTree extends MathjaxAdapter {
             if (!typeTarget.classList) {
                 return;
             }
+            // hover over step label => show tooltip of definition, highlight constraints added
+            // hover over type => highlight it everywhere
             let isType = typeTarget.classList.contains("typicalc-type");
             let isLabel = typeTarget.classList.contains("typicalc-label");
             if (mouseIn) {
@@ -453,6 +458,7 @@ class MathjaxProofTree extends MathjaxAdapter {
                     }
                     let stepIndex = stepTarget.getAttribute("typicalc") === "step" ? Number(stepTarget.id.substring(4)) : -1;
 
+                    // un-hide the definition text
                     const defId = typeTarget.classList[1].replace("-label-", "-definition-");
                     const defEl = this.shadowRoot!.getElementById(defId)! as unknown as SVGGraphicsElement;
                     const transform = viewport.getTransformToElement(typeTarget);
@@ -462,6 +468,7 @@ class MathjaxProofTree extends MathjaxAdapter {
                     const svgRect = defEl.getBBox();
                     defEl.transform.baseVal[0].matrix.e = -transform.e - svgRect.width + offsetX + 1000;
                     defEl.transform.baseVal[0].matrix.f = -transform.f - 5500 + offsetY;
+                    // create the yellow tooltip background
                     this.defElBackground = root.getElementById(this.hoverTextBackgroundElID) as SVGRectElement | null;
                     if (!this.defElBackground) {
                         this.defElBackground = document.createElementNS("http://www.w3.org/2000/svg", "rect");
@@ -488,10 +495,11 @@ class MathjaxProofTree extends MathjaxAdapter {
                     p.style.top = (ctm2.bottom - ctm1.top) + "px";
                     p.style.backgroundColor = "white";
                     p.style.padding = "5px";
-                    p.innerText = data[stepIndex];
+                    p.innerText = data[stepIndex]; // add custom data to tooltip
                     // @ts-ignore
                     window.MathJax.typesetPromise([p])
                         .then(() => {
+                            // add rendered custom text to the main tooltip
                             const svgRect2 = this.defElBackground!.getBBox();
 
                             const svgP = p.getElementsByTagName("svg")[0];
@@ -567,9 +575,15 @@ class MathjaxProofTree extends MathjaxAdapter {
             const exp = explainers[explainers.length - 1];
             exp.parentNode!.removeChild(exp);
         }
+        // hide definition texts
         this.shadowRoot!
             .querySelectorAll<SVGGraphicsElement>(".typicalc-definition")!
-            .forEach((it) => it.style.display = "none");
+            .forEach((it) => {
+                if (it.style) {
+                    it.style.display = "none"
+                }
+            });
+        // remove the tooltip background
         let defElBackground = this.shadowRoot!.getElementById(this.hoverTextBackgroundElID);
         if (defElBackground) {
             defElBackground.parentElement!.removeChild(defElBackground);
diff --git a/frontend/src/mathjax-setup.js b/frontend/src/mathjax-setup.js
index 1c51320..d140dcf 100644
--- a/frontend/src/mathjax-setup.js
+++ b/frontend/src/mathjax-setup.js
@@ -3,6 +3,7 @@
 SVGElement.prototype.getTransformToElement = SVGElement.prototype.getTransformToElement || function(elem) {
     return elem.getScreenCTM().inverse().multiply(this.getScreenCTM());
 };
+// MathJax configuration boilerplate and ShadowDOM adapter
 window.MathJax = {
     loader: {
         load: ['output/svg', '[tex]/ams', '[tex]/bussproofs', '[tex]/color', '[tex]/html', '[tex]/textmacros', '[tex]/unicode']
@@ -112,13 +113,13 @@ window.MathJax = {
                 bubbles: true,
                 composed: true,
                 detail: "composed"
-            })
+            });
             MathJax.startup.defaultReady();
             MathJax.startup.promise.then(() => {
                 console.log("MathJax initialized");
                 MathJax.isInitialized = true;
                 document.dispatchEvent(event);
-            })
+            });
         }
     }
 };
diff --git a/frontend/src/mathjax-style-hacks.ts b/frontend/src/mathjax-style-hacks.ts
index e446f47..9fc83cc 100644
--- a/frontend/src/mathjax-style-hacks.ts
+++ b/frontend/src/mathjax-style-hacks.ts
@@ -1,3 +1,6 @@
+// to ease hovering above step labels and types, we increase the usable target area
+// in the case of Firefox, we add an invisible stroke to the SVG element
+// in the case of Chrome, we set the pointer-events area to the rectangular bounding box of the element
 export const hoverAreaAroundElements: string = `
 .typicalc-type, g[semantics='bspr_prooflabel:left'] {
 	/* cross-browser-compatibility: Chrome does not support the stroke trick, but instead bounding-box (which is not supported by Firefox..) */
diff --git a/frontend/src/share-dialog-autoselect.ts b/frontend/src/share-dialog-autoselect.ts
index 36bc849..67031eb 100644
--- a/frontend/src/share-dialog-autoselect.ts
+++ b/frontend/src/share-dialog-autoselect.ts
@@ -1,5 +1,6 @@
 // @ts-ignore
 window.autoSelect = (className: string) => {
+	// select entire text when the field is focused
 	let el = document.getElementsByClassName(className);
 	Array.from(el).forEach(field => {
 		field.addEventListener('focus', event => {
diff --git a/frontend/src/type-input-listener.ts b/frontend/src/type-input-listener.ts
index b83b083..e59a7f6 100644
--- a/frontend/src/type-input-listener.ts
+++ b/frontend/src/type-input-listener.ts
@@ -1,3 +1,5 @@
+// this listener is used in the type assumptions input field to subscript type indices etc.
+
 const subscripted = [...'\u2080\u2081\u2082\u2083\u2084\u2085\u2086\u2087\u2088\u2089'];
 
 // @ts-ignore
diff --git a/frontend/styles/view/main/upper-bar.css b/frontend/styles/view/main/upper-bar.css
index 8898f3a..3a98600 100644
--- a/frontend/styles/view/main/upper-bar.css
+++ b/frontend/styles/view/main/upper-bar.css
@@ -20,6 +20,8 @@
 
 #input-bar {
 	width: 75%;
+	/* require a larger width on small screens! */
+	min-width: min(100%, 1100px);
 	flex-grow: 1;
 	align-items: flex-end;
 	padding: 0 1em;