diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-28 11:00:44 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-28 11:00:44 +0000 |
| commit | 09fc77336b72b5bcc123a5eba7d30253348af2e9 (patch) | |
| tree | 589605ff7715fab4fc306dec5149d1c782e06ee1 /etc/isar | |
| parent | eb0191e663e1c208d023b7ccfe2bfbdbb44f13b5 (diff) | |
Property merging now works with tweaks in unicode-tokens
Diffstat (limited to 'etc/isar')
| -rw-r--r-- | etc/isar/TokensAcid.thy | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy index 21a0699a..4430cc88 100644 --- a/etc/isar/TokensAcid.thy +++ b/etc/isar/TokensAcid.thy @@ -62,7 +62,8 @@ term "\<And2> {\<lambda> x. True, \<lambda> y. False}" (* Tokens for layout control: next char *) (* NB: below here cannot be processed: just in terms to check with - string font for terms *) + string font for terms. *) + term "a\<^sub>b" term "a\<^sup>b" term "a\<^isub>b" @@ -81,11 +82,11 @@ term "\<^bscript>Script \<alpha>\<beta>\<gamma>\<delta>\<in>\<forall>\<^escript> term "\<^bfrakt>Frakt \<alpha>\<beta>\<gamma>\<delta> \<in>\<forall>\<^efrakt>" term "\<^bserif>Roman \<alpha>\<beta>\<gamma>\<delta> \<in>\<forall>\<^eserif>" -(* Note: nesting regions not reliable; merging properties flaw? *) +(* Bold and italic combinations for regions *) term "\<^bbold>Bold and \<^bitalic>italic\<^eitalic>\<^ebold>" term "\<^bitalic>Italic and \<^bbold>bold\<^ebold>\<^eitalic>" -(* Font changes work, though *) +(* Font and weight/shape changes for regions *) term "\<^bbold>Bold and \<^bscript>script\<^escript>\<^ebold>" term "\<^bserif>Roman and \<^bitalic>italic\<^eitalic> and \<^bbold>bold\<^ebold> \<^eserif>" term "\<^bfrakt>Frakt and \<^bitalic>italic\<^eitalic> and \<^bbold>bold\<^ebold> \<^efrakt>" |