Skip to content

Commit

Permalink
Merge pull request siegebell#54 from maximedenes/customize-proofview
Browse files Browse the repository at this point in the history 
Remove proofview customization logic and expose themable colors instead
  • Loading branch information
@maximedenes
maximedenes authored Sep 19, 2019
2 parents d298a4e + ede81e6 commit bdd4b52
Show file tree
Hide file tree
Showing 11 changed files with 476 additions and 556 deletions.
264 changes: 254 additions & 10 deletions client/package.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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."
}
}
},
Expand Down Expand Up @@ -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": [
Expand Down Expand Up @@ -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": {
Expand Down
52 changes: 1 addition & 51 deletions client/src/HtmlCoqView.ts
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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');
Expand All @@ -33,7 +32,6 @@ interface SettingsState {
fontFamily?: string,
fontSize?: string,
fontWeight?: string,
cssFile?: string,
prettifySymbolsMode?: boolean,
}

Expand All @@ -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)));
}
Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -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());
}
}
}
}
Loading

0 comments on commit bdd4b52

Please sign in to comment.