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
Re: [isabelle-dev] NEWS: Isabelle/VSCode
Dear Makarius, I've already occasionally peeked into your Isabelle/VSCode commits before. For me Isabelle/VSCode it works out of the box (after installing VSCode via the package system of my operating system). It only took me some time to find the OUTPUT "panel" (View ~> Output) ;) cheers chris On 07/01/2017 07:36 PM, 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 > ___ 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
Re: [isabelle-dev] [isabelle] Good name for "sublist" predicates
Just for the record: * Topological_Spaces.subseq has already been present before 2007 in HOL/Hyperreal/SEQ.thy (cf. eb85850d3eb7) * strict_mono has entered in 2009, see abefe1dfadbb Hence we have the typical situation that a generalized constant subsumes a more ancient unconsciously. Cheers, Florian Am 30.06.2017 um 20:41 schrieb Manuel Eberl: > On 2017-06-30 20:33, Sebastien Gouezel wrote: >> I used subseq quite heavily in my ergodic theory developments. From >> a mathematician point of view, taking subsequences of sequences >> from nat to nat is very common and very useful in analysis (much >> more than taking subsequences of lists). > > So what about the suggestion of just writing "strict_mono" instead? > Besides, you can always introduce local abbreviations for things with > "notation" and delete them with "no_notation" afterwards. > >> By the way, I recently encountered a similar (and even more nasty) >> name clash, with compact. The following works perfectly > > It's "Topological_Spaces.compact" and that should definitely work. We > should probably make the one from Complete_Partial_Order2 qualified. In > my opinion, there is no question that "compact" should be "compact" in > the topological sense. > > Cheers, > > Manuel > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
