Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-02-01

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

All times shown according to UTC.

Time Nick Message
02:48 ilbot3 joined #isabelle
02:48 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
10:27 int-e hmm I wish the "proof outline" message would disappear when there already is a proof outline in the text (squiggles are annoying, even when they're light blue)
10:33 larsrh int-e: interesting idea
10:33 larsrh not sure how easy that would be to fit into the document model
10:35 int-e Yeah, I'm not even sure how to specify the presence of a proof outline semi-formally.
10:37 juls joined #isabelle
10:45 larsrh int-e: well, you could make the message disappear once you click on it
10:55 silver joined #isabelle
11:03 int-e Maybe having a matching successful qed would be a good enough criterion.
11:03 JCaesar larsrh: It would reappear once you move your cursor away from it and back, no?
11:03 int-e (the information whether something has been clicked won't survive reloads and the like)
11:33 wagle joined #isabelle
11:38 JCaesar sledgehammer[timeout=31536000] … sledgehammer has become self-aware and does not want to prove your puny subgoals anymore.
14:24 silver_ joined #isabelle
14:25 ammbauer joined #isabelle
15:16 stoopkid joined #isabelle

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