## Stream: general

### Topic: documentation view

#### Patrick Massot (Jan 15 2019 at 08:05):

@Gabriel Ebner What happened to the documentation view feature of vscode-lean?

#### Gabriel Ebner (Jan 15 2019 at 08:38):

@Patrick Massot I'm a bit busy at the moment so there's nothing new (though it's available in the released version now). In the other thread you suggested that the documentation view should have back/forward buttons and a way to input your own url. I completely agree. (The webview api in vscode is unfortunately really, really stripped down... Not even hyperlinks work by default, we are changing them to vscode commands on the fly....)
@Edward Ayers if you want to look at this, I can give you pointers.

#### Gabriel Ebner (Jan 15 2019 at 08:39):

In case anybody has too much free time and wants to give feedback, run "ctrl+shift+p open documentation view" and post your complaints here.

#### Patrick Massot (Jan 15 2019 at 08:42):

Thanks Gabriel! Did you intend to ping Bryan instead of Ed?

#### Patrick Massot (Jan 15 2019 at 08:43):

@Jeremy Avigad Did you see that feature?

#### Gabriel Ebner (Jan 15 2019 at 08:44):

No, Ed asked me in Amsterdam to please give him work on the vscode extension. But I'm happy about contributions from all sides.

#### Patrick Massot (Jan 15 2019 at 08:47):

By the way, am I correct in thinking that this was not in the previous release? If not then please forgive me for asking today

#### Gabriel Ebner (Jan 15 2019 at 08:50):

I made a release for Ed's translations PR yesterday, that's the first release with the documentation view.

#### Patrick Massot (Jan 15 2019 at 08:53):

Weird... I did try to check before posting. Sorry

#### Jeremy Avigad (Jan 16 2019 at 02:51):

I just tried documentation view. It's great! Here are two comments.

The bigger one: once we move from the table of contents to a specific chapter, as far as I can tell it is impossible to go back to the table of contents without pressing ctrl-shift-P and choosing "open documentation view" again. That makes it less convenient to browse. I don't know the ideal solution here. Maybe the best solution is to assign a keystroke to "open documentation view", so that pressing that would return to the TOC.

The smaller issue: the natural way to play with the text and examples is to split the screen, put the text in the left, and then run the examples in the right. But even when I have a split screen, when I click on the "try it" button, the window opens on the left, and I have to manually move it to the right. Would it be possible to have the window open on the right?

#### Patrick Massot (Jan 31 2019 at 10:47):

I just tried to use the VScode Lean documentation view in our computer rooms, with no success. Could it be that it tries to access TPIL without using the system-wide proxy setup?

#### Patrick Massot (Jan 31 2019 at 10:48):

@Edward Ayers @Gabriel Ebner

#### Gabriel Ebner (Jan 31 2019 at 10:48):

Yes, I'm pretty sure it doesn't look at proxy settings.

#### Patrick Massot (Jan 31 2019 at 10:49):

Fixing this would be a nice improvement

#### Edward Ayers (Jan 31 2019 at 11:01):

Did you have to set the http.proxy in the vscode settings for the extension downloading to work?

#### Gabriel Ebner (Jan 31 2019 at 11:02):

Ideally, we could use the system proxy settings that vscode uses itself, but it looks like this is not possible yet: https://github.com/Microsoft/vscode/issues/12588

#### Gabriel Ebner (Jan 31 2019 at 11:03):

The http.proxy* settings are the older (now deprecated) way to set the proxy in vscode (and it is ignored by most of vscode). We could use this setting (but Patrick needs to set it).

#### Patrick Massot (Jan 31 2019 at 11:05):

I didn't have to set anything to get the extension

#### Gabriel Ebner (Jan 31 2019 at 11:06):

@Patrick Massot vscode has two settings for proxies: one is taken directly from the system settings and is used for extension fetching, etc. But this is unfortunately not accessible to extensions (i.e., us).

#### Kevin Buzzard (Jan 31 2019 at 11:35):

issues/12588. Wow -- and I thought we had issues.

#### Kevin Buzzard (Jan 31 2019 at 11:37):

When there are 4621 open issues, how do you get people to work on the one you want to be fixed?

#### Mario Carneiro (Jan 31 2019 at 11:41):

in big companies the issues process has to be a lot more formal. There is triage and tagging, periodic review of priorities, and work is often aimed for milestones. Quite often the issues system is the force behind all work - i.e. if you want to change something you should make an issue first, so that the intent is logged and prioritized

#### Mario Carneiro (Jan 31 2019 at 11:42):

so you have people working on the most important things and other people adding and organizing new issues

#### Mario Carneiro (Jan 31 2019 at 11:44):

For a big github project, you can vote on your favorite issues by adding a thumbs up reaction to it; this sometimes helps, depending on the team, but it's just a suggestion

#### Mario Carneiro (Jan 31 2019 at 11:46):

apparently people really want floating windows https://github.com/Microsoft/vscode/issues?q=is%3Aopen+is%3Aissue+sort%3Areactions-%2B1-desc

Last updated: May 10 2021 at 00:31 UTC