NEWS
changeset 56939 c2ddbf327bbd
parent 56927 4044a7d1720f
child 56942 5fff4dc31d34
equal deleted inserted replaced
56938:ef44b488bad8 56939:c2ddbf327bbd
   134 * More support for remote files (e.g. http) using standard Java
   134 * More support for remote files (e.g. http) using standard Java
   135 networking operations instead of jEdit virtual file-systems.
   135 networking operations instead of jEdit virtual file-systems.
   136 
   136 
   137 * Improved Console/Scala plugin: more uniform scala.Console output,
   137 * Improved Console/Scala plugin: more uniform scala.Console output,
   138 more robust treatment of threads and interrupts.
   138 more robust treatment of threads and interrupts.
       
   139 
       
   140 * Improved management of dockable windows: clarified keyboard focus
       
   141 and window placement wrt. main editor view; optional menu item to
       
   142 "Detach" a copy where this makes sense.
   139 
   143 
   140 
   144 
   141 *** Pure ***
   145 *** Pure ***
   142 
   146 
   143 * Basic constants of Pure use more conventional names and are always
   147 * Basic constants of Pure use more conventional names and are always