merged
authorwenzelm
Tue May 20 16:28:05 2014 +0200 (2014-05-20)
changeset 570230662ccd94158
parent 57016 c44ce6f4067d
parent 57022 801c01004a21
child 57024 c9e98c2498fd
merged
     1.1 --- a/Admin/isatest/crontab.lxbroy2	Tue May 20 16:00:00 2014 +0200
     1.2 +++ b/Admin/isatest/crontab.lxbroy2	Tue May 20 16:28:05 2014 +0200
     1.3 @@ -1,5 +1,5 @@
     1.4  03 00 * * *                  $HOME/bin/checkout-admin
     1.5 -17 00 * * *                  $HOME/bin/isatest-makedist
     1.6 +17 00 * * *                  /usr/bin/ssh lxbroy10 '$HOME/bin/isatest-makedist'
     1.7  01 08 * * *                  $HOME/bin/isatest-check
     1.8  
     1.9  04 23 31 1,3,5,7,8,10,12 *   $HOME/bin/logmove
     2.1 --- a/src/Pure/Isar/token.scala	Tue May 20 16:00:00 2014 +0200
     2.2 +++ b/src/Pure/Isar/token.scala	Tue May 20 16:28:05 2014 +0200
     2.3 @@ -185,7 +185,9 @@
     2.4     (source.startsWith("\"") ||
     2.5      source.startsWith("`") ||
     2.6      source.startsWith("{*") ||
     2.7 -    source.startsWith("(*"))
     2.8 +    source.startsWith("(*") ||
     2.9 +    source.startsWith(Symbol.open) ||
    2.10 +    source.startsWith(Symbol.open_decoded))
    2.11  
    2.12    def is_begin: Boolean = is_keyword && source == "begin"
    2.13    def is_end: Boolean = is_keyword && source == "end"