From 09fc77336b72b5bcc123a5eba7d30253348af2e9 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 28 Aug 2009 11:00:44 +0000 Subject: Property merging now works with tweaks in unicode-tokens --- etc/isar/TokensAcid.thy | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'etc/isar') 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 "\ {\ x. True, \ 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 \\\\\\\<^escript> term "\<^bfrakt>Frakt \\\\ \\\<^efrakt>" term "\<^bserif>Roman \\\\ \\\<^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>" -- cgit v1.2.3