diff options
| author | David Aspinall | 2009-08-28 11:05:13 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-08-28 11:05:13 +0000 |
| commit | 73b59287a56b883d9c134d9110db0e01c5724f54 (patch) | |
| tree | 57c1105f582b9b6b179ad630d491dabb597f2b7a /isar/Example-Tokens.thy | |
| parent | 413782128b0c47d3b71b29d16f37fcfe33c91fd2 (diff) | |
Change font-lock-keywords to use our own hacked `unicode-tokens-prepend-text-property'
instead of `font-lock-prepend-text-property' which gave ill formed
property values for 'face. Still not clear if that function is faulty or
usage was not as intended. Anyway, this repairs outstanding merge properties
problem so that <bold><italic>foo</italic></bold> works as expected.
Also: fix key binding for unicode-tokens-show-controls so is usable.
Diffstat (limited to 'isar/Example-Tokens.thy')
0 files changed, 0 insertions, 0 deletions