# HG changeset patch # User wenzelm # Date 1375987434 -7200 # Node ID d1bcb4479a2f8fe4679453cf29b86428bd8efea4 # Parent 2b68f4109075b55a432be2c90e96e269cfc3a92d# Parent 0ea2b657eb420f4dda90cf38a77f6aec421942d1 merged diff -r 2b68f4109075 -r d1bcb4479a2f lib/Tools/update_sub_sup --- 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 \"~~\"." diff -r 2b68f4109075 -r d1bcb4479a2f lib/scripts/update_sub_sup --- 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\\E/\\<^sup>1/g; + s/\Q\\E/\\<^sup>2/g; + s/\Q\\E/\\<^sup>3/g; my $result = $_; diff -r 2b68f4109075 -r d1bcb4479a2f src/Doc/Tutorial/Documents/Documents.thy --- 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 "\"} (\verb+\+\verb++), @{text "\"} (\verb+\+\verb++), etc. (excluding @{text "\"}), special letters like @{text "\"} (\verb+\+\verb++) and @{text - "\"} (\verb+\+\verb++), and the control symbols - \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter - sub and super scripts. This means that the input + "\"} (\verb+\+\verb++). 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,\,\verb,\<^isub>1.,~\verb,\,\verb,\<^isub>1 = \,\verb,\<^isup>\,} + {\small\noindent \verb,\,\verb,\,\verb,\<^isub>1.,~\verb,\,\verb,\<^isub>1 = \,\verb,\<^isub>\,} \medskip - \noindent is recognized as the term @{term "\\\<^isub>1. \\<^isub>1 = \\<^isup>\"} - by Isabelle. Note that @{text "\\<^isup>\"} is a single - syntactic entity, not an exponentiation. + \noindent is recognized as the term @{term "\\\<^isub>1. \\<^isub>1 = \\<^isub>\"} + by Isabelle. Replacing our previous definition of @{text xor} by the following specifies an Isabelle symbol for the new operator: diff -r 2b68f4109075 -r d1bcb4479a2f src/Pure/General/scan.scala --- 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) diff -r 2b68f4109075 -r d1bcb4479a2f src/Pure/General/symbol.ML --- 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; diff -r 2b68f4109075 -r d1bcb4479a2f src/Pure/General/symbol_pos.ML --- 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; diff -r 2b68f4109075 -r d1bcb4479a2f src/Pure/PIDE/document.scala --- 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)] = diff -r 2b68f4109075 -r d1bcb4479a2f src/Pure/Syntax/lexicon.ML --- 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; diff -r 2b68f4109075 -r d1bcb4479a2f src/Pure/term.ML --- 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