Mon, 06 Apr 2015 16:30:44 +0200 | wenzelm | clarified command keyword markup; | changeset | files |
Mon, 06 Apr 2015 16:00:19 +0200 | wenzelm | more position information and PIDE markup for command keywords; | changeset | files |
Mon, 06 Apr 2015 14:09:31 +0200 | wenzelm | allow prefix before keyword, notably 'private'; | changeset | files |
Mon, 06 Apr 2015 13:34:22 +0200 | wenzelm | support local command setup; | changeset | files |
Mon, 06 Apr 2015 13:28:54 +0200 | wenzelm | proper header; | changeset | files |
Mon, 06 Apr 2015 12:51:25 +0200 | wenzelm | tuned signature; | changeset | files |