Fri, 07 Mar 2014 11:48:11 +0100 | wenzelm | no completion of concealed names; | changeset | files |
Fri, 07 Mar 2014 11:46:26 +0100 | wenzelm | more official const syntax: avoid educated guessing by Syntax_Phases.decode_term; | changeset | files |
Fri, 07 Mar 2014 11:41:25 +0100 | wenzelm | tuned whitespace; | changeset | files |