use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
authorkleing
Wed Oct 15 07:03:43 2003 +0200 (2003-10-15)
changeset 142349590df3c5f2a
parent 14233 f6b6b2c55141
child 14235 281295a1bbaa
use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid
conflict with locale subscript syntax)
NEWS
lib/texinputs/isabelle.sty
src/Pure/General/symbol.ML
     1.1 --- a/NEWS	Wed Oct 15 01:58:41 2003 +0200
     1.2 +++ b/NEWS	Wed Oct 15 07:03:43 2003 +0200
     1.3 @@ -17,9 +17,10 @@
     1.4    symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
     1.5    existing theory and ML files.
     1.6  
     1.7 -* Pure: single letter subscripts (\<^sub>l) are now allowed in identifiers.
     1.8 -  Similar to greek letters \<^sub> is now considered a normal letter. 
     1.9 -	For multiple letter subscripts repeat \<^sub> like this: i\<^sub>1\<^sub>2. 
    1.10 +* Pure: single letter sub/superscripts (\<^isub> and \<^isup>) are now 
    1.11 +  allowed in identifiers. Similar to greek letters \<^isub> is now considered 
    1.12 +  a normal (but invisible) letter. For multiple letter subscripts repeat 
    1.13 +  \<^isub> like this: x\<^isub>1\<^isub>2. 
    1.14  
    1.15  * Pure: Using the functions Theory.add_finals or Theory.add_finals_i
    1.16    or the new Isar command "finalconsts", it is now possible to
     2.1 --- a/lib/texinputs/isabelle.sty	Wed Oct 15 01:58:41 2003 +0200
     2.2 +++ b/lib/texinputs/isabelle.sty	Wed Oct 15 07:03:43 2003 +0200
     2.3 @@ -24,6 +24,8 @@
     2.4  \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
     2.5  \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     2.6  \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
     2.7 +\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
     2.8 +\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
     2.9  \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
    2.10  
    2.11  \newdimen\isa@parindent\newdimen\isa@parskip
     3.1 --- a/src/Pure/General/symbol.ML	Wed Oct 15 01:58:41 2003 +0200
     3.2 +++ b/src/Pure/General/symbol.ML	Wed Oct 15 07:03:43 2003 +0200
     3.3 @@ -110,7 +110,7 @@
     3.4  
     3.5      val bbb_letters = ["bool","complex","nat","rat","real","int"]
     3.6  
     3.7 -    val control_letters = ["^sub"]
     3.8 +    val control_letters = ["^isub", "^isup"]
     3.9   
    3.10      val pre_letters =
    3.11  	cal_letters   @