| Sat, 08 Mar 2014 21:31:12 +0100 | wenzelm | keep current context visibility for PIDE markup and completion (in contrast to 8e3e004f1c31): Attrib.check_src of 9dc5ce83202c should intern/report attributes once, which happens for local_theory in the (visible) auxiliary context; | changeset | files |
| Sat, 08 Mar 2014 21:08:10 +0100 | wenzelm | modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); | changeset | files |
| Sat, 08 Mar 2014 13:49:01 +0100 | wenzelm | allow suffix of underscores for words (notably keywords), similar to semantic completion; | changeset | files |