[isabelle-dev] NEWS: Isabelle/VSCode

Mathias Fleury mathias.fleury at ens-rennes.fr
Mon Jul 3 16:11:07 CEST 2017


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 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-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/685ea8f7/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 842 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170703/685ea8f7/attachment.sig>


More information about the isabelle-dev mailing list