Re: [isabelle-dev] NEWS: Dockable window Find
On 09/23/2013 01:25 PM, Makarius wrote: On Fri, 20 Sep 2013, Holger Gast wrote: The layers 2+3 offer extensive means of customization. To come back to the above example, one does, of course, not set StyleRanges on the SWT widget oneself. One registers with the JFace TextViewer's syntax highlighting mechanism and produces them on demand -- for instance from the semantic markup offered by Isabelle/Scala. Again: Why not make this practical, and tell Andrius Velykis about it? He has already Isabelle/Eclipse that is more than just a proof of concept or a small demo, so it deserves to catch up with the quality standards of Isabelle/jEdit. I'm sure there is no need to explain such elementary facts as the Eclipse/JFace/SWT layers and their respective responsibilities to Andrius. My motivation for outlining the Eclipse stack in some detail here is quite simply that I wished to motivate people to consider writing UIs for their own Isabelle applications. Wouldn't it be great if we saw more C/Java/... verification tools integrated with the Eclipse CDT/JDT/... environment? (One of my students has shown that it can be done for C, Java should be even simpler; the basis was the model layer of I3P.) Such integrations would foster the interest of practitioners in theorem proving, which would certainly be desirable. The prerequisite for such developments is, however, that people are not scared away from UI programming by statements such as all existing frameworks being crap, their developers being evil companies, and that it is imperative to read through tons of sources to achieve one's goals. Depending on the sources introduces tight coupling anyway, which in turn leads to dependencies on specific versions of the JDK and ensuing portability issues. In reality, due to its long history and high practical relevance, UI programming is one of the best understood areas in software development. The available tool support (Netbeans' Matisse or Eclipse's WindowBuilder) makes it very simple to get panels up quickly. The editing frameworks of both Netbeans and Eclipse are very mature. As long as one adheres conscientiously to the contracts stated in the frameworks' documentation, there's no need to understand the sources. Anyway, this thread is going in circles, back to the point where it started 5 years ago. The only difference is that Isabelle/jEdit has become real in the meantime Well, there are other differences: I3P has (long since) become a reality and has actually been used by others, in different environments, and has even been built upon in Matej Urbas' Diabelli project [1]. Thanks to the well-designed and stable Netbeans infrastructure, there have never been any portability problems. I do agree, however, that there are certain circles in the discussion due to fundamentally different approaches to UI programming. I hope to have contributed, at least, a second opinion on the topic as taken from the literature on Swing [2], Netbeans [3], and Eclipse [4]. Cheers, Holger [1] Urbas and Jamnik: Diabelli: a heterogeneous proof system, IJCAR 2012. [2] Eckstein et al. Java Swing, O'Reilly. [3] Boudreau et al.: Rich Client Programming: Plugging into the Netbeans platform, Prentice Hall. [4] McAffer et al.: Eclipse Rich Client Platform, Addison-Wesley ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Preferences on Mac OS X
On Wed, 25 Sep 2013, Andrew Boyton wrote: The fact that Isabelle/jEdit doesn't obey the standard OS X keybindings is frustrating but sadly typical for a Java application. For a Mac application I expect Command+, to bring up the preferences, but I also expect the preferences to be in the menu jEdit - Preferences, like every other Mac application. I do accept though that Java applications are rarely good citizens on any platform, and so am not surprised. There is a long story behind Mac OS X + Java not working quite as well as on other platforms, and many parties are to blame for it: Sun, Apple, Oracle, as well as the average Mac user who is not very active in supporting open source projects to get it really right. I have myself started to use Mac OS X part-time in 2008 to make up for this. Right now I have initiated some activity on the jEdit Sourceforge project to get things into shape for Java 7. To make jEdit a really good citizen on Mac OS X, the inhabitants of that platform need to do something. Neither Apple nor Oracle have the resources to make it just work out of the box. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Tue, 24 Sep 2013, Lawrence Paulson wrote: my issue has nothing to do with editing the surrounding text. On the contrary, it has to do with activating s/h, walking away from the computer, and coming back to find that sendback does not work. Now I understand what you mean. I've addresses this here: changeset: 53867:6e69f9ca8f1c user:wenzelm date:Wed Sep 25 11:12:59 2013 +0200 files: src/Pure/PIDE/query_operation.scala src/Tools/jEdit/src/find_dockable.scala src/Tools/jEdit/src/sledgehammer_dockable.scala description: explicit Status.REMOVED, which is required e.g. for sledgehammer to retrieve command of sendback exec_id (in contrast to find_theorems, see c2da0d3b974d); Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit doesn't process theories
On Wed, 25 Sep 2013, Jasmin Christian Blanchette wrote: Isabelle/jEdit is currently unwilling to process theories The file is correctly opened, but nothing is processed -- no imports are processed, the theory text has a pink background, etc. I think you have merely disabled Continuous checking by accident. So this is another instance of the two many modes problem. These days I have quite often the Theories panel on, where this status is directly visible. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle/jEdit doesn't process theories
Am 25.09.2013 um 13:03 schrieb Makarius makar...@sketis.net: On Wed, 25 Sep 2013, Jasmin Christian Blanchette wrote: Isabelle/jEdit is currently unwilling to process theories The file is correctly opened, but nothing is processed -- no imports are processed, the theory text has a pink background, etc. I think you have merely disabled Continuous checking by accident. So this is another instance of the two many modes problem. Indeed, this is exactly what happened. Perhaps it's one of those options that should not be remembered across sessions? This reminds me of this little very similar story: http://textmate.1073791.n5.nabble.com/New-behavior-moving-cursor-pass-end-of-line-td16179.html Jasmin ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Dockable window Find
On Wed, 25 Sep 2013, Holger Gast wrote: In reality, due to its long history and high practical relevance, UI programming is one of the best understood areas in software development. The available tool support (Netbeans' Matisse or Eclipse's WindowBuilder) makes it very simple to get panels up quickly. The editing frameworks of both Netbeans and Eclipse are very mature. As long as one adheres conscientiously to the contracts stated in the frameworks' documentation, there's no need to understand the sources. This is probably quoted from some marketing brochure. In reality it works differently: guessing how it actually works, Googling, asking on forums, asking of stackexchange, looking through sources (if available). The reason why this strange mainstream stuff like Java and Swing is still being used successfully is the amount of explanations found on the Web. I3P has (long since) become a reality and has actually been used by others, in different environments, and has even been built upon in Matej Urbas' Diabelli project [1]. So is I3P still maintained? Its latest release is for Isabelle2012 -- 10.6.2012. Since I3P uses APIs of Isabelle that were never public, have changed several times, and are about to disappear, it is getting more and more difficult. Thanks to the well-designed and stable Netbeans infrastructure, there have never been any portability problems. Netbeans is in the same boat with Swing incompatibilities. It is actually the Netbeans community that is most active to point out to Oracle what is still missing to make it half-decent on all platforms. This is also how proper support for Mac OS X Retina displays now got into jdk-7u40 -- only with 6 months delay, so really quick for Java standards. I think they did that relatively promptly, because bad visual quality is immediately visible to anybody, without understanding general software quality. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Preferences on Mac OS X
Another Mac user has pointed out full-screen support. After the recent renewal of Mac OS X activity on the jedit-devel mailing list, the MacOSX plugin (e.g. current version 1.3) now works with Java 7. It already takes care to enable com.apple.eawt.FullScreenUtilities.setWindowCanFullScreen for the main jEdit view windows. So the top-right window corner has this device to switch into full-screen mode in a Apple-conformant manner. I see this as another indication that I should dismantle http://isabelle.in.tum.de/repos/isabelle/file/87941795956c/src/Tools/jEdit/src/osx_adapter.scala and bundle the regular MacOSX.jar from jEdit instead. People hooked on the Isabelle repository can enable the plugin via the jEdit Plugin Manager (its full name is Mac OS X Support). Moving in that direction would mean to trust more the regular jEdit development process than trying to make local fixes and patches. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
On Wed, 25 Sep 2013, Lawrence Paulson wrote: I seem to be having problems with this version (f54a8f591e0f). I tried the usual tricks but I still get compilation errors. ~/isabelle/hfinite/Incompleteness: isabelle jedit -f SyntaxN.thy ### Building Isabelle/Scala ... GUI/gui.scala:47: error: not found: value split_lines if (height 0 split_lines(txt).length height) text.rows = height ^ Tools/main.scala:140: error: not found: value quote error(Bad Isabelle home directory: + quote(isabelle_home)) ^ 83 errors found Failed to compile sources ~/isabelle/hfinite/Incompleteness: hg id f54a8f591e0f tip I don't see a public Isabelle version of that id -- isn't that your project repository? Maybe your Isabelle clone got messed up locally, as a bad merge produced hy hg fetch or hg up. You can also try to purge Isabelle/lib/classes carefully by hand. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] sledgehammer panel problem
Sorry 7cec5a4d5532 Deleting Isabelle/lib/classes did the trick. Larry On 25 Sep 2013, at 14:58, Makarius makar...@sketis.net wrote: I don't see a public Isabelle version of that id -- isn't that your project repository? Maybe your Isabelle clone got messed up locally, as a bad merge produced hy hg fetch or hg up. You can also try to purge Isabelle/lib/classes carefully by hand. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Preferences on Mac OS X
On Wed, 25 Sep 2013, Makarius wrote: I see this as another indication that I should dismantle http://isabelle.in.tum.de/repos/isabelle/file/87941795956c/src/Tools/jEdit/src/osx_adapter.scala and bundle the regular MacOSX.jar from jEdit instead. People hooked on the Isabelle repository can enable the plugin via the jEdit Plugin Manager (its full name is Mac OS X Support). Isabelle/c83727c7a510 now bundles the MacOSX plugin -- it is off by default to avoid multiplatform confusion. People connected to the Isabelle repository need to tick the plugin in the Plugin Manager -- without download. I think that an update from the official jEdit plugin repository will override the bundled one. This did work already some weeks ago with Highlighter. Moreover Mac users should enable the native system look-and-feel in Utilities / Options / Global Options / Appearance, if this is not the case already. This configuration supports many Apple things, like full-screen mode, drag-and-drop of text files on the running application window, preferences menu, about menu, quit menu and quit action in the dock. The Isabelle.app for end-users will have both the Mac OS X look-and-feel and the plugin enabled by default. It also provides a proper application icon. File types via .thy extensions are still missing, though, since the underlying appbundler 1.0 by Oracle does not support this yet. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Isabelle_25-Sep-2013 integration test
Here is another integration test (based on Isabelle/c83727c7a510): http://www4.in.tum.de/~wenzelm/test/Isabelle_25-Sep-2013 Many of the contributing components have changed since last time, so it is worth checking again if everything fits together on all platforms, and nothing important is missing. Next week or so we start with official release candidates on isabelle-users. Right now it is just everyday business on isabelle-dev. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Dockable window Find
On Mon, Sep 23, 2013 at 12:25 PM, Makarius makar...@sketis.net wrote: The layers 2+3 offer extensive means of customization. To come back to the above example, one does, of course, not set StyleRanges on the SWT widget oneself. One registers with the JFace TextViewer's syntax highlighting mechanism and produces them on demand -- for instance from the semantic markup offered by Isabelle/Scala. Again: Why not make this practical, and tell Andrius Velykis about it? He has already Isabelle/Eclipse that is more than just a proof of concept or a small demo, so it deserves to catch up with the quality standards of Isabelle/jEdit. I am aware of the syntax highlighting capabilities in Eclipse. In Isabelle/Eclipse I am interfacing the APIs and frameworks provided by Eclipse in the majority of cases. In other cases, such as tokenisation, the Isabelle/Scala libraries are used just like in Isabelle/jEdit (rather than writing custom rules for Eclipse tokenisers). This is currently implemented so that a wrapper is provided on top of the Isabelle/Scala tokeniser that adheres to Eclipse's interfaces. I have to admit that the quality standards are a bit behind in comparison to Isabelle/jEdit. However, this is mostly the lack of time spent on adding specific features rather than having implementation troubles. I am aware of the `rise` field in StyleRange to render sub-/superscript, it's just that I haven't gone around to doing the whole control-symbols support yet. There is an open issue that tracks this though ( https://github.com/andriusvelykis/isabelle-eclipse/issues/8)! I do hope to achieve parity with Isabelle/jEdit once I am finished with writing up my PhD thesis, which is hopefully soon enough :) Isabelle/Eclipse is not there because Eclipse is better or something. I am not aiming at platform wars - Isabelle/Eclipse has been born out of the fact that I like Eclipse and I wanted to build tools on top of Eclipse and Isabelle. I do hope that people who also like Eclipse can contribute or build upon Isabelle/Eclipse so that the project would grow. Furthermore, I think that having different UIs on top of Isabelle/Scala can help with better APIs and more general implementation there. I would also agree with Holger: writing UIs should be encouraged for formal tools. The popularity of Eclipse as platform for different IDEs does help with implementing Isabelle/Eclipse. There are a number of editors to use as a reference for own implementations. Even if Scala is your language of choice, there is the Scala IDE code to look for implementation hints ( https://github.com/scala-ide/scala-ide).Furthermore, Eclipse tools such as Plug-in Spy helps with finding classes that implement features of the IDE. For example, I can click on a button within my Eclipse and see what is the class that provides implementation for this button. In the end, I am still playing catch-up with Isabelle/jEdit as well as all the goodies in Eclipse (the JDT editor has some nifty features to copy from). So props to Makarius for developing a nice PIDE and I hope Isabelle/Eclipse will be as nice in the near future :) Best regards, Andrius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: Dockable window Find
On Wed, 25 Sep 2013, Andrius Velykis wrote: Isabelle/Eclipse is not there because Eclipse is better or something. I am not aiming at platform wars - Isabelle/Eclipse has been born out of the fact that I like Eclipse and I wanted to build tools on top of Eclipse and Isabelle. I do hope that people who also like Eclipse can contribute or build upon Isabelle/Eclipse so that the project would grow. Furthermore, I think that having different UIs on top of Isabelle/Scala can help with better APIs and more general implementation there. These are very good reasons for Isabelle/Eclipse. The PIDE document model of Isabelle/Scala was done in a way to support exactly that. After some years working on the Isabelle/Scala basis and the Isabelle/jEdit front-end I had almost gotten the impression that nobody manages to pick up the challenge. Maybe you have noticed the subtle changes in the wording of the blurb for Isabelle/jEdit: Isabelle2011-1 and Isabelle2012: Isabelle/jEdit is an example application within the PIDE framework --- it illustrates many of the ideas in a realistic manner, ready to be used right now in Isabelle applications. Isabelle2013: Isabelle/jEdit is the flagship application of the PIDE framework --- it is ready for small and large Isabelle applications, for beginners and experts alike. Isabelle2013-1: Isabelle/jEdit is the main example application of the PIDE framework and the default user-interface for Isabelle. It is targeted at beginners and experts alike. So the slightly odd marketing talk about flagship has gone (I had copied that actually from PG Eclipse). Thanks to Isabelle/Eclipse the Isabelle/Scala/PIDE universe is populated by 1 non-trivial applications. In the end, I am still playing catch-up with Isabelle/jEdit as well as all the goodies in Eclipse (the JDT editor has some nifty features to copy from). So props to Makarius for developing a nice PIDE and I hope Isabelle/Eclipse will be as nice in the near future :) I had a very productive summer this year, so there are many new things in the main example application of PIDE. I am looking forward to see Isabelle/Eclipse catching up eventually (after you have finished your thesis). It will help to make some general progress in the field, such that projects like https://itu.dk/research/tomeso/kopitiam/ won't have to go back again to the TTY loop, as is done there for Coq (even though the TTY speaks XML in Coq 8.4). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_25-Sep-2013 integration test
First impression: amazing!! Huge thanks a lot for everyone involved in this new release. Isabelle/jEdit seems like a brave new world! All the Best! On Wed, Sep 25, 2013 at 12:37 PM, Makarius makar...@sketis.net wrote: Here is another integration test (based on Isabelle/c83727c7a510): http://www4.in.tum.de/~**wenzelm/test/Isabelle_25-Sep-**2013http://www4.in.tum.de/~wenzelm/test/Isabelle_25-Sep-2013 Many of the contributing components have changed since last time, so it is worth checking again if everything fits together on all platforms, and nothing important is missing. Next week or so we start with official release candidates on isabelle-users. Right now it is just everyday business on isabelle-dev. Makarius __**_ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.**informatik.tu-muenchen.de/** mailman/listinfo/isabelle-devhttps://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- Alfio Ricardo Martini PhD in Computer Science (TU Berlin) www.inf.pucrs.br/alfio Lattes: http://lattes.cnpq.br/4016080665372277 Associate Professor at Faculty of Informatics (PUCRS) Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática 90619-900 -Porto Alegre - RS - Brasil ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
