Thu, 25 May 2017 21:32:51 +0200 | wenzelm | more progress information, for the sake of sporadic dropouts; | changeset | files |
Thu, 25 May 2017 21:20:22 +0200 | wenzelm | restricted perspective depending on the caret -- important for reactivity when editing big files; | changeset | files |
Thu, 25 May 2017 19:50:37 +0200 | wenzelm | parallel retrieval of PIDE markup; | changeset | files |
Thu, 25 May 2017 19:23:01 +0200 | wenzelm | clarified output: do not require "method", which is absent for ResponseMessage; | changeset | files |