# HG changeset patch # User wenzelm # Date 1400596085 -7200 # Node ID 0662ccd94158370e3de1ff1b539b1f425ff1837f # Parent c44ce6f4067d98447d5e8c1a5b6c73929a88a2f4# Parent 801c01004a21c01483ccaee04e7ac44f146ff2f1 merged diff -r c44ce6f4067d -r 0662ccd94158 Admin/isatest/crontab.lxbroy2 --- a/Admin/isatest/crontab.lxbroy2 Tue May 20 16:00:00 2014 +0200 +++ b/Admin/isatest/crontab.lxbroy2 Tue May 20 16:28:05 2014 +0200 @@ -1,5 +1,5 @@ 03 00 * * * $HOME/bin/checkout-admin -17 00 * * * $HOME/bin/isatest-makedist +17 00 * * * /usr/bin/ssh lxbroy10 '$HOME/bin/isatest-makedist' 01 08 * * * $HOME/bin/isatest-check 04 23 31 1,3,5,7,8,10,12 * $HOME/bin/logmove diff -r c44ce6f4067d -r 0662ccd94158 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Tue May 20 16:00:00 2014 +0200 +++ b/src/Pure/Isar/token.scala Tue May 20 16:28:05 2014 +0200 @@ -185,7 +185,9 @@ (source.startsWith("\"") || source.startsWith("`") || source.startsWith("{*") || - source.startsWith("(*")) + source.startsWith("(*") || + source.startsWith(Symbol.open) || + source.startsWith(Symbol.open_decoded)) def is_begin: Boolean = is_keyword && source == "begin" def is_end: Boolean = is_keyword && source == "end"