Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2015-06-05

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary

All times shown according to UTC.

Time Nick Message
00:51 tautologico joined #isabelle
00:52 tautologico I can't get isabelle to work with proof general (emacs)
00:52 tautologico anyone using pg + isabelle on os x?
08:22 eduard__ joined #isabelle
08:43 int-e I believe that doesn't work anymore with Isabelle 2015 (and was unsupported in Isabelle 2014)
09:18 tautologico int-e: thanks
11:30 ThreeOfEight tautologico: Proof General has been abandoned for technical reasons. Isabelle/JEdit is the only supported editor these days.
11:31 kholerabbi emacs :sniff:
14:56 tautologico ThreeOfEight: can I ask what are the technical reasons?
17:02 int-e tautologico: As far as I understand, Isabelle's tty loop (which Proof General uses) and Isabelle's interactive document model (which Isabelle/Jedit uses) don't share any code, and supporting the former got in the way of improving the latter. Also Makarius grew tired of maintaining two backends. In principle it should be possible to have Proof General use the same interface as jedit, but it's...
17:02 int-e ...probably a lot of work and nobody has volunteered to do it.
17:03 tautologico int-e: that's what I imagined, thank you
20:45 tautologico joined #isabelle

| Channels | #isabelle index | Today | | Search | Google Search | Plain-Text | summary