# HG changeset patch # User wenzelm # Date 1373637085 -7200 # Node ID 0d0c20a0a34f901032ec14691a0910828099f4c7 # Parent 1e930ee99b0cc9b6df3b1357cedfaca9deee1f5b# Parent 0b30bde83185800efaaec2b4c21054cde8fe09d4 merged diff -r 1e930ee99b0c -r 0d0c20a0a34f lib/Tools/unsymbolize --- a/lib/Tools/unsymbolize Fri Jul 12 14:18:07 2013 +0200 +++ b/lib/Tools/unsymbolize Fri Jul 12 15:51:25 2013 +0200 @@ -14,11 +14,13 @@ echo echo "Usage: isabelle $PRG [FILES|DIRS...]" echo - echo " Recursively find .thy/.ML files, removing unreadable symbol names." + echo " Recursively find .thy/.ML files and remove symbols that are unreadably" + echo " in plain text (e.g. \)." + echo echo " Note: this is an ad-hoc script; there is no systematic way to replace" echo " symbols independently of the inner syntax of a theory!" echo - echo " Renames old versions of FILES by appending \"~~\"." + echo " Old versions of files are preserved by appending \"~~\"." echo exit 1 } @@ -33,5 +35,5 @@ ## main -find $SPECS \( -name \*.ML -o -name \*.thy \) -print | \ - xargs "$ISABELLE_HOME/lib/scripts/unsymbolize" +find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \ + xargs -0 "$ISABELLE_HOME/lib/scripts/unsymbolize" diff -r 1e930ee99b0c -r 0d0c20a0a34f lib/Tools/update_sub_sup --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/Tools/update_sub_sup Fri Jul 12 15:51:25 2013 +0200 @@ -0,0 +1,36 @@ +#!/usr/bin/env bash +# +# Author: Makarius +# +# DESCRIPTION: update sub/sup control symbols + + +## diagnostics + +PRG="$(basename "$0")" + +function usage() +{ + echo + echo "Usage: isabelle $PRG [FILES|DIRS...]" + echo + echo " Recursively find .thy/.ML files and update control symbols for" + echo " sub- and superscript." + echo + echo " Old versions of files are preserved by appending \"~~\"." + echo + exit 1 +} + + +## process command line + +[ "$#" -eq 0 -o "$1" = "-?" ] && usage + +SPECS="$@"; shift "$#" + + +## main + +find $SPECS \( -name \*.ML -o -name \*.thy \) -print0 | \ + xargs -0 "$ISABELLE_HOME/lib/scripts/update_sub_sup" diff -r 1e930ee99b0c -r 0d0c20a0a34f lib/scripts/unsymbolize --- a/lib/scripts/unsymbolize Fri Jul 12 14:18:07 2013 +0200 +++ b/lib/scripts/unsymbolize Fri Jul 12 15:51:25 2013 +0200 @@ -2,8 +2,7 @@ # # Author: Markus Wenzel, TU Muenchen # -# unsymbolize.pl - remove unreadable symbol names from sources -# +# unsymbolize - remove unreadable symbol names from sources use warnings; use strict; @@ -46,7 +45,7 @@ my $result = $_; if ($text ne $result) { - print STDERR "fixing $file\n"; + print STDERR "changing $file\n"; if (! -f "$file~~") { rename $file, "$file~~" || die $!; } diff -r 1e930ee99b0c -r 0d0c20a0a34f lib/scripts/update_sub_sup --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/update_sub_sup Fri Jul 12 15:51:25 2013 +0200 @@ -0,0 +1,41 @@ +#!/usr/bin/env perl +# +# Author: Makarius +# +# update_sub_sup - update sub/sup control symbols + +use warnings; +use strict; + +sub update_sub_sup { + my ($file) = @_; + + open (FILE, $file) || die $!; + undef $/; my $text = ; $/ = "\n"; # slurp whole file + close FILE || die $!; + + $_ = $text; + + s/\Q\<^isub>\E/\\<^sub>/g; + s/\Q\<^isup>\E/\\<^sup>/g; + + my $result = $_; + + if ($text ne $result) { + print STDERR "changing $file\n"; + if (! -f "$file~~") { + rename $file, "$file~~" || die $!; + } + open (FILE, "> $file") || die $!; + print FILE $result; + close FILE || die $!; + } +} + + +## main + +foreach my $file (@ARGV) { + eval { &update_sub_sup($file); }; + if ($@) { print STDERR "*** update_sub_sup $file: ", $@, "\n"; } +} diff -r 1e930ee99b0c -r 0d0c20a0a34f src/HOL/MicroJava/BV/Typing_Framework_JVM.thy --- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Fri Jul 12 14:18:07 2013 +0200 +++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Fri Jul 12 15:51:25 2013 +0200 @@ -301,21 +301,19 @@ shows "wf_prog (\G C bd. Q G C bd) G" -proof - - from wf show ?thesis - apply (unfold wf_prog_def wf_cdecl_def) - apply clarsimp - apply (drule bspec, assumption) - apply (unfold wf_cdecl_mdecl_def) - apply clarsimp - apply (drule bspec, assumption) - apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+) - apply (frule is_type_pTs [OF wf], assumption+) - apply clarify - apply (drule rule [OF wf], assumption+) - apply (rule HOL.refl) - apply assumption+ - done -qed + using wf + apply (unfold wf_prog_def wf_cdecl_def) + apply clarsimp + apply (drule bspec, assumption) + apply (unfold wf_cdecl_mdecl_def) + apply clarsimp + apply (drule bspec, assumption) + apply (frule methd [OF wf [THEN wf_prog_ws_prog]], assumption+) + apply (frule is_type_pTs [OF wf], assumption+) + apply clarify + apply (drule rule [OF wf], assumption+) + apply (rule HOL.refl) + apply assumption+ + done end diff -r 1e930ee99b0c -r 0d0c20a0a34f src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri Jul 12 14:18:07 2013 +0200 +++ b/src/Pure/General/scan.scala Fri Jul 12 15:51:25 2013 +0200 @@ -348,7 +348,18 @@ private def other_token(is_command: String => Boolean) : Parser[Token] = { - val id = one(Symbol.is_letter) ~ many(Symbol.is_letdig) ^^ { case x ~ y => x + y } + val letdigs1 = many1(Symbol.is_letdig) + val sub_sup = + 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>") + val id = + one(Symbol.is_letter) ~ + (rep(letdigs1 | (sub_sup ~ letdigs1 ^^ { case x ~ y => x + y })) ^^ (_.mkString)) ^^ + { case x ~ y => x + y } + val nat = many1(Symbol.is_digit) val natdot = nat ~ "." ~ nat ^^ { case x ~ y ~ z => x + y + z } val id_nat = id ~ opt("." ~ nat) ^^ { case x ~ Some(y ~ z) => x + y + z case x ~ None => x } diff -r 1e930ee99b0c -r 0d0c20a0a34f src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Fri Jul 12 14:18:07 2013 +0200 +++ b/src/Pure/General/symbol.ML Fri Jul 12 15:51:25 2013 +0200 @@ -46,7 +46,6 @@ val decode: symbol -> sym datatype kind = Letter | Digit | Quasi | Blank | Other val kind: symbol -> kind - val is_letter_symbol: symbol -> bool val is_letter: symbol -> bool val is_digit: symbol -> bool val is_quasi: symbol -> bool @@ -377,9 +376,7 @@ "\\", "\\", "\\", - "\\", - "\\<^isub>", - "\\<^isup>" + "\\" ]; in @@ -520,6 +517,7 @@ 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 1e930ee99b0c -r 0d0c20a0a34f src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Jul 12 14:18:07 2013 +0200 +++ b/src/Pure/General/symbol.scala Fri Jul 12 15:51:25 2013 +0200 @@ -347,9 +347,7 @@ "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", "\\", - "\\", "\\", - - "\\<^isub>", "\\<^isup>") + "\\", "\\") val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<^newline>") diff -r 1e930ee99b0c -r 0d0c20a0a34f src/Pure/General/symbol_pos.ML --- a/src/Pure/General/symbol_pos.ML Fri Jul 12 14:18:07 2013 +0200 +++ b/src/Pure/General/symbol_pos.ML Fri Jul 12 15:51:25 2013 +0200 @@ -215,51 +215,19 @@ local -val latin = Symbol.is_ascii_letter; -val digit = Symbol.is_ascii_digit; -fun underscore s = s = "_"; -fun prime s = s = "'"; -fun subscript s = s = "\\<^sub>" orelse s = "\\<^isub>"; -fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>"; -fun special_letter s = Symbol.is_letter_symbol s andalso not (script s); - -val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single; -val scan_digit = Scan.one (digit o symbol) >> single; -val scan_prime = Scan.one (prime o symbol) >> single; -val scan_extended = - Scan.one ((latin orf digit orf prime orf underscore orf special_letter) o symbol) >> single; - -val scan_subscript = - Scan.one (subscript o symbol) -- - Scan.one ((latin orf digit orf prime orf special_letter) o symbol) - >> (fn (x, y) => [x, y]); - -val scan_ident_part1 = - Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_subscript) >> flat) || - Scan.one (special_letter o symbol) ::: - (Scan.repeat (scan_digit || scan_prime || scan_subscript) >> flat); - -val scan_ident_part2 = - Scan.repeat1 (scan_plain || scan_subscript) >> flat || - scan_ident_part1; +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>")); in -val scan_ident0 = - Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol); - -val scan_ident1 = - Scan.one ((latin orf special_letter) o symbol) ::: - (Scan.repeat (scan_extended || Scan.one (subscript o symbol) ::: scan_extended) >> flat); - -val scan_ident2 = - scan_ident_part1 @@@ - (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat); +val scan_ident = + letter ::: (Scan.repeat (letdigs1 || sub_sup ::: letdigs1) >> flat); end; -val scan_ident = scan_ident0; - fun is_identifier s = Symbol.is_ascii_identifier s orelse (case try (Scan.finite stopper scan_ident) (explode (s, Position.none)) of diff -r 1e930ee99b0c -r 0d0c20a0a34f src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Fri Jul 12 14:18:07 2013 +0200 +++ b/src/Pure/PIDE/command.ML Fri Jul 12 15:51:25 2013 +0200 @@ -135,7 +135,9 @@ (fn () => Outer_Syntax.side_comments span |> maps (fn cmt => (Thy_Output.check_text (Token.source_position_of cmt) st'; []) - handle exn => ML_Compiler.exn_messages_ids exn)) (); + handle exn => + if Exn.is_interrupt exn then reraise exn + else ML_Compiler.exn_messages_ids exn)) (); fun proof_status tr st = (case try Toplevel.proof_of st of @@ -201,8 +203,10 @@ val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list); fun print_error tr e = - (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () handle exn => - List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); + (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e () + handle exn => + if Exn.is_interrupt exn then reraise exn + else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); fun print_eq (Print {exec_id, ...}, Print {exec_id = exec_id', ...}) = exec_id = exec_id'; diff -r 1e930ee99b0c -r 0d0c20a0a34f src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Fri Jul 12 14:18:07 2013 +0200 +++ b/src/Pure/Syntax/lexicon.ML Fri Jul 12 15:51:25 2013 +0200 @@ -296,6 +296,7 @@ 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) diff -r 1e930ee99b0c -r 0d0c20a0a34f src/Pure/term.ML --- a/src/Pure/term.ML Fri Jul 12 14:18:07 2013 +0200 +++ b/src/Pure/term.ML Fri Jul 12 15:51:25 2013 +0200 @@ -980,6 +980,7 @@ (case rev (Symbol.explode x) of _ :: "\\<^sub>" :: _ => false | _ :: "\\<^isub>" :: _ => false + | _ :: "\\<^sup>" :: _ => false | _ :: "\\<^isup>" :: _ => false | c :: _ => Symbol.is_digit c | _ => true);