--- 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
--- 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"