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