Re: [isabelle-dev] NEWS: Isabelle/VSCode

[Makarius]

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

[Simon Wimmer]

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 
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 "\\<^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

[Mathias Fleury]

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

[Christian Sternagel]

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

[Makarius]

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

[Christian Sternagel]

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

[Makarius]

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

[Christian Sternagel]

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

[Makarius Wenzel]

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

[Makarius]

*** 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