Perl 6 - the future is here, just unevenly distributed

IRC log for #isabelle, 2017-07-26

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

All times shown according to UTC.

Time Nick Message
00:34 deep-book-gk_ joined #isabelle
00:37 deep-book-gk_ left #isabelle
01:51 ilbot3 joined #isabelle
01:51 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/
05:15 dmiles joined #isabelle
08:00 chindy I dont know whether it's intended or not, but the bottom one works whereas the top one does not, probably due to some parsing: http://downthetypehole.de/paste/1N1fL1GL
08:03 larsrh neither works for me
08:03 larsrh the paste looks incomplete; e.g. there's the equality sign after "locale" missing
08:04 larsrh also I don't know what this "text_raw {}" syntax is supposed to mean
08:04 larsrh if I remove it both work
09:04 exprosic joined #isabelle
09:04 exprosic left #isabelle
09:08 chindy larsrh: yea i just typed it out of my mind from a more complex example thta i have ... I use text_raw for for snippets for latex
09:14 Merv_ joined #isabelle
09:21 larsrh chindy: text_raw is a command, so it'll interrupt a locale declaration
09:21 larsrh if you need some inline commenting, use --
09:24 chindy larsrh: tried it, does not work. FYI I use "text_raw {*\DefineSnippet{poeFWT}{*}"  to define snippets that i later include in the paper
09:29 larsrh ok, then you should probably do that before the locale declaration
11:55 dmiles joined #isabelle

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