I'm still a regular user of PG. From time to time, I test Isabelle/jEdit, and my reasons for switching back to PG are somewhat similar to what Andreas reported. My main problems with Isabelle/JEdit are:
1. I cannot really control what Isabelle/Jedit processes when, and it invests computation power on the meaningless parts of the file directly after the point where I am editing. I'm not even convinced that it is the right approach to let Isabelle/jEdit's heuristics decide when and what it processes, and make user intervention impossible at first place (Or even worse, force the user into workarounds like inserting semicolons or "end"s behind the current editing point, which seems to be common practice among Isabelle/jEdit users) 2. In PG, when the processed region reaches the end of a theory file, I can be pretty sure that everything is fine with this theory. In Isabelle/jEdit, I have to scan the theory status panel manually for remaining red or pink bars, which is very inconvenient for large projects with hundreds of files. Moreover, I find it a bit scary that severe errors related to Isabelle/jEdit's document processing model (cf. https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-November/msg00170.html) can go undiscovered for several month, although most Isabelle users are on Isabelle/jEdit these days. I ask myself: Have they got so used to strange behaviours of the IDE that they do not realize severe errors any more? -- Peter On Mo, 2014-04-28 at 09:14 +0200, Andreas Lochbihler wrote: > Hi Makarius, > > Over the past weeks, I've been using Isabelle/jEdit about half of my Isabelle > time (and > ProofGeneral 3.7.1.1 with XEmacs the other half). Isabelle/jEdit is great > when it comes to > working on small projects or refactoring existing sources. I really like the > negative line > spacing setting and completion of fact names! Thanks! > > My main usage of PG is when I want to construct a complicated proof method > call like > > (fastforce intro: ... dest: ... elim: ... simp add: ... cong: ... del: ... > simp del: ...)+ > > that collapses an apply script of a hundred lines. I haven't yet found a > convenient way to > write the apply script in Isabelle/jEdit, because of reactivity issues (see > item 2 below) > and the continuous updates of the output window (when I scroll to some other > part of the > apply script using the cursor keys). Are there key bindings for scrolling > that do not move > the cursor? > > > Here are some things that could be improved in Isabelle/jEdit (I am currently > on > Isabelle/4e2a0d4e7a82): > > 1. Symbol completion in PG was absolutely deterministic. The immediate symbol > completion > in jEdit works great, too, I merely had to learn new sequences of key > strokes. Symbol > completion of non-unique results is not satisfactory. > > a) Given some text like > > definition foo where "foo = ..." > > when I add an attribute like [simp]: after the where, I get a symbol > completion popup to > replace the : with the element sign. Usually, my next thing is to move the > cursor with the > cursor keys. But the popup gobbles all the key strokes until I explicitly > close it with > ESC. As colons are used everywhere in Isabelle's outer syntax, it would > really be great if > the popup only appears when I am in inner syntax. > > b) Sometimes, when I write a HOL term, I used to not get the completion popup > when I enter > something like \un if there were sufficiently many parse errors in that > partial term. Even > Ctrl-b did not help. However, I cannot reproduce it in a small example at the > moment. > > > 2. Reactivity when processing large files > > With PG, I knew how to control the Isabelle prover. When I edit a large file > in a larger > project like JinjaThreads, every now and then, Isabelle changes the > background colour from > red to gray and then, apparently nothing happens for minutes before Isabelle > turns it red > again and starts reprocessing. Is there some way to explicitly tell Isabelle > that it > should now start to check again. Toggling "continuous checking" does not > help. Sometimes, > I even have to close the theory file and reopen it again. > > > 3. Navigation between theories files > > In PG, I usually have only a small subset of the loaded theories and ML files > open as > buffers, and I conveniently switch between them with Ctrl-x b. In jEdit, I > use Ctrl-` to > go to the previous file, but going to a different one is a pain, because I > have to search > it in the complete list of open files. > > It would be great if there was a list of just those files that I had on my > screen > previously, not all loaded files. > > Moreover, when I close a file and then press Ctrl-` in the file that shows > up, I do not > get to the file I have visited before the two, but to some arbitrary other. > Can jEdit > remember the order in which files have been visited? XEmacs at least does > this. > > > Maybe there are already solutions to the above annoyances, I just don't know > them. There's > another thing I would like to see in jEdit: The window layout has three > columns (one dock > on the left and one on the right) and the middle column (with the editor > area) can be > divided in three rows (dock - text - dock). Is there some way that I can > split the right > column into two rows to show two information areas at the same time (e.g. > Output at the > top and Find below)? > > > Andreas > > > On 27/04/14 20:14, Makarius wrote: > > Are there any remaining uses of Proof General, e.g. in the situation of > > current > > Isabelle/5b6f4655e2f2 ? > > > > This is neither a joke nor a running gag -- I just can't think of anything > > myself after > > the introduction of the spell checker. > > > > > > 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 mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
