--- 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. \<Longrightarrow>)."
+ 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"
--- /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"
--- 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 $!;
}
--- /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 = <FILE>; $/ = "\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"; }
+}
--- 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 (\<lambda>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
--- 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 }
--- 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 @@
"\\<Upsilon>",
"\\<Phi>",
"\\<Psi>",
- "\\<Omega>",
- "\\<^isub>",
- "\\<^isup>"
+ "\\<Omega>"
];
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;
--- 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 @@
"\\<tau>", "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
"\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>", "\\<Lambda>",
"\\<Xi>", "\\<Pi>", "\\<Sigma>", "\\<Upsilon>", "\\<Phi>",
- "\\<Psi>", "\\<Omega>",
-
- "\\<^isub>", "\\<^isup>")
+ "\\<Psi>", "\\<Omega>")
val blanks = recode_set(" ", "\t", "\n", "\u000B", "\f", "\r", "\r\n", "\\<^newline>")
--- 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
--- 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';
--- 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)
--- 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);