--- a/lib/Tools/update_sub_sup Thu Aug 08 18:20:15 2013 +0200
+++ b/lib/Tools/update_sub_sup Thu Aug 08 20:43:54 2013 +0200
@@ -2,7 +2,7 @@
#
# Author: Makarius
#
-# DESCRIPTION: update sub/sup control symbols
+# DESCRIPTION: update Isabelle symbols involving sub/superscripts
## diagnostics
@@ -14,7 +14,7 @@
echo
echo "Usage: isabelle $PRG [FILES|DIRS...]"
echo
- echo " Recursively find .thy/.ML files and update control symbols for"
+ echo " Recursively find .thy/.ML files and update Isabelle symbols involving"
echo " sub- and superscript."
echo
echo " Old versions of files are preserved by appending \"~~\"."
--- a/lib/scripts/update_sub_sup Thu Aug 08 18:20:15 2013 +0200
+++ b/lib/scripts/update_sub_sup Thu Aug 08 20:43:54 2013 +0200
@@ -2,7 +2,7 @@
#
# Author: Makarius
#
-# update_sub_sup - update sub/sup control symbols
+# update_sub_sup - update Isabelle symbols involving sub/superscripts
use warnings;
use strict;
@@ -18,6 +18,9 @@
s/\Q\<^isub>\E/\\<^sub>/g;
s/\Q\<^isup>\E/\\<^sup>/g;
+ s/\Q\<onesuperior>\E/\\<^sup>1/g;
+ s/\Q\<twosuperior>\E/\\<^sup>2/g;
+ s/\Q\<threesuperior>\E/\\<^sup>3/g;
my $result = $_;
--- a/src/Doc/Tutorial/Documents/Documents.thy Thu Aug 08 18:20:15 2013 +0200
+++ b/src/Doc/Tutorial/Documents/Documents.thy Thu Aug 08 20:43:54 2013 +0200
@@ -121,17 +121,16 @@
@{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}
(\verb+\+\verb+<beta>+), etc. (excluding @{text "\<lambda>"}),
special letters like @{text "\<A>"} (\verb+\+\verb+<A>+) and @{text
- "\<AA>"} (\verb+\+\verb+<AA>+), and the control symbols
- \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter
- sub and super scripts. This means that the input
+ "\<AA>"} (\verb+\+\verb+<AA>+). Moreover the control symbol
+ \verb+\+\verb+<^sub>+ may be used to subscript a single letter or digit
+ in the trailing part of an identifier. This means that the input
\medskip
- {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,}
+ {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isub>\<A>,}
\medskip
- \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"}
- by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single
- syntactic entity, not an exponentiation.
+ \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isub>\<A>"}
+ by Isabelle.
Replacing our previous definition of @{text xor} by the
following specifies an Isabelle symbol for the new operator:
--- a/src/Pure/General/scan.scala Thu Aug 08 18:20:15 2013 +0200
+++ b/src/Pure/General/scan.scala Thu Aug 08 20:43:54 2013 +0200
@@ -349,15 +349,13 @@
: Parser[Token] =
{
val letdigs1 = many1(Symbol.is_letdig)
- val sub_sup =
+ val sub =
one(s =>
s == Symbol.sub_decoded || s == "\\<^sub>" ||
- s == Symbol.isub_decoded || s == "\\<^isub>" ||
- s == Symbol.sup_decoded || s == "\\<^sup>" ||
- s == Symbol.isup_decoded || s == "\\<^isup>")
+ s == Symbol.isub_decoded || s == "\\<^isub>")
val id =
one(Symbol.is_letter) ~
- (rep(letdigs1 | (sub_sup ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
+ (rep(letdigs1 | (sub ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^
{ case x ~ y => x + y }
val nat = many1(Symbol.is_digit)
--- a/src/Pure/General/symbol.ML Thu Aug 08 18:20:15 2013 +0200
+++ b/src/Pure/General/symbol.ML Thu Aug 08 20:43:54 2013 +0200
@@ -517,8 +517,6 @@
fun symbolic_end (_ :: "\\<^sub>" :: _) = true
| symbolic_end (_ :: "\\<^isub>" :: _) = true
- | symbolic_end (_ :: "\\<^sup>" :: _) = true
- | symbolic_end (_ :: "\\<^isup>" :: _) = true
| symbolic_end (s :: _) = is_symbolic s
| symbolic_end [] = false;
--- a/src/Pure/General/symbol_pos.ML Thu Aug 08 18:20:15 2013 +0200
+++ b/src/Pure/General/symbol_pos.ML Thu Aug 08 20:43:54 2013 +0200
@@ -217,14 +217,11 @@
val letter = Scan.one (symbol #> Symbol.is_letter);
val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
-val sub_sup =
- Scan.one (symbol #>
- (fn s => s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^sup>" orelse s = "\\<^isup>"));
+val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>" orelse s = "\\<^isub>"));
in
-val scan_ident =
- letter ::: (Scan.repeat (letdigs1 || sub_sup ::: letdigs1) >> flat);
+val scan_ident = letter ::: (Scan.repeat (letdigs1 || sub ::: letdigs1) >> flat);
end;
--- a/src/Pure/PIDE/document.scala Thu Aug 08 18:20:15 2013 +0200
+++ b/src/Pure/PIDE/document.scala Thu Aug 08 20:43:54 2013 +0200
@@ -196,7 +196,7 @@
def commands: Linear_Set[Command] = _commands.commands
def update_commands(new_commands: Linear_Set[Command]): Node =
- if (new_commands eq _commands) this
+ if (new_commands eq _commands.commands) this
else new Node(header, perspective, Node.Commands(new_commands))
def command_range(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] =
--- a/src/Pure/Syntax/lexicon.ML Thu Aug 08 18:20:15 2013 +0200
+++ b/src/Pure/Syntax/lexicon.ML Thu Aug 08 20:43:54 2013 +0200
@@ -296,8 +296,6 @@
fun chop_idx [] ds = idxname [] ds
| chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
| chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
- | chop_idx (cs as (_ :: "\\<^sup>" :: _)) ds = idxname cs ds
- | chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
| chop_idx (c :: cs) ds =
if Symbol.is_digit c then chop_idx cs (c :: ds)
else idxname (c :: cs) ds;
--- a/src/Pure/term.ML Thu Aug 08 18:20:15 2013 +0200
+++ b/src/Pure/term.ML Thu Aug 08 20:43:54 2013 +0200
@@ -980,8 +980,6 @@
(case rev (Symbol.explode x) of
_ :: "\\<^sub>" :: _ => false
| _ :: "\\<^isub>" :: _ => false
- | _ :: "\\<^sup>" :: _ => false
- | _ :: "\\<^isup>" :: _ => false
| c :: _ => Symbol.is_digit c
| _ => true);
in