| Tue, 25 Feb 2014 22:54:21 +0100 | wenzelm | merged | changeset | files |
| Tue, 25 Feb 2014 22:13:57 +0100 | wenzelm | uniform insert vs. popup policy; | changeset | files |
| Tue, 25 Feb 2014 21:58:46 +0100 | wenzelm | tuned proofs; | changeset | files |
| Tue, 25 Feb 2014 21:32:26 +0100 | wenzelm | back to Markup.command for actual tokens (amending 4a4e5686e091) -- avoid conflict of jEdit token marker with Rendering.text_colors; | changeset | files |
| Tue, 25 Feb 2014 20:57:57 +0100 | wenzelm | tuned signature; | changeset | files |
| Tue, 25 Feb 2014 20:46:09 +0100 | wenzelm | no word completion within word context; | changeset | files |