diff --git a/client/package.json b/client/package.json
index a795ae4..bcd9cab 100644
--- a/client/package.json
+++ b/client/package.json
@@ -137,11 +137,6 @@
 					"type": "boolean",
 					"default": true,
 					"description": "Auto-unindent `Qed.`, `Defined.`, and `Admitted.`. Note: requires `editor.formatOnType' to be set to `true` in settings.json"
-				},
-				"coq.hacks.userSettingsLocation": {
-					"type": "string",
-					"default": null,
-					"description": "Hack: vscode does not currently indicate to extensions where user-settings should be stored. Currently, we store such settings in this extension's own directory, but these will be overriden when this extension is updated. This setting allows you to override where user-settings are stored. WARNING: this setting will eventually go away."
 				}
 			}
 		},
@@ -332,11 +327,6 @@
 				"command": "extension.coq.ltacProf.getResults",
 				"title": "View ltac profile",
 				"category": "Coq"
-			},
-			{
-				"command": "extension.coq.proofView.customizeProofViewStyle",
-				"title": "Customize proof-view styling",
-				"category": "Coq"
 			}
 		],
 		"keybindings": [
@@ -531,6 +521,260 @@
 				"language": "coq",
 				"path": "./snippets/coq.json"
 			}
+		],
+		"colors": [
+			{
+				"id": "coq.proofviewText",
+				"description": "Color for proofview text.",
+				"defaults": {
+					"dark": "#cccccc",
+					"light": "#333333",
+					"highContrast": "#333333"
+				}
+			},
+			{
+				"id": "coq.proofviewMessage",
+				"description": "Color for proofview messages.",
+				"defaults": {
+					"dark": "#cccccc",
+					"light": "#333333",
+					"highContrast": "#333333"
+				}
+			},
+			{
+				"id": "coq.proofviewError",
+				"description": "Color for proofview errors.",
+				"defaults": {
+					"dark": "#ffc0cb",
+					"light": "#ff0000",
+					"highContrast": "#ff0000"
+				}
+			},
+			{
+				"id": "coq.hypothesisIdent",
+				"description": "Color for goal hypotheses identifiers.",
+				"defaults": {
+					"dark": "#20b2aa",
+					"light": "#006400",
+					"highContrast": "#006400"
+				}
+			},
+			{
+				"id": "coq.hypothesesSeparator",
+				"description": "Color for hypotheses separator.",
+				"defaults": {
+					"dark": "#ffffff66",
+					"light": "#00000033",
+					"highContrast": "#00000033"
+				}
+			},
+			{
+				"id": "coq.oddHypothesisBackground",
+				"description": "Background color for hypotheses with odd index.",
+				"defaults": {
+					"dark": "#0000000d",
+					"light": "#ffffff0d",
+					"highContrast": "#ffffff0d"
+				}
+			},
+			{
+				"id": "coq.newHypothesisBackground",
+				"description": "Background color for new hypotheses.",
+				"defaults": {
+					"dark": "#00ff0017",
+					"light": "#00aa0040",
+					"highContrast": "#00aa0040"
+				}
+			},
+			{
+				"id": "coq.changedHypothesisBackground",
+				"description": "Background color for changed hypotheses.",
+				"defaults": {
+					"dark": "#0000ff26",
+					"light": "#0000ff0d",
+					"highContrast": "#0000ff0d"
+				}
+			},
+			{
+				"id": "coq.goalId",
+				"description": "Color of goal identifiers.",
+				"defaults": {
+					"dark": "#add8e6",
+					"light": "#00008b",
+					"highContrast": "#00008b"
+				}
+			},
+			{
+				"id": "coq.addedCharacter",
+				"description": "Color of added characters (in diffs).",
+				"defaults": {
+					"dark": "#00fa001a",
+					"light": "#00fa0033",
+					"highContrast": "#00fa0033"
+				}
+			},
+			{
+				"id": "coq.removedCharacter",
+				"description": "Color of removed characters (in diffs).",
+				"defaults": {
+					"dark": "#fa000099",
+					"light": "#fa000033",
+					"highContrast": "#fa000033"
+				}
+			},
+			{
+				"id": "coq.mainSubgoalBackground",
+				"description": "Background color for main subgoal.",
+				"defaults": {
+					"dark": "#ffffff0d",
+					"light": "#0000000d",
+					"highContrast": "#0000000d"
+				}
+			},
+			{
+				"id": "coq.subgoalBackground",
+				"description": "Background color for subgoals.",
+				"defaults": {
+					"dark": "#ffffff0d",
+					"light": "#0000000d",
+					"highContrast": "#0000000d"
+				}
+			},
+			{
+				"id": "coq.subgoalSeparator",
+				"description": "Color of subgoal separators.",
+				"defaults": {
+					"dark": "#ffffff33",
+					"light": "#00000033",
+					"highContrast": "#00000033"
+				}
+			},
+			{
+				"id": "coq.termNotation",
+				"description": "Color of term notations.",
+				"defaults": {
+					"dark": "#ff8c00",
+					"light": "#ff8c00",
+					"highContrast": "#ff8c00"
+				}
+			},
+			{
+				"id": "coq.termKeyword",
+				"description": "Color of term keywords.",
+				"defaults": {
+					"dark": "#6495ed",
+					"light": "#6495ed",
+					"highContrast": "#6495ed"
+				}
+			},
+			{
+				"id": "coq.termEvar",
+				"description": "Color of existential variables.",
+				"defaults": {
+					"dark": "#ff8c00",
+					"light": "#ff8c00",
+					"highContrast": "#ff8c00"
+				}
+			},
+			{
+				"id": "coq.termPath",
+				"description": "Color of term paths.",
+				"defaults": {
+					"dark": "#9370d8",
+					"light": "#ff8c00",
+					"highContrast": "#ff8c00"
+				}
+			},
+			{
+				"id": "coq.termReference",
+				"description": "Color of name references in terms.",
+				"defaults": {
+					"dark": "#7cfc00",
+					"light": "#32cd32",
+					"highContrast": "#32cd32"
+				}
+			},
+			{
+				"id": "coq.termType",
+				"description": "Color of types in terms.",
+				"defaults": {
+					"dark": "#f08080",
+					"light": "#ff7f50",
+					"highContrast": "#ff7f50"
+				}
+			},
+			{
+				"id": "coq.termVariable",
+				"description": "Color of variables in terms.",
+				"defaults": {
+					"dark": "#7fff00",
+					"light": "#20b2aa",
+					"highContrast": "#20b2aa"
+				}
+			},
+			{
+				"id": "coq.debugMessage",
+				"description": "Color of debug messages.",
+				"defaults": {
+					"dark": "#9370d8",
+					"light": "#daa520",
+					"highContrast": "#daa520"
+				}
+			},
+			{
+				"id": "coq.errorMessage",
+				"description": "Color of error messages.",
+				"defaults": {
+					"dark": "#ff0000",
+					"light": "#ff0000",
+					"highContrast": "#ff0000"
+				}
+			},
+			{
+				"id": "coq.warningMessage",
+				"description": "Color of warning messages.",
+				"defaults": {
+					"dark": "#ffff00",
+					"light": "#ffff00",
+					"highContrast": "#ffff00"
+				}
+			},
+			{
+				"id": "coq.moduleKeyword",
+				"description": "Color of module keywords.",
+				"defaults": {
+					"dark": "#6495ed",
+					"light": "#6495ed",
+					"highContrast": "#6495ed"
+				}
+			},
+			{
+				"id": "coq.tacticKeyword",
+				"description": "Color of tactic keywords.",
+				"defaults": {
+					"dark": "#6495ed",
+					"light": "#6495ed",
+					"highContrast": "#6495ed"
+				}
+			},
+			{
+				"id": "coq.tacticPrimitive",
+				"description": "Color of tactic primitives.",
+				"defaults": {
+					"dark": "#5f9ea0",
+					"light": "#5f9ea0",
+					"highContrast": "#5f9ea0"
+				}
+			},
+			{
+				"id": "coq.tacticString",
+				"description": "Color of tactic strings.",
+				"defaults": {
+					"dark": "#ffa500",
+					"light": "#ffa500",
+					"highContrast": "#ffa500"
+				}
+			}
 		]
 	},
 	"scripts": {
diff --git a/client/src/HtmlCoqView.ts b/client/src/HtmlCoqView.ts
index 5cd7d8a..cb83f7f 100644
--- a/client/src/HtmlCoqView.ts
+++ b/client/src/HtmlCoqView.ts
@@ -6,7 +6,6 @@ import {extensionContext} from './extension'
 import * as proto from './protocol'
 import * as path from 'path';
 import * as docs from './CoqProject';
-import * as nasync from './nodejs-async';
 import * as psm from './prettify-symbols-mode';
 
 import mustache = require('mustache');
@@ -33,7 +32,6 @@ interface SettingsState {
   fontFamily?: string,
   fontSize?: string,
   fontWeight?: string,
-  cssFile?: string,
   prettifySymbolsMode?: boolean,
 }
 
@@ -42,13 +40,6 @@ type ProofViewProtocol = GoalUpdate | SettingsUpdate;
 
 const VIEW_PATH = 'html_views';
 
-function proofViewCSSFile() {
-  const userDir = vscode.workspace.getConfiguration("coq.hacks")
-    .get("userSettingsLocation", null)
-    || extensionContext.asAbsolutePath(path.join(VIEW_PATH,'goals'));
-  return vscode.Uri.file(path.join(userDir,'proof-view.css'));
-}
-
 function proofViewFile(file: string = "") {
   return vscode.Uri.file(extensionContext.asAbsolutePath(path.join(VIEW_PATH,'goals',file)));
 }
@@ -106,10 +97,8 @@ export class HtmlCoqView implements view.CoqView {
     }
   }
 
-
   private async createBuffer() : Promise<void> {
     try {
-      await HtmlCoqView.prepareStyleSheet();
       this.coqViewUri = vscode.Uri.parse(`file://${proofViewHtmlPath().path.replace(/%3A/, ':')}`);
       console.log("Goals: " + decodeURIComponent(this.coqViewUri.with({scheme: 'file'}).toString()));
     } catch(err) {
@@ -177,47 +166,8 @@ export class HtmlCoqView implements view.CoqView {
     this.currentSettings.fontFamily = vscode.workspace.getConfiguration("editor").get("fontFamily") as string;
     this.currentSettings.fontSize = `${vscode.workspace.getConfiguration("editor").get("fontSize") as number}pt`;
     this.currentSettings.fontWeight = vscode.workspace.getConfiguration("editor").get("fontWeight") as string;
-    this.currentSettings.cssFile = decodeURIComponent(proofViewCSSFile().toString());
     this.currentSettings.prettifySymbolsMode = psm.isEnabled();
     await this.sendMessage(Object.assign<SettingsState,{command: 'settings-update'}>(this.currentSettings,{command: 'settings-update'}));
   }
 
-  private static async shouldResetStyleSheet() : Promise<boolean> {
-    try {
-      const styleFile = proofViewCSSFile();
-      if(!await nasync.fs.exists(styleFile.fsPath))
-        return true;
-      const stat = await nasync.fs.stat(styleFile.fsPath);
-      if(stat.size < 5 && (await nasync.fs.readFile(styleFile.fsPath, 'utf8')).trim() === "")
-        return true;
-    } catch(err) {
-      console.error(err.toString());
-    }
-    return false;
-  }
-
-  /** makes sure that the style sheet is available */
-  private static async prepareStyleSheet() {
-    try {
-      const styleFile = proofViewCSSFile();
-      if(await HtmlCoqView.shouldResetStyleSheet() === true) {
-        const defaultFile = proofViewFile('default-proof-view.css');
-        await nasync.fs.copyFile(defaultFile.fsPath,styleFile.fsPath);
-      }
-    } catch(err) {
-      console.error(err.toString());
-    }
-  }
-
-
-  public static async customizeProofViewStyle() {
-    try {
-      await HtmlCoqView.prepareStyleSheet();
-      const styleFile = proofViewCSSFile();
-      const doc = await vscode.workspace.openTextDocument(styleFile.fsPath);
-      await vscode.window.showTextDocument(doc);
-    } catch(err) {
-      console.error(err.toString());
-    }
-  }
-}
+}
\ No newline at end of file
diff --git a/client/src/extension.ts b/client/src/extension.ts
index b3c8ee1..aff4969 100644
--- a/client/src/extension.ts
+++ b/client/src/extension.ts
@@ -5,7 +5,6 @@ import * as proto from './protocol';
 import {CoqProject, CoqDocument} from './CoqProject';
 import * as snippets from './Snippets';
 import {initializeDecorations} from './Decorations';
-import {HtmlCoqView} from './HtmlCoqView';
 import * as editorAssist from './EditorAssist';
 import * as psm from './prettify-symbols-mode';
 
@@ -64,7 +63,6 @@ export function activate(context: ExtensionContext) {
   regTCmd('query.prompt.print', queryPrint);
   regTCmd('proofView.viewStateAt', viewProofStateAt); 
   regTCmd('proofView.open', viewCurrentProofState); 
-  regCmd('proofView.customizeProofViewStyle', customizeProofViewStyle);
   regProjectCmd('ltacProf.getResults', project.ltacProfGetResults);
   regCmd('display.toggle.implicitArguments', () => project.setDisplayOption(proto.DisplayOption.ImplicitArguments, proto.SetDisplayOption.Toggle)); 
   regCmd('display.toggle.coercions', () => project.setDisplayOption(proto.DisplayOption.Coercions, proto.SetDisplayOption.Toggle)); 
@@ -193,8 +191,4 @@ function viewCurrentProofState(editor: TextEditor, edit: TextEditorEdit) {
   return withDocAsync(editor, async (doc) =>
     doc.viewGoalState(editor)
   )
-}
-
-function customizeProofViewStyle() {
-  HtmlCoqView.customizeProofViewStyle();
 }
\ No newline at end of file
diff --git a/html_views/.vscode/launch.json b/html_views/.vscode/launch.json
deleted file mode 100644
index 5c906c6..0000000
--- a/html_views/.vscode/launch.json
+++ /dev/null
@@ -1,27 +0,0 @@
-{
-  "version": "0.2.0",
-  "configurations": [
-    {
-      "name": "Launch Chrome against localhost, with sourcemaps",
-      "type": "chrome",
-      "request": "launch",
-      // "url": "file:///c:/users/cj/Research/vscoq/client/html_views/goals/ContainProofView.html?host=127.0.0.1&port=7731",
-      "url": "file:///c:/users/cj/Research/vscoq/client/html_views/ltacprof/LtacProf.html?host=127.0.0.1&port=6388",
-      "sourceMaps": true,
-      "webRoot": "c:/users/cj/Research/vscoq/",
-      "userDataDir": "${workspaceRoot}/chrome",
-      "sourceMapPathOverrides": {
-        "file:///c:/users/cj/Research/vscoq/client/html_views/src/*": "c:/users/cj/Research/vscoq/html_views/src/*",
-        "file:///c:/users/cj/Research/vscoq/client/html_views/goals/*": "c:/users/cj/Research/vscoq/html_views/src/goals/*"
-      }
-    },
-    {
-      "name": "Attach to Chrome, with sourcemaps",
-      "type": "chrome",
-      "request": "attach",
-      "port": 9222,
-      "sourceMaps": true,
-      "webRoot": "${workspaceRoot}"
-    }
-  ]
-}
\ No newline at end of file
diff --git a/html_views/src/goals/ContainProofView.html b/html_views/src/goals/ContainProofView.html
deleted file mode 100644
index 08edf3d..0000000
--- a/html_views/src/goals/ContainProofView.html
+++ /dev/null
@@ -1,19 +0,0 @@
-<!DOCTYPE HTML>
-<head>
-  <title>ProofView</title>
-  <style>
-    :root {
-      --background-color: blue;
-    }
-  </style>
-  <script type="text/javascript">
-    function loadC() {
-      var container = document.getElementById("container");
-      container.src = "file:///C:/users/cj/Research/vscoq/client/html_views/goals/Coq.html" + window.location.href.substr(window.location.href.indexOf('?'));
-    }
-  </script>
-</head>
-<body onload="loadC()" style="margin:0px;padding:0px;width:100%;height:100vh;border:none;position:absolute;top:0px;left:0px;right:0px;bottom:0px">
-	<iframe id="container" src="file:///C:/users/cj/Research/vscoq/client/html_views/goals/Coq.html?host=127.0.0.1&port=43704" seamless style="position:absolute;top:0px;left:0px;right:0px;bottom:0px;border:none;margin:0px;padding:0px;width:100%;height:100%"
-	/>
-</body>
\ No newline at end of file
diff --git a/html_views/src/goals/Coq.html b/html_views/src/goals/Coq.html
index d8fec09..2cc698e 100644
--- a/html_views/src/goals/Coq.html
+++ b/html_views/src/goals/Coq.html
@@ -11,10 +11,6 @@
   </script>
 </head>
 <body class="prettifySymbolsMode">
-  <div id="toolbar">
-    <button value="R" onclick="location.reload(true)">Refresh</button>
-    <!--<button title="Toggle prettify-symbols-mode" value="P" id="togglePrettifySymbols" onclick="togglePrettifySymbolsMode()">Prettify</button>-->
-  </div>
   <div id="measureTest"></div>
   <canvas id="textMeasurer" style="display: none"></canvas>
   <div id="states">
diff --git a/html_views/src/goals/default-proof-view.css b/html_views/src/goals/default-proof-view.css
deleted file mode 100644
index 77a9c50..0000000
--- a/html_views/src/goals/default-proof-view.css
+++ /dev/null
@@ -1,387 +0,0 @@
-html, body {
-  width:100%;
-  height:100%;
-  margin:0px;
-  padding:0px;
-  border:none;
-  position:absolute;
-  top:0px;
-  left:0px;
-  right:0px;
-  bottom:0px;
-}
-body {
-  background-color: var(--background-color);
-  font-family: var(--font-family, 'Segoe WPC','Segoe UI', SFUIText-Light, HelveticaNeue-Light, sans-serif, 'Droid Sans Fallback');
-  font-weight: var(--font-weight);
-  font-size: var(--font-size, 12pt);
-}
-body.vscode-light {
-  color: var(--color, hsl(0, 0%, 20%));
-}
-body.vscode-dark {
-  color: var(--color, hsl(0, 0%, 80%));
-}
-#messages {
-  padding: 0 10pt;
-  font-family: var(--vscode-editor-font-family);
-  font-size: var(--vscode-editor-font-size);
-}
-.vscode-dark #messages {
-  color: hsl(0, 0%, 80%);
-}
-.vscode-light #messages {
-  color: hsl(0, 0%, 20%);
-}
-#stdout {
-  padding-left: 4pt;
-}
-#error {
-  white-space: pre-wrap;
-  font-family: var(--vscode-editor-font-family);
-  font-size: var(--vscode-editor-font-size);
-  padding: 0 10pt;
-}
-.vscode-dark #error {
-  color: pink;
-}
-.vscode-light #error {
-  color: red;
-}
-.hidden {
-  display: none;
-}
-
-.prettifySymbolsMode span .substitution::before {
-  content: attr(subst);
-  font-size: 1000em;
-}
-.prettifySymbolsMode span .substitution {
-  content: attr(subst);
-  font-size: 0.001em;
-}
-
-.hypotheses {
-  border-bottom: 2pt solid;
-  padding: 0pt;
-  padding-bottom: 1em;
-}
-.vscode-dark .hypotheses {
-  border-bottom-color: hsla(0, 0%, 100%, 0.4)
-}
-.vscode-light .hypotheses {
-  border-bottom-color: hsla(0, 0%, 0%, 0.2);
-}
-.hypotheses .hypothesis .rel {
-  margin-right: 1ex;
-  margin-left: 3pt;
-}
-.vscode-dark .hypotheses .hypothesis .ident {
-  color: lightseagreen;
-}
-.vscode-light .hypotheses .hypothesis .ident {
-  color: darkgreen;
-}
-.hypotheses .hypothesis > ul {
-  list-style-type: none;
-  display: block;
-  margin-left: 0pt;
-  padding-left: 0pt;
-  text-indent: 0pt
-}
-.hypotheses > li {
-  list-style-type: none;
-  display: block;
-  padding: 2pt 10pt;
-  text-indent: 0pt
-}
-.vscode-dark .hypotheses li:nth-child(odd) {
-  background-color: hsla(0, 0%, 0%, 0.05);
-}
-.vscode-dark .hypotheses .new {
-  background-color: rgba(0,255,0,0.09) !important;
-}
-.vscode-dark .hypotheses .changed {
-  background-color: rgba(0,0,255,0.15) !important;
-}
-.vscode-light .hypotheses li:nth-child(odd) {
-  background-color: hsla(0, 0%, 100%, 0.05);
-}
-.vscode-light .hypotheses .new {
-  background-color: rgba(00,170,00,0.25) !important;
-}
-.vscode-light .hypotheses .changed {
-  background-color: rgba(0,0,255,0.05) !important;
-}
-.hypothesis {
-  white-space: nowrap;
-}
-.breakText {
-  white-space: pre;
-}
-.noBreakText .expr {
-  white-space: nowrap;
-}
-.noBreakText .ident {
-  text-decoration: underline;
-}
-/*.noBreakContainedText .breakText {
-  white-space: normal;
-}*/
-/*.noBreakContainedText .breakText .hypLine:before {
-  content: ' ';
-}*/
-/*.noBreakContainedText,.breakContainedText  {
-  opacity: 1;
-}*/
-.goal .goalId {
-  /*display: block;*/
-  margin-right: 1ex;
-}
-.vscode-dark .goal .goalId {
-  color: lightblue;
-}
-.vscode-light .goal .goalId {
-  color: darkblue;
-}
-.goal .goalId:before {
-  content: '(';
-}
-.goal .goalId:after {
-  content: ')';
-}
-.goal {
-  list-style-type: none;
-  white-space: pre;
-}
-.goal .expr {
-  display: block;
-}
-.hypotheses .new .ident {
-  font-weight: bold;
-}
-.hypotheses .changed .ident {
-  font-style: italic;
-}
-.charsAdded {
-  font-style: italic;
-}
-.vscode-dark .charsAdded {
-  background-color: rgba(0,250,0,0.1);
-}
-span[class~=charsAdded][class~=substitution]::before {
-  font-style: italic;
-}
-.vscode-dark span[class~=charsAdded][class~=substitution]::before {
-  background-color: rgba(0,250,0,0.1);
-}
-.charsRemoved {
-  text-decoration: line-through;
-}
-.vscode-dark .charsRemoved {
-  background-color: rgba(250,0,0,0.6);
-}
-span[class~=charsRemoved][class~=substitution]::before {
-  text-decoration: line-through;
-}
-.vscode-dark span[class~=charsRemoved][class~=substitution]::before {
-  background-color: rgba(250,0,0,0.6);
-}
-.vscode-light .charsAdded {
-  background-color: rgba(0,250,0,0.2);
-}
-.vscode-light span[class~=charsAdded][class~=substitution]::before {
-  background-color: rgba(0,250,0,0.2);
-}
-.vscode-light .charsRemoved {
-  background-color: rgba(250,0,0,0.2);
-}
-.vscode-light span[class~=charsRemoved][class~=substitution]::before {
-  background-color: rgba(250,0,0,0.2);
-}
-/*.vscode-light .hypotheses .expr .charsAdded {
-  color: rgba(0,180,0,1);
-} */
-/*.goal .expr .charsAdded {
-  color: lightgreen;
-}
-.vscode-light .goal .expr .charsAdded {
-  color: rgba(0,180,0,1);
-}*/
-
-.hypothesese, .hypothesis, .goal, #stdout, #textMeasurer, #measureTest {
-  font-family: var(--vscode-editor-font-family);
-  font-weight: var(--vscode-editor-font-weight);
-  font-size: var(--vscode-editor-font-size);
-}
-
-.goalsList {
-  margin-left: 0;
-  padding-left: 0;
-}
-.goalsList li:first-child {
-  background-color: inherit;
-  border-top: 0pt;
-}
-.goalsList li {
-  border-top: 1pt solid;
-  padding: 5pt 10pt;
-}
-.vscode-dark .goalsList li:first-child {
-  background-color: hsla(0, 0%, 100%, 0.05);
-}
-.vscode-light .goalsList li:first-child {
-  background-color: inherit;
-}
-.vscode-dark .goalsList li {
-  border-top-color: hsla(0, 0%, 100%, 0.2);
-}
-.vscode-light .goalsList li {
-  border-top-color: hsla(0, 0%, 0%, 0.2);
-  background-color: hsla(0, 0%, 0%, 0.05);
-}
-#measureTest {
-  display: none;
-}
-
-#toolbar {
-  display: block;
-  height: 20pt;
-  line-height: 20pt;
-  padding: 5pt 5pt;
-  margin-bottom: 10pt;
-}
-
-#toolbar button {
-  display: inline-block;
-  border-width: 1px;
-  height: 100%;
-  padding: 2pt 8pt;
-  font-size: inherit;
-  font-family: inherit;
-  outline: none;
-}
-#toolbar button:hover, #toolbar button:active {
-  cursor: pointer;
-}
-
-.vscode-dark #toolbar button {
-  background: hsla(0, 0%, 100%, 0.05);
-  border-color: hsla(0, 0%, 100%, 0.2);
-  color: hsl(0, 0%, 80%);
-}
-.vscode-light #toolbar button {
-  background: hsla(0, 0%, 0%, 0.05);
-  border-color: hsla(0, 0%, 0%, 0.2);
-  color: hsl(0, 0%, 20%);
-}
-.vscode-dark #toolbar button:hover, .vscode-light #toolbar button:active {
-  background: hsla(0, 0%, 100%, 0.1);
-}
-.vscode-light #toolbar button:hover, .vscode-light #toolbar button:active {
-  background: hsla(0, 0%, 0%, 0.1);
-}
-
-.vscode-dark .richpp .constr-notation {
-  color: darkorange;
-}
-.vscode-dark .richpp .constr-keyword {
-  color: cornflowerblue;
-}
-.vscode-dark .richpp .constr-evar {
-  color: darkorange;
-  font-style: italic;
-}
-.vscode-dark .richpp .constr-keyword {
-  color: cornflowerblue;
-}
-.vscode-dark .richpp .constr-path {
-  color: mediumpurple;
-}
-.vscode-dark .richpp .constr-reference {
-  color: lawngreen;
-}
-.vscode-dark .richpp .constr-type {
-  color: lightcoral;
-}
-.vscode-dark .richpp .constr-variable {
-  color: chartreuse;
-}
-.vscode-dark .richpp .message-debug {
-  color: mediumpurple;
-}
-.vscode-dark .richpp .message-error {
-  color: red;
-  text-decoration: underline;
-}
-.vscode-dark .richpp .message-warning {
-  color: yellow;
-}
-.vscode-dark .richpp .module-keyword {
-  color: cornflowerblue;
-}
-.vscode-dark .richpp .tactic-keyword {
-  color: cornflowerblue;
-}
-.vscode-dark .richpp .tactic-primitive {
-  color: cadetblue;
-}
-.vscode-dark .richpp .tactic-string {
-  color: orange;
-}
-
-
-.vscode-light .richpp .constr-notation {
-  color: darkorange;
-}
-.vscode-light .richpp .constr-keyword {
-  color: cornflowerblue;
-}
-.vscode-light .richpp .constr-evar {
-  color: darkorange;
-  font-style: italic;
-}
-.vscode-light .richpp .constr-keyword {
-  color: cornflowerblue;
-}
-.vscode-light .richpp .constr-path {
-  color: mediumpurple;
-}
-.vscode-light .richpp .constr-reference {
-  color: limegreen;
-}
-.vscode-light .richpp .constr-type {
-  color: coral;
-}
-.vscode-light .richpp .constr-variable {
-  color: lightseagreen;
-}
-.vscode-light .richpp .message-debug {
-  color: mediumpurple;
-}
-.vscode-light .richpp .message-error {
-  color: red;
-  text-decoration: underline;
-}
-.vscode-light .richpp .message-warning {
-  color: goldenrod;
-}
-.vscode-light .richpp .module-keyword {
-  color: cornflowerblue;
-}
-.vscode-light .richpp .tactic-keyword {
-  color: cornflowerblue;
-}
-.vscode-light .richpp .tactic-primitive {
-  color: cadetblue;
-}
-.vscode-light .richpp .tactic-string {
-  color: orange;
-}
-
-#togglePrettifySymbols {
-  text-decoration: line-through;
-}
-.prettifySymbolsMode #togglePrettifySymbols {
-  text-decoration: none
-}
diff --git a/html_views/src/goals/goals.ts b/html_views/src/goals/goals.ts
index 67e2818..e3d5b3a 100644
--- a/html_views/src/goals/goals.ts
+++ b/html_views/src/goals/goals.ts
@@ -76,32 +76,9 @@ function goalsLoad() {
   }));
 }
 
-
-let currentCSSNode : HTMLLinkElement|null = null;
-function loadCSS(filename: string) {
-  // ref: http://stackoverflow.com/questions/9979415/dynamically-load-and-unload-stylesheets
-  unloadCSS();
-  var head = document.getElementsByTagName("head")[0];
-  currentCSSNode = document.createElement('link');
-  currentCSSNode.type = 'text/css';
-  currentCSSNode.rel = 'stylesheet';
-  currentCSSNode.media = 'screen';
-  currentCSSNode.href = filename;
-  head.appendChild(currentCSSNode);
-}
-function unloadCSS() {
-  if(!currentCSSNode)
-    return;
-  var head = document.getElementsByTagName("head")[0];
-  head.removeChild(currentCSSNode);
-}
-
 function updateSettings(settings: SettingsState) : void {
-  if(settings.cssFile !== undefined)
-    loadCSS(settings.cssFile);
   if(settings.prettifySymbolsMode !== undefined)
     setPrettifySymbolsMode(settings.prettifySymbolsMode);
-
   computePrintingWidth();
 }
 
diff --git a/html_views/src/goals/proof-view.css b/html_views/src/goals/proof-view.css
new file mode 100644
index 0000000..f4257c4
--- /dev/null
+++ b/html_views/src/goals/proof-view.css
@@ -0,0 +1,221 @@
+html, body {
+  width:100%;
+  height:100%;
+  margin:0px;
+  padding:0px;
+  border:none;
+  position:absolute;
+  top:0px;
+  left:0px;
+  right:0px;
+  bottom:0px;
+}
+body {
+  background-color: var(--background-color);
+  font-family: var(--font-family, 'Segoe WPC','Segoe UI', SFUIText-Light, HelveticaNeue-Light, sans-serif, 'Droid Sans Fallback');
+  font-weight: var(--font-weight);
+  font-size: var(--font-size, 12pt);
+}
+body {
+  color: var(--vscode-coq-proofviewText);
+}
+#messages {
+  padding: 0 10pt;
+  font-family: var(--vscode-editor-font-family);
+  font-size: var(--vscode-editor-font-size);
+}
+#messages {
+  color: var(--vscode-coq-proofviewMessage);
+}
+#stdout {
+  padding-left: 4pt;
+}
+#error {
+  white-space: pre-wrap;
+  font-family: var(--vscode-editor-font-family);
+  font-size: var(--vscode-editor-font-size);
+  padding: 0 10pt;
+}
+#error {
+  color: var(--vscode-coq-proofviewError);
+}
+.hidden {
+  display: none;
+}
+
+.prettifySymbolsMode span .substitution::before {
+  content: attr(subst);
+  font-size: 1000em;
+}
+.prettifySymbolsMode span .substitution {
+  content: attr(subst);
+  font-size: 0.001em;
+}
+
+.hypotheses {
+  border-bottom: 2pt solid;
+  padding: 0pt;
+  padding-bottom: 1em;
+}
+.hypotheses {
+  border-bottom-color: var(--vscode-coq-hypothesesSeparator);
+}
+.hypotheses .hypothesis .rel {
+  margin-right: 1ex;
+  margin-left: 3pt;
+}
+.hypotheses .hypothesis .ident {
+  color: var(--vscode-coq-hypothesisIdent);
+}
+.hypotheses .hypothesis > ul {
+  list-style-type: none;
+  display: block;
+  margin-left: 0pt;
+  padding-left: 0pt;
+  text-indent: 0pt
+}
+.hypotheses > li {
+  list-style-type: none;
+  display: block;
+  padding: 2pt 10pt;
+  text-indent: 0pt
+}
+.hypotheses li:nth-child(odd) {
+  background-color: var(--vscode-coq-oddHypothesisBackground);
+}
+.hypotheses .new {
+  background-color: var(--vscode-coq-newHypothesisBackground) !important;
+}
+.hypotheses .changed {
+  background-color: var(--vscode-coq-changedHypothesisBackground) !important;
+}
+.hypothesis {
+  white-space: nowrap;
+}
+.breakText {
+  white-space: pre;
+}
+.noBreakText .expr {
+  white-space: nowrap;
+}
+.noBreakText .ident {
+  text-decoration: underline;
+}
+.goal .goalId {
+  /*display: block;*/
+  margin-right: 1ex;
+}
+.goal .goalId {
+  color: var(--vscode-coq-goalId);
+}
+.goal .goalId:before {
+  content: '(';
+}
+.goal .goalId:after {
+  content: ')';
+}
+.goal {
+  list-style-type: none;
+  white-space: pre;
+}
+.goal .expr {
+  display: block;
+}
+.hypotheses .new .ident {
+  font-weight: bold;
+}
+.hypotheses .changed .ident {
+  font-style: italic;
+}
+.charsAdded {
+  font-style: italic;
+  background-color: var(--vscode-coq-addedCharacter);
+}
+span[class~=charsAdded][class~=substitution]::before {
+  font-style: italic;
+  background-color: var(--vscode-coq-addedCharacter);
+}
+.charsRemoved {
+  text-decoration: line-through;
+  background-color: var(--vscode-coq-removedCharacter);
+}
+span[class~=charsRemoved][class~=substitution]::before {
+  text-decoration: line-through;
+  background-color: var(--vscode-coq-removedCharacter);
+}
+
+.hypothesese, .hypothesis, .goal, #stdout, #textMeasurer, #measureTest {
+  font-family: var(--vscode-editor-font-family);
+  font-weight: var(--vscode-editor-font-weight);
+  font-size: var(--vscode-editor-font-size);
+}
+
+.goalsList {
+  margin-left: 0;
+  padding-left: 0;
+}
+.goalsList li:first-child {
+  background-color: var(--vscode-coq-mainSubgoalBackground);
+  border-top: 0pt;
+}
+.goalsList li {
+  background-color: var(--vscode-coq-subgoalBackground);
+  border-top: 1pt solid;
+  padding: 5pt 10pt;
+  border-top-color: var(--vscode-coq-subgoalSeparator);
+}
+#measureTest {
+  display: none;
+}
+
+.richpp .constr-notation {
+  color: var(--vscode-coq-termNotation);
+}
+.richpp .constr-keyword {
+  color: var(--vscode-coq-termKeyword);
+}
+.richpp .constr-evar {
+  color: var(--vscode-coq-termEvar);
+  font-style: italic;
+}
+.richpp .constr-path {
+  color: var(--vscode-coq-termPath);
+}
+.richpp .constr-reference {
+  color: var(--vscode-coq-termReference);
+}
+.richpp .constr-type {
+  color: var(--vscode-coq-termType);
+}
+.richpp .constr-variable {
+  color: var(--vscode-coq-termVariable);
+}
+.richpp .message-debug {
+  color: var(--vscode-coq-debugMessage);
+}
+.richpp .message-error {
+  color: var(--vscode-coq-errorMessage);
+  text-decoration: underline;
+}
+.richpp .message-warning {
+  color: var(--vscode-coq-warningMessage);
+}
+.richpp .module-keyword {
+  color: var(--vscode-coq-moduleKeyword);
+}
+.richpp .tactic-keyword {
+  color: var(--vscode-coq-tacticKeyword);
+}
+.richpp .tactic-primitive {
+  color: var(--vscode-coq-tacticPrimitive);
+}
+.richpp .tactic-string {
+  color: var(--vscode-coq-tacticString);
+}
+
+#togglePrettifySymbols {
+  text-decoration: line-through;
+}
+.prettifySymbolsMode #togglePrettifySymbols {
+  text-decoration: none
+}
diff --git a/html_views/src/goals/protocol.ts b/html_views/src/goals/protocol.ts
index 2934006..1db3921 100644
--- a/html_views/src/goals/protocol.ts
+++ b/html_views/src/goals/protocol.ts
@@ -19,7 +19,6 @@ export interface SettingsState {
   fontFamily?: string,
   fontSize?: string,
   fontWeight?: string,
-  cssFile?: string,
   prettifySymbolsMode?: boolean,
 }
 
diff --git a/html_views/src/ltacprof/LtacProf.html b/html_views/src/ltacprof/LtacProf.html
index e4487c9..ee5272d 100644
--- a/html_views/src/ltacprof/LtacProf.html
+++ b/html_views/src/ltacprof/LtacProf.html
@@ -106,29 +106,6 @@
 table.rc-table-resizing thead > th > a {
   cursor: ew-resize;
 }*/
-    #toolbar {
-      display: block;
-      margin: 0px 0px 0px 0px;
-      position: fixed;
-      height: 1em;
-      top: 0px;
-      left: 0px;
-      right: 0px;
-      z-index: 1000;
-    }
-    #toolbar button {
-      background: none;
-      border-color: blue;
-      border-width: 1px;
-      height: 1.5em;
-      min-width: 1.5em;
-      color: green;
-      padding: 0pt;
-      font-size: 8pt;
-    }
-    #toolbar-placeholder {
-      height: 1em;
-    }
 
     #local-unit, #total-unit {
       -moz-appearance: none;
@@ -206,11 +183,6 @@
   <script src="ltacprof.js"></script>
 </head>
 <body onload="ltacProfLoad()">
-  <div id="toolbar">
-    <button value="R" onclick="location.reload(true)">Refresh</button>
-    <button value="C" onclick="clearResults()">Clear</button>
-  </div>
-  <div id="toolbar-placeholder"></div>
   <!--<table id="sticky-results-header">
     <thead>
     <tr><th>tactic</th><th>total (s)</th><th>local (s)</th><th>#calls</th><th>max total (s)</th></tr>