Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

REPL doesn't use configured font #191

Open
DjebbZ opened this issue Oct 11, 2017 · 2 comments
Open

REPL doesn't use configured font #191

DjebbZ opened this issue Oct 11, 2017 · 2 comments

Comments

@DjebbZ
Copy link

DjebbZ commented Oct 11, 2017

Hello,

First : thank you for the package ! Really nice to learn Idris with the book "Type-Driven development with Idris".

Second : it may be related to #139, but the panel doesn't use the configured font. I'm using Fira Code for the ligatures.

I tried the following in the Application : open your Stylesheet (styles.less), with strictly no change :

.atom-panel {
  font-size: 20px;
  font-family: "Fira Code";
}

.tool-panel {
  font-size: 20px;
  font-family: "Fira Code";
}

.panel-heading {
  font-size: 20px;
  font-family: "Fira Code";
}

.line-message .preview {
  font-size: 20px;
  font-family: "Fira Code";
}

Using Atom 1.20.1 on Linux and your plugin v0.4.10.

Feel free to close the ticket if you consider it a duplicate of #139 and/or that I am a "help vampire".

@justjoheinz
Copy link
Contributor

I have been experimenting a bit with


.idris-panel {
  font-family: firacode-retina
}
 .idris-repl-output {
   font-family: firacode-retina
 }

which seems to go into the right direction (Max OS X, which might explain the "-retina" add on. If you get it working properly, please post your results here.

For the main editor I have been using firacode without the need to adjust anything in the stylesheets, btw.

@peterb12
Copy link

Please this, yes.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants