diff --git a/client/public/fonts/JuliaMono-Regular.ttf b/client/public/fonts/JuliaMono-Regular.ttf new file mode 100644 index 00000000..30b84f3c Binary files /dev/null and b/client/public/fonts/JuliaMono-Regular.ttf differ diff --git a/client/public/fonts/LICENSE-JuliaMono b/client/public/fonts/LICENSE-JuliaMono new file mode 100644 index 00000000..cc69da81 --- /dev/null +++ b/client/public/fonts/LICENSE-JuliaMono @@ -0,0 +1,93 @@ +Copyright (c) 2020 - 2023, cormullion +with Reserved Font Name JuliaMono. + +This Font Software is licensed under the SIL Open Font License, Version 1.1. +This license is copied below, and is also available with a FAQ at: +http://scripts.sil.org/OFL + +----------------------------------------------------------- +SIL OPEN FONT LICENSE Version 1.1 - 26 February 2007 +----------------------------------------------------------- + +PREAMBLE +The goals of the Open Font License (OFL) are to stimulate worldwide +development of collaborative font projects, to support the font creation +efforts of academic and linguistic communities, and to provide a free and +open framework in which fonts may be shared and improved in partnership +with others. + +The OFL allows the licensed fonts to be used, studied, modified and +redistributed freely as long as they are not sold by themselves. The +fonts, including any derivative works, can be bundled, embedded, +redistributed and/or sold with any software provided that any reserved +names are not used by derivative works. The fonts and derivatives, +however, cannot be released under any other type of license. The +requirement for fonts to remain under this license does not apply +to any document created using the fonts or their derivatives. + +DEFINITIONS +"Font Software" refers to the set of files released by the Copyright +Holder(s) under this license and clearly marked as such. This may +include source files, build scripts and documentation. + +"Reserved Font Name" refers to any names specified as such after the +copyright statement(s). + +"Original Version" refers to the collection of Font Software components as +distributed by the Copyright Holder(s). + +"Modified Version" refers to any derivative made by adding to, deleting, +or substituting -- in part or in whole -- any of the components of the +Original Version, by changing formats or by porting the Font Software to a +new environment. + +"Author" refers to any designer, engineer, programmer, technical +writer or other person who contributed to the Font Software. + +PERMISSION & CONDITIONS +Permission is hereby granted, free of charge, to any person obtaining +a copy of the Font Software, to use, study, copy, merge, embed, modify, +redistribute, and sell modified and unmodified copies of the Font +Software, subject to the following conditions: + +1) Neither the Font Software nor any of its individual components, +in Original or Modified Versions, may be sold by itself. + +2) Original or Modified Versions of the Font Software may be bundled, +redistributed and/or sold with any software, provided that each copy +contains the above copyright notice and this license. These can be +included either as stand-alone text files, human-readable headers or +in the appropriate machine-readable metadata fields within text or +binary files as long as those fields can be easily viewed by the user. + +3) No Modified Version of the Font Software may use the Reserved Font +Name(s) unless explicit written permission is granted by the corresponding +Copyright Holder. This restriction only applies to the primary font name as +presented to the users. + +4) The name(s) of the Copyright Holder(s) or the Author(s) of the Font +Software shall not be used to promote, endorse or advertise any +Modified Version, except to acknowledge the contribution(s) of the +Copyright Holder(s) and the Author(s) or with their explicit written +permission. + +5) The Font Software, modified or unmodified, in part or in whole, +must be distributed entirely under this license, and must not be +distributed under any other license. The requirement for fonts to +remain under this license does not apply to any document created +using the Font Software. + +TERMINATION +This license becomes null and void if any of the above conditions are +not met. + +DISCLAIMER +THE FONT SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO ANY WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT +OF COPYRIGHT, PATENT, TRADEMARK, OR OTHER RIGHT. IN NO EVENT SHALL THE +COPYRIGHT HOLDER BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, +INCLUDING ANY GENERAL, SPECIAL, INDIRECT, INCIDENTAL, OR CONSEQUENTIAL +DAMAGES, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING +FROM, OUT OF THE USE OR INABILITY TO USE THE FONT SOFTWARE OR FROM +OTHER DEALINGS IN THE FONT SOFTWARE. diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx index 2c696579..caf5c4ea 100644 --- a/client/src/Editor.tsx +++ b/client/src/Editor.tsx @@ -79,7 +79,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: tabSize: 2, 'semanticHighlighting.enabled': true, theme: 'vs', - wordWrap: config.wordWrap + wordWrap: config.wordWrap ? "on" : "off", + fontFamily: "JuliaMono", }) setEditor(editor) const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor) diff --git a/client/src/css/index.css b/client/src/css/index.css index 7f0e5fdd..d94cc178 100644 --- a/client/src/css/index.css +++ b/client/src/css/index.css @@ -8,3 +8,8 @@ body { #root { height: 100vh; } + +@font-face { + font-family: 'JuliaMono'; + src: local('JuliaMono'), url('./fonts/JuliaMono-Regular.ttf') format('truetype'); +} diff --git a/client/src/editor/leanclient.ts b/client/src/editor/leanclient.ts index 8073cf97..1f31b0fc 100644 --- a/client/src/editor/leanclient.ts +++ b/client/src/editor/leanclient.ts @@ -103,6 +103,7 @@ export class LeanClient implements Disposable { console.log(`[LeanClient] Restarting Lean Server with project ${project}`) if (this.isStarted()) { + // TODO: This times out in lean4game... await this.stop() } diff --git a/client/src/editor/vscode.css b/client/src/editor/vscode.css index 482ec977..6a66366d 100644 --- a/client/src/editor/vscode.css +++ b/client/src/editor/vscode.css @@ -1,7 +1,7 @@ :root { --vscode-font-weight:normal; --vscode-font-size:13px; - --vscode-editor-font-family: 'Source Code Pro', 'STIX Two Math', monospace; + --vscode-editor-font-family: 'JuliaMono', 'Source Code Pro', 'STIX Two Math', monospace; --vscode-editor-font-weight:normal; --vscode-editor-font-size:15px; --vscode-foreground: #616161; diff --git a/client/src/index.tsx b/client/src/index.tsx index 4702530b..e18897df 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -2,6 +2,7 @@ import * as React from 'react'; import { createRoot } from 'react-dom/client'; import './css/index.css'; import App from './App'; +// import './fonts/JuliaMono-Regular.ttf'; const container = document.getElementById('root'); const root = createRoot(container!);