From 096f56044f4eec14b9cd7009e87a86938bcdffee Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 28 Aug 2009 16:53:32 +0000 Subject: Add more commentary and new control examples --- etc/isar/TokensAcid.thy | 170 ++++++++++++++++++++++++++++++++---------------- 1 file changed, 114 insertions(+), 56 deletions(-) (limited to 'etc/isar') diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index 4430cc88..523f8cb5 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -1,49 +1,115 @@ -(* Some acid tests for token modes *) +(* Some acid tests for token modes in Isabelle + David Aspinall, 2008-9. + $Id$ +*) theory TokensAcid imports Main begin -(* Here's a table of all tokens for symbols, - produced by unicode-tokens-list-tokens *) +(* Symbols. + + Here's a table of all tokens for symbols, 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. +*) (* -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \
\ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \
-\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \ \ \ \ \ -\ \ \ \ \ \

\ \ \ \ -\ \ \ \ \ \ + 1. \ \ \ \ \ \ \ \ \ \ + 2. \ \ \ \ \ \ \ \ \ \ + 3. \ \ \ \ \ \ \ \ \ \ + 4. \ \ \ \ \ \ \ \ \ \ + 5. \ \ \ \ \ \ \ \ \ \ + 6. \ \ \ \ \ \ \ \ \ \ + 7. \ \ \ \ \ \ \ \ \ \ + 8. \ \ \ \ \ \ \ \ \ \ + 9. \ \ \ \ \ \ \ \ \ \ + 10. \ \ \ \ \ \ \ \ \ \ + 11. \ \ \ \ \ \ \ \ \ \ + 12. \ \ \ \ \ \ \ \ \ \

+ 13. \ \ \ \ \ \ \ \ \ \ + 14. \ \ \ \ \ \ \ \ \ \ + 15. \ \ \ \ \ \ \ \ \ \ + 16. \ \ \ \ \ \ \ \ \ \ + 17. \ \ \ \ \ \ \ \ \ \ + 18. \ \ \ \ \ \ \
\ \ \ + 19. \ \ \ \ \ \ \ \ \ \ + 20. \ \ \ \ \ \ \ \ \ \ + 21. \ \ \ \ \ \ \ \ \ \ + 22. \ \ \ \ \ \ \ \ \ \ + 23. \ \ \ \ \ \ \ \ \ \ + 24. \ \ \ \ \ \ \ \ \ \ + 25. \ \ \ \ \ \ \ \ \ \ + 26. \ \ \ \ \ \ \ \ \ \ + 27. \ \ \ \ \ \ \ \ \ \ + 28. \ \ \ \ \ \ \ \ \ \ + 29. \ \ \ \ \ \ \ \ \ \ + 30. \ \ \ \ \ \ \ \ \ \ + 31. \ \ \ \ \ \ \ \ \ \ + 32. \ \ \ \ \ \ \ \ \

\ + 33. \ \ \ \ \ \ \ \ \ *) -(* Demonstrating variants on token names: different token names, - same appearance. Simulated overloading. - Let's take back \ from the meta-level. +(* Tokens controlling layout and fonts: regions. + + Token region convention in Isabelle is \<^bFOO>... \<^eFOO> + + The \<^bserif>font\<^eserif> and \<^bbold>bold\<^ebold>/\<^bitalic>italic\<^eitalic> controls are non-standard and + may not be supported by other interfaces. + + Convenience functions: + Select a region, use Tokens -> Format Region -> Bold, etc + + Editing can be a bit fiddly, use C-c C-t C-t to show or hide + the control tokens to help. +*) + +term "a\<^bsub>longsub\<^esub>" +term "b\<^bsup>longsuper\<^esup>" +term "\<^bbold>Bold text \\\\ \ \\<^ebold>" +term "\<^bitalic>Italic text \\\\ \\\<^eitalic>" +term "\<^bsans>Sans serif text \\\\\\\<^esans>" +term "\<^bscript>Script \\\\\\\<^escript>" +term "\<^bfrakt>Frakt \\\\ \\\<^efrakt>" +term "\<^bserif>Roman \\\\ \\\<^eserif>" + + +(* Tokens controlling layout and fonts: next character. + + These are tokens that affect the following character/identifier only. + + Similar to previous case. + + See Tokens -> Format Char -> ... +*) + +(* NB: below here cannot be processed: just in terms to check with + string font for terms. *) + +term "a\<^sub>b" (* NB: here and below cannot be processed *) +term "a\<^sup>b" +term "a\<^isub>b" +term "a\<^isup>b" +term "\<^loc>a" +term "\<^bold>b" +term "\<^italic>b" + + +(* + Variants on token names: different token names, + same appearance. Simulated overloading, \<^bitalic>much\<^eitalic> simpler to do + this in the UI than mess with type classes, etc, + in the logical framework! + + Demonstration: let's take back \ from the meta-level. + + NB: the token scheme mechanism here is a PG convenience, + in other frontends you may have to define \< AndX> to + appear in the same way as \< And> individually. + Similarly for LaTeX output. + + Use C-c C-t C-z to toggle the display of tokens. *) consts @@ -60,27 +126,19 @@ term "\ {\ x. True, \ y. False}" (* Note: of course, copy and paste will produce wrong result for above: default token without variant is produced! *) -(* Tokens for layout control: next char *) -(* NB: below here cannot be processed: just in terms to check with - string font for terms. *) -term "a\<^sub>b" -term "a\<^sup>b" -term "a\<^isub>b" -term "a\<^isup>b" -term "\<^loc>a" -term "\<^bold>b" -term "\<^italic>b" -(* Tokens for layout control: regions *) +(* More esoteric stuff *) + + +term "\<^bbig>large text \ \ \\<^ebig>" + +term "\<^bsmall>small\<^esmall>" + +term "\<^bunderline>underlined\<^eunderline>" + +term "\<^boverline>overlined\<^eoverline>" -term "a\<^bsub>long\<^esub>" -term "b\<^bsup>long\<^esup>" -term "\<^bbold>Bold text \\\\ \ \\<^ebold>" -term "\<^bitalic>Italic text \\\\ \\\<^eitalic>" -term "\<^bscript>Script \\\\\\\<^escript>" -term "\<^bfrakt>Frakt \\\\ \\\<^efrakt>" -term "\<^bserif>Roman \\\\ \\\<^eserif>" (* Bold and italic combinations for regions *) term "\<^bbold>Bold and \<^bitalic>italic\<^eitalic>\<^ebold>" -- cgit v1.2.3