[isabelle-dev] NEWS: Isabelle/VSCode

Simon Wimmer wimmersimon at gmail.com
Mon Jul 3 21:14:41 CEST 2017


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 Fleury <mathias.fleury at ens-rennes.fr>
wrote:

> 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 "\<times>\<^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-dev at in.tum.dehttps://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170703/8f6f7e1b/attachment-0002.html>


More information about the isabelle-dev mailing list