Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 03/07/17 21:14, Simon Wimmer wrote: > > One thing that disturbed me in the beginning was that I first have to > edit a document before any symbols get prettified. This might be a weakness of the Prettify Symbols Mode, or just a mistake in setting it up on my side. (For months, I have not heard anything from its author CJ Bell, who is also the guy behind VSCoq.) In the section about limitations in src/Tools/VSCode/extension/README.md, I wrote: * Isabelle symbols are merely an optical illusion: it would be better to make them a first-class Unicode charset as in Isabelle/jEdit. This would also solve the Unicode copy-paste confusion, and make it work as in Isabelle/jEdit. Doing that might require a small patch here https://github.com/Microsoft/vscode/blob/master/src/vs/base/node/encoding.ts and then to rebuild/rebrand/repackage the whole VSCode/Electron application. I still need to figure out how this works in the first place ... Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
Hi Makarius, the same goes for me. Installing and running this worked without any trouble when following your instructions. One thing that disturbed me in the beginning was that I first have to edit a document before any symbols get prettified. Simon On Mon, Jul 3, 2017 at 4:11 PM Mathias Fleurywrote: > Dear Makarius, > > I am using Isabelle/VSCode code for a week now. So it is possible to > install and use it. > > > I mostly like it: > >- I really like VSCode's Control-P to search for commands. > >- the PIDE protocol, unlike "isabelle build", accepts unicode >characters: If the file contains "×⇩r" instead of "\\<^sub>r" (e.g. >because I copy-pasted it) , Isabelle/jEdit and Isabelle/VSCode will accept >the expression, but "isabelle build" will fail. It took a long time to >figure that out, since in Iaabelle/jEdit, the symbols are shown in the same >fashion. > >- there are some weird slow-downs: Every once in a while, >refreshing/jumping to the definition take several seconds. I am not yet >sure whether Isabelle or VSCode is responsible. > > > Mathias > > > > On 01.07.17 19:36, Makarius wrote: > > *** General *** > > * Experimental support for Visual Studio Code (VSCode) as alternative > Isabelle/PIDE front-end, see > alsohttps://marketplace.visualstudio.com/items?itemName=makarius.isabelle > > VSCode is a new type of application that continues the concepts of > "programmer's editor" and "integrated development environment" towards > fully semantic editing and debugging -- in a relatively light-weight > manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure. > Technically, VSCode is based on the Electron application framework > (Node.js + Chromium browser + V8), which is implemented in JavaScript > and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala > modules around a Language Server implementation. > > > This refers to Isabelle/8f39d60b943d. The marketplace link above also > shows a screenshot. > > I am interested to hear if anybody manages to run the application: > presently it lacks the all-inclusive application bundling of Isabelle/jEdit. > > > Makarius > ___ > isabelle-dev mailing > listisabelle-...@in.tum.dehttps://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
Dear Makarius, I am using Isabelle/VSCode code for a week now. So it is possible to install and use it. I mostly like it: * I really like VSCode's Control-P to search for commands. * the PIDE protocol, unlike "isabelle build", accepts unicode characters: If the file contains "×⇩r" instead of "\\<^sub>r" (e.g. because I copy-pasted it) , Isabelle/jEdit and Isabelle/VSCode will accept the expression, but "isabelle build" will fail. It took a long time to figure that out, since in Iaabelle/jEdit, the symbols are shown in the same fashion. * there are some weird slow-downs: Every once in a while, refreshing/jumping to the definition take several seconds. I am not yet sure whether Isabelle or VSCode is responsible. Mathias On 01.07.17 19:36, Makarius wrote: > *** General *** > > * Experimental support for Visual Studio Code (VSCode) as alternative > Isabelle/PIDE front-end, see also > https://marketplace.visualstudio.com/items?itemName=makarius.isabelle > > VSCode is a new type of application that continues the concepts of > "programmer's editor" and "integrated development environment" towards > fully semantic editing and debugging -- in a relatively light-weight > manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure. > Technically, VSCode is based on the Electron application framework > (Node.js + Chromium browser + V8), which is implemented in JavaScript > and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala > modules around a Language Server implementation. > > > This refers to Isabelle/8f39d60b943d. The marketplace link above also > shows a screenshot. > > I am interested to hear if anybody manages to run the application: > presently it lacks the all-inclusive application bundling of Isabelle/jEdit. > > > Makarius > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 07/02/2017 10:59 PM, Makarius wrote: > On 02/07/17 22:16, Christian Sternagel wrote: >> >>> It should work analogously to the "Preview" button, but without having a >>> button. >> >> Preview (more concretely the "Open Preview" "button" -- some kind of >> magnifying glass icon where the rest is to tiny to discern) only gives >> me a white box with a very light gray copy of the theory file content. > > Odd. Is this really Isabelle_01-Jul-2017 as described in README.md -- or > alternatively current Isabelle/453f9cabddb5 ? The isabelle.home settings > of VSCode needs to point to the currect ISABELLE_HOME directory. Oh, I overlooked this part. I was still on ded1c636aece (the first version where I started looking into Isabelle/VSCode and did no longer remember README.md; but there where no error messages). Now I am on 453f9cabddb5. Sorry for that. > > You've also said that your VSCode is from the OS package repository. > Maybe it is better to use the official > https://code.visualstudio.com/Download I also updated VSCode (through its own interface) to the latest version from the above link. Now it works like you suggested. chris > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 02/07/17 22:16, Christian Sternagel wrote: > >> It should work analogously to the "Preview" button, but without having a >> button. > > Preview (more concretely the "Open Preview" "button" -- some kind of > magnifying glass icon where the rest is to tiny to discern) only gives > me a white box with a very light gray copy of the theory file content. Odd. Is this really Isabelle_01-Jul-2017 as described in README.md -- or alternatively current Isabelle/453f9cabddb5 ? The isabelle.home settings of VSCode needs to point to the currect ISABELLE_HOME directory. You've also said that your VSCode is from the OS package repository. Maybe it is better to use the official https://code.visualstudio.com/Download Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 07/02/2017 02:21 PM, Makarius wrote: > On 02/07/17 13:31, Christian Sternagel wrote: >> On 07/01/2017 09:21 PM, Makarius Wenzel wrote: >>> There is also a "State" panel that imitates the dockable of the same >>> name in Isabelle/jEdit. You will get to that via the "isabelle.state" >>> command, e.g. use the SHIFT-CONTROL-P command palette and search for >>> "Isabelle" commands. It has the description "Show State". >> >> Nothing happens when I select (by clicking) "Isabelle: Show State" after >> SHIFT-CONTROL-P and searching for "Isabelle". > > You need to have an active theory file (with running prover process). I think I do (at least in "View ~> Output" I see subgoals when moving through a proof). > > It should work analogously to the "Preview" button, but without having a > button. Preview (more concretely the "Open Preview" "button" -- some kind of magnifying glass icon where the rest is to tiny to discern) only gives me a white box with a very light gray copy of the theory file content. chris > > > Makarius > ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 02/07/17 13:31, Christian Sternagel wrote: > On 07/01/2017 09:21 PM, Makarius Wenzel wrote: >> There is also a "State" panel that imitates the dockable of the same >> name in Isabelle/jEdit. You will get to that via the "isabelle.state" >> command, e.g. use the SHIFT-CONTROL-P command palette and search for >> "Isabelle" commands. It has the description "Show State". > > Nothing happens when I select (by clicking) "Isabelle: Show State" after > SHIFT-CONTROL-P and searching for "Isabelle". You need to have an active theory file (with running prover process). It should work analogously to the "Preview" button, but without having a button. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 07/01/2017 09:21 PM, Makarius Wenzel wrote: > On 01.07.17 20:46, Christian Sternagel wrote: >> >> It only took me some time to find the OUTPUT "panel" (View ~> Output) ;) > > That is a plain-text channel of VSCode. Oh, okay. > > There is also a "State" panel that imitates the dockable of the same > name in Isabelle/jEdit. You will get to that via the "isabelle.state" > command, e.g. use the SHIFT-CONTROL-P command palette and search for > "Isabelle" commands. It has the description "Show State". Nothing happens when I select (by clicking) "Isabelle: Show State" after SHIFT-CONTROL-P and searching for "Isabelle". chris > > Wiring up that GUI panel required a whole lot of tricks, but it should > be now trivial to make more panels. Although, this poses the problem of > multi-window management. > > > Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Isabelle/VSCode
On 01.07.17 20:46, Christian Sternagel wrote: It only took me some time to find the OUTPUT "panel" (View ~> Output) ;) That is a plain-text channel of VSCode. There is also a "State" panel that imitates the dockable of the same name in Isabelle/jEdit. You will get to that via the "isabelle.state" command, e.g. use the SHIFT-CONTROL-P command palette and search for "Isabelle" commands. It has the description "Show State". Wiring up that GUI panel required a whole lot of tricks, but it should be now trivial to make more panels. Although, this poses the problem of multi-window management. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: Isabelle/VSCode
*** General *** * Experimental support for Visual Studio Code (VSCode) as alternative Isabelle/PIDE front-end, see also https://marketplace.visualstudio.com/items?itemName=makarius.isabelle VSCode is a new type of application that continues the concepts of "programmer's editor" and "integrated development environment" towards fully semantic editing and debugging -- in a relatively light-weight manner. Thus it fits nicely on top of the Isabelle/PIDE infrastructure. Technically, VSCode is based on the Electron application framework (Node.js + Chromium browser + V8), which is implemented in JavaScript and TypeScript, while Isabelle/VSCode mainly consists of Isabelle/Scala modules around a Language Server implementation. This refers to Isabelle/8f39d60b943d. The marketplace link above also shows a screenshot. I am interested to hear if anybody manages to run the application: presently it lacks the all-inclusive application bundling of Isabelle/jEdit. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev