From 6bf7903d3d22e64045783c709d27fdcc2cfea714 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 1 Dec 2009 23:13:27 +0000 Subject: Update token list adding fraktur characters. --- etc/isar/TokensAcid.thy | 43 ++++++++++++++++++++++++++----------------- 1 file changed, 26 insertions(+), 17 deletions(-) (limited to 'etc/isar') diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index f3773497..631ef336 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -16,14 +16,14 @@ begin produced by menu command Tokens -> List Tokens You should see glyphs in all positions except the whitespace - tokens at the end of row 25 and start of row 26. + tokens at positions 208, 262 and 263. I recommend using StixGeneral for symbols. See http://olegueret.googlepages.com/stixfonts-ttf This is the default for the symbol font if you have it installed. -*) + Other good choices are: Lucida Grande, Lucida Sans Unicode, + or DejaVuLGC Sans Mono. -(* 1. \ \ \ \ \ \ \ \ \ \ 2. \ \ \ \ \ \ \ \ \ \ 3. \ \ \ \ \ \ \ \ \ \ @@ -43,20 +43,29 @@ begin 17. \ \ \ \ \ \ \ \ \ \ 18. \ \ \ \ \ \ \
\ \ \ 19. \ \ \ \ \ \ \ \ \ \ - 20. \ \ \ \ \ \ \ \ \ \ - 21. \ \ \ \ \ \ \ \ \ \ - 22. \ \ \ \ \ \ \ \ \ \ - 23. \ \ \ \ \ \ \ \ \ \ - 24. \ \ \ \ \ \ \ \ \ \ - 25. \ \ \ \ \ \ \ \ \ \ - 26. \ \ \ \ \ \ \ \ \ \ - 27. \ \ \ \ \ \ \ \ \ \ - 28. \ \ \ \ \ \ \ \ \ \ - 29. \ \ \ \ \ \ \ \ \ \ - 30. \ \ \ \ \ \ \ \ \ \ - 31. \ \ \ \ \ \ \ \ \ \ - 32. \ \ \ \ \ \ \ \ \

\ \ \ + 34. \ \ \ \ \ \ \ \ \ \ + 35. \ \ \ \ \ \ \ \ \ \ + 36. \ \ \

\ \ \ \ \ \ \ + 37. \ \ \ \ \ \ \

\ \ \ + 38. \ \ \ \ \ \ \ \ \ \ + 39. \ \ \ \ \ \ \ \ \ \ + 40. \ \ \
\ \ \ \ \ \ \ + 41. \ \ \ \ \ \ \ \ \ \ + 42. \ \ \ \ \ *) (* Tokens controlling layout and fonts: regions. -- cgit v1.2.3

\ - 33. \ \ \ \ \ \ \ \ \ + 20. \ \ \ \ \ \ \ \ \ \ + 21. \ \ \ \ \ \ \ \ \ \ + 22. \ \ \ \ \ \ \ \ \ \ + 23. \ \ \ \ \ \ \ \ \ \ + 24. \ \ \ \ \ \ \ \ \ \ + 25. \ \ \ \ \ \ \ \ \ \ + 26. \ \ \ \ \ \ \ \ \ \ + 27. \ \ \ \ \ \ \ \ \ \ + 28. \ \ \ \ \ \ \ \ \ \ + 29. \ \ \ \ \ \ \ \ \ \ + 30. \ \ \ \ \ \ \ \ \ \ + 31. \ \ \ \ \ \ \ \ \ \ + 32. \ \ \ \ \ \ \ \ \ \ + 33. \ \ \ \ \ \ \