3 files changed, 75 insertions, 6 deletions
diff --git a/etc/isar/TokensAcid.thy b/etc/isar/TokensAcid.thy
new file mode 100644
index 00000000..a6f80cf7
--- /dev/null
+++ b/etc/isar/TokensAcid.thy
@@ -0,0 +1,45 @@
+(* Some acid tests for token modes *)
+
+theory TokensAcid imports Main 
+begin
+
+(*  Here's a table of all tokens for symbols,  
+    produced by unicode-tokens-list-tokens *)
+
+(*
+\<alpha>	\<beta>	\<gamma>	\<delta>	\<epsilon>	\<zeta>	\<eta>	\<theta>	\<iota>	\<kappa>
+\<lambda>	\<mu>	\<nu>	\<xi>	\<pi>	\<rho>	\<sigma>	\<tau>	\<upsilon>	\<phi>
+\<chi>	\<psi>	\<omega>	\<Gamma>	\<Delta>	\<Theta>	\<Lambda>	\<Xi>	\<Pi>	\<Sigma>
+\<Upsilon>	\<Phi>	\<Psi>	\<Omega>	\<leftarrow>	\<rightarrow>	\<Leftarrow>	\<Rightarrow>	\<leftrightarrow>	\<Leftrightarrow>
+\<mapsto>	\<longleftarrow>	\<Longleftarrow>	\<longrightarrow>	\<Longrightarrow>	\<longleftrightarrow>	\<Longleftrightarrow>	\<longmapsto>	\<midarrow>	\<Midarrow>
+\<hookleftarrow>	\<hookrightarrow>	\<leftharpoondown>	\<rightharpoondown>	\<leftharpoonup>	\<rightharpoonup>	\<rightleftharpoons>	\<leadsto>	\<downharpoonleft>	\<downharpoonright>
+\<upharpoonleft>	\<upharpoonright>	\<restriction>	\<Colon>	\<up>	\<Up>	\<down>	\<Down>	\<updown>	\<Updown>
+\<langle>	\<rangle>	\<lceil>	\<rceil>	\<lfloor>	\<rfloor>	\<lparr>	\<rparr>	\<lbrakk>	\<rbrakk>
+\<lbrace>	\<rbrace>	\<guillemotleft>	\<guillemotright>	\<bottom>	\<top>	\<and>	\<And>	\<or>	\<Or>
+\<forall>	\<exists>	\<nexists>	\<not>	\<box>	\<diamond>	\<turnstile>	\<Turnstile>	\<tturnstile>	\<TTurnstile>
+\<stileturn>	\<surd>	\<le>	\<ge>	\<lless>	\<ggreater>	\<in>	\<notin>	\<subset>	\<supset>
+\<subseteq>	\<supseteq>	\<sqsubset>	\<sqsupset>	\<sqsubseteq>	\<sqsupseteq>	\<inter>	\<Inter>	\<union>	\<Union>
+\<squnion>	\<sqinter>	\<setminus>	\<propto>	\<uplus>	\<noteq>	\<sim>	\<doteq>	\<simeq>	\<approx>
+\<asymp>	\<cong>	\<smile>	\<equiv>	\<frown>	\<bowtie>	\<prec>	\<succ>	\<preceq>	\<succeq>
+\<parallel>	\<bar>	\<plusminus>	\<minusplus>	\<times>	\<div>	\<cdot>	\<star>	\<bullet>	\<circ>
+\<dagger>	\<ddagger>	\<lhd>	\<rhd>	\<unlhd>	\<unrhd>	\<triangleleft>	\<triangleright>	\<triangle>	\<triangleq>
+\<oplus>	\<otimes>	\<odot>	\<ominus>	\<oslash>	\<dots>	\<cdots>	\<Sum>	\<Prod>	\<Coprod>
+\<infinity>	\<integral>	\<ointegral>	\<clubsuit>	\<diamondsuit>	\<heartsuit>	\<spadesuit>	\<aleph>	\<emptyset>	\<nabla>
+\<partial>	\<Re>	\<Im>	\<flat>	\<natural>	\<sharp>	\<angle>	\<copyright>	\<registered>	\<hyphen>
+\<inverse>	\<onesuperior>	\<twosuperior>	\<threesuperior>	\<onequarter>	\<onehalf>	\<threequarters>	\<ordmasculine>	\<ordfeminine>	\<section>
+\<paragraph>	\<exclamdown>	\<questiondown>	\<euro>	\<pounds>	\<yen>	\<cent>	\<currency>	\<degree>	\<mho>
+\<lozenge>	\<wp>	\<wrong>	\<acute>	\<index>	\<dieresis>	\<cedilla>	\<hungarumlaut>	\<spacespace>	\<some>
+\<stareq>	\<defeq>	\<questioneq>	\<vartheta>	\<varpi>	\<varrho>	\<varsigma>	\<varphi>	\<hbar>	\<ell>
+\<ast>	\<bigcirc>	\<bigtriangleup>	\<bigtriangledown>	\<ni>	\<mid>	\<notlt>	\<notle>	\<notprec>	\<notpreceq>
+\<notsubset>	\<notsubseteq>	\<notsqsubseteq>	\<notgt>	\<notge>	\<notsucc>	\<notsucceq>	\<notsupset>	\<notsupseteq>	\<notsqsupseteq>
+\<notequiv>	\<notsim>	\<notsimeq>	\<notapprox>	\<notcong>	\<notasymp>	\<nearrow>	\<searrow>	\<swarrow>	\<nwarrow>
+\<vdots>	\<ddots>	\<closequote>	\<openquote>	\<opendblquote>	\<closedblquote>	\<emdash>	\<prime>	\<doubleprime>	\<tripleprime>
+\<nbspace>	\<thinspace>	\<notni>	\<colonequals>	\<foursuperior>	\<fivesuperior>	\<sixsuperior>	\<sevensuperior>	\<eightsuperior>	\<ninesuperior>
+\<zero>	\<one>	\<two>	\<three>	\<four>	\<five>	\<six>	\<seven>	\<eight>	\<nine>
+\<A>	\<B>	\<C>	\<D>	\<E>	\<F>	\<G>	\<H>	\<I>	\<J>
+\<K>	\<L>	\<M>	\<N>	\<O>	\<P>	\<Q>	\<R>	\<S>	\<T>
+\<U>	\<V>	\<W>	\<X>	\<Y>	\<Z>	
+*)
+
+
+end
diff --git a/etc/isar/XSymbolTests.thy b/etc/isar/XSymbolTests.thy
index 3689f300..0425fc39 100644
--- a/etc/isar/XSymbolTests.thy
+++ b/etc/isar/XSymbolTests.thy
@@ -1,4 +1,4 @@
-(* Some checks for X-Symbol behaviour.  
+(* Some checks for Unicode Tokens behaviour.  
 
    This file should be displayed sensibly, and also the
    display back from Isabelle ought to match.
@@ -26,14 +26,18 @@ by auto
    Problem reported by Norbert Schirmer <norbert.schirmer@web.de>
    Currently, superscript output highlighting seems broken anyway? *)
 
-consts silly:: "'a => 'a => 'a" ("_\<^sup>_" [1000,1000] 1000)
+consts "\<alpha1>":: "'a => 'a" ("\<alpha1>\<^sup>_")
+consts "\<alpha2>":: "'a => 'a => 'a" ("\<alpha2>\<^sup>_")
+consts "\<alpha3>":: "'a => 'a => 'a => 'a" ("_\<^sup>_\<^sup>_")
 
 consts k:: 'a
 
+term "\<alpha>"
 term "a\<^sup>b" (* b should be a blue variable *)
 term "\<forall>x. a\<^sup>x" (* x should be a green bound variable *)
 term "a\<^sup>k" (* k should be a black constant *)
 term "\<alpha>\<^isub>2" (* alpha should be blue variable with subscripted blue 2 *)
+term "\<alpha>\<^isup>x"  (* identifier *)
 
 consts sausage:: "'a => 'a => 'a" ("_\<^bsup>_\<^esup>" [1000,1000] 1000)
 
@@ -58,6 +62,8 @@ constdefs
  P2 :: bool   ("P\<^sup>2")    (* superscript *)
  "P\<^sup>2 == True"
 
+ "P\<^loc>x" (* location escape *)
+
 (* Buglet here: if we enable x-sym during scripting,
    goals/response flks are not updated, so xsyms
    do not appear in output windows. Stoping/starting
@@ -68,6 +74,12 @@ thm P1_def P2_def	(* check display from Isabelle *)
 
 constdefs (* long sub/sups, new 29/12/03, added by Gerwin Klein *)
 
+\<^bitalic>test italics\<^eitalic>
+\<^bserif>serif\<^eserif>
+\<^bfrakt>fraktur\<^efrakt>
+\<^bbold>test\<^ebold>
+
+\<^bsub> asda low\<^esub>
  Plow :: bool ("P\<^bsub>low\<^esub>")		(* spanning subscript *)
   "P\<^bsub>low\<^esub> \<equiv> True"
  Phigh :: bool ("P\<^bsup>high\<^esup>")		(* spanning superscript *)
@@ -80,9 +92,10 @@ by (simp add: P1_def P2_def)  (* .. and response window *)
 
 consts
  "P\<^sup>\<alpha>" :: bool   (* superscript of a token char *)
- "\<^bold>X"  :: bool   (* bold character 
-			    [not supported in current X-Symbols] *)
+ "\<^bold>P"  :: bool   (* bold character *)
+ "\<^italic>i"  :: int 
 
+\<^bitalic>italic?\<^eitalic>
 
 (* test: using a symbol as a subscript *)
 (* 9.3.03: this causes nasty prob with pre-command hook,
@@ -91,6 +104,10 @@ consts
 consts
  intof :: "nat \<Rightarrow> int"  ("_\<^sub>\<int>" 50)
  mynat :: nat ("\<gamma>")
+\<one> \<two> \<C> \<J>      \<S> \<h> h \<AA> 
+
+\<^bscript>foo\<^escript>
+bar
 
 term "intof 3"
 
@@ -118,3 +135,12 @@ primrec
 
 end
 
+\<A>
+\<AA> \<ABC> \<ss> \<pounds> \<yen>
+
+SYMBOL Ideas:
+
+ \<0x888>  for unicode character
+ \<alpha:foo> for variants, same display
+
+ \<color:foo> for colour, no sems (dropped in translation)
+\ No newline at end of file
diff --git a/etc/isar/multiple/C.thy b/etc/isar/multiple/C.thy
index 079a1f78..22d86858 100644
--- a/etc/isar/multiple/C.thy
+++ b/etc/isar/multiple/C.thy
@@ -1,5 +1,3 @@
-(* -*- isar -*- *)
-
 theory C imports A B
 begin