--- a/NEWS Wed Jun 10 21:04:36 2009 +0200
+++ b/NEWS Thu Jun 11 11:21:01 2009 +0200
@@ -4,28 +4,38 @@
New in this Isabelle version
----------------------------
+*** General ***
+
+* Discontinued old form of "escaped symbols" such as \\<forall>. Only
+one backslash should be used, even in ML sources.
+
+
*** Pure ***
-* On instantiation of classes, remaining undefined class parameters are
-formally declared. INCOMPATIBILITY.
+* On instantiation of classes, remaining undefined class parameters
+are formally declared. INCOMPATIBILITY.
*** HOL ***
-* Class semiring_div requires superclass no_zero_divisors and proof of div_mult_mult1;
-theorems div_mult_mult1, div_mult_mult2, div_mult_mult1_if, div_mult_mult1 and
-div_mult_mult2 have been generalized to class semiring_div, subsuming former
-theorems zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and zdiv_zmult_zmult2.
-div_mult_mult1 is now [simp] by default. INCOMPATIBILITY.
-
-* Power operations on relations and functions are now one dedicate constant compow with
-infix syntax "^^". Power operations on multiplicative monoids retains syntax "^"
-and is now defined generic in class power. INCOMPATIBILITY.
-
-* ML antiquotation @{code_datatype} inserts definition of a datatype generated
-by the code generator; see Predicate.thy for an example.
-
-* New method "linarith" invokes existing linear arithmetic decision procedure only.
+* Class semiring_div requires superclass no_zero_divisors and proof of
+div_mult_mult1; theorems div_mult_mult1, div_mult_mult2,
+div_mult_mult1_if, div_mult_mult1 and div_mult_mult2 have been
+generalized to class semiring_div, subsuming former theorems
+zdiv_zmult_zmult1, zdiv_zmult_zmult1_if, zdiv_zmult_zmult1 and
+zdiv_zmult_zmult2. div_mult_mult1 is now [simp] by default.
+INCOMPATIBILITY.
+
+* Power operations on relations and functions are now one dedicate
+constant compow with infix syntax "^^". Power operations on
+multiplicative monoids retains syntax "^" and is now defined generic
+in class power. INCOMPATIBILITY.
+
+* ML antiquotation @{code_datatype} inserts definition of a datatype
+generated by the code generator; see Predicate.thy for an example.
+
+* New method "linarith" invokes existing linear arithmetic decision
+procedure only.
*** ML ***
--- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Jun 10 21:04:36 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Introduction.tex Thu Jun 11 11:21:01 2009 +0200
@@ -249,9 +249,9 @@
\hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
\hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
-\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~(let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
-\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
+\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys) );\\
\hspace*{0pt}\\
\hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
\hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
--- a/doc-src/Codegen/Thy/document/Program.tex Wed Jun 10 21:04:36 2009 +0200
+++ b/doc-src/Codegen/Thy/document/Program.tex Thu Jun 11 11:21:01 2009 +0200
@@ -346,8 +346,8 @@
\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
\hspace*{0pt}fun mult (A{\char95}:'a semigroup) = {\char35}mult A{\char95};\\
\hspace*{0pt}\\
-\hspace*{0pt}type 'a monoid = {\char123}Program{\char95}{\char95}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
-\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}Program{\char95}{\char95}semigroup{\char95}monoid A{\char95};\\
+\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
+\hspace*{0pt}fun semigroup{\char95}monoid (A{\char95}:'a monoid) = {\char35}semigroup{\char95}monoid A{\char95};\\
\hspace*{0pt}fun neutral (A{\char95}:'a monoid) = {\char35}neutral A{\char95};\\
\hspace*{0pt}\\
\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
@@ -363,9 +363,8 @@
\hspace*{0pt}\\
\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
\hspace*{0pt}\\
-\hspace*{0pt}val monoid{\char95}nat =\\
-\hspace*{0pt} ~{\char123}Program{\char95}{\char95}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}~:\\
-\hspace*{0pt} ~nat monoid;\\
+\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
+\hspace*{0pt} ~:~nat monoid;\\
\hspace*{0pt}\\
\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
\hspace*{0pt}\\
@@ -967,9 +966,9 @@
\noindent%
\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
-\hspace*{0pt} ~let {\char123}\\
+\hspace*{0pt} ~(let {\char123}\\
\hspace*{0pt} ~~~(y :~ys) = rev xs;\\
-\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
+\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys) );\\
\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/Codegen/Thy/examples/Example.hs Wed Jun 10 21:04:36 2009 +0200
+++ b/doc-src/Codegen/Thy/examples/Example.hs Thu Jun 11 11:21:01 2009 +0200
@@ -23,9 +23,9 @@
dequeue (AQueue [] []) = (Nothing, AQueue [] []);
dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
dequeue (AQueue (v : va) []) =
- let {
+ (let {
(y : ys) = rev (v : va);
- } in (Just y, AQueue [] ys);
+ } in (Just y, AQueue [] ys) );
enqueue :: forall a. a -> Queue a -> Queue a;
enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
--- a/doc-src/antiquote_setup.ML Wed Jun 10 21:04:36 2009 +0200
+++ b/doc-src/antiquote_setup.ML Thu Jun 11 11:21:01 2009 +0200
@@ -19,16 +19,16 @@
| "{" => "\\{"
| "|" => "$\\mid$"
| "}" => "\\}"
- | "\\<dash>" => "-"
+ | "\<dash>" => "-"
| c => c);
-fun clean_name "\\<dots>" = "dots"
+fun clean_name "\<dots>" = "dots"
| clean_name ".." = "ddot"
| clean_name "." = "dot"
| clean_name "_" = "underscore"
| clean_name "{" = "braceleft"
| clean_name "}" = "braceright"
- | clean_name s = s |> translate (fn "_" => "-" | "\\<dash>" => "-" | c => c);
+ | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
(* verbatim text *)
--- a/src/Pure/General/symbol.ML Wed Jun 10 21:04:36 2009 +0200
+++ b/src/Pure/General/symbol.ML Thu Jun 11 11:21:01 2009 +0200
@@ -433,7 +433,7 @@
val scan_encoded_newline =
$$ "\^M" -- $$ "\n" >> K "\n" ||
$$ "\^M" >> K "\n" ||
- $$ "\\" -- Scan.optional ($$ "\\") "" -- Scan.this_string "<^newline>" >> K "\n";
+ Scan.this_string "\\<^newline>" >> K "\n";
val scan_raw =
Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) ||
@@ -442,7 +442,7 @@
val scan =
Scan.one is_plain ||
scan_encoded_newline ||
- (($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
+ ($$ "\\" ^^ $$ "<" ^^
!! (fn (cs, _) => malformed_msg (beginning 10 ("\\" :: "<" :: cs)))
(($$ "^" ^^ (scan_raw || scan_id) || scan_id) ^^ $$ ">")) ||
Scan.one not_eof;
@@ -453,7 +453,7 @@
Scan.this_string "{*" || Scan.this_string "*}";
val recover =
- (Scan.this (explode "\\\\<") || Scan.this (explode "\\<")) @@@
+ Scan.this ["\\", "<"] @@@
Scan.repeat (Scan.unless scan_resync (Scan.one not_eof))
>> (fn ss => malformed :: ss @ [end_malformed]);
--- a/src/Pure/General/symbol.scala Wed Jun 10 21:04:36 2009 +0200
+++ b/src/Pure/General/symbol.scala Thu Jun 11 11:21:01 2009 +0200
@@ -20,12 +20,12 @@
[^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
private val symbol = new Regex("""(?xs)
- \\ \\? < (?:
+ \\ < (?:
\^? [A-Za-z][A-Za-z0-9_']* |
\^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
- """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
+ """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
// total pattern
val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
@@ -133,8 +133,8 @@
}
val ch = new String(Character.toChars(code))
} yield (sym, ch)
- (new Recoder(mapping ++ (for ((x, y) <- mapping) yield ("\\" + x, y))),
- new Recoder(for ((x, y) <- mapping) yield (y, x)))
+ (new Recoder(mapping),
+ new Recoder(mapping map { case (x, y) => (y, x) }))
}
def decode(text: String) = decoder.recode(text)
--- a/src/Pure/ML/ml_lex.ML Wed Jun 10 21:04:36 2009 +0200
+++ b/src/Pure/ML/ml_lex.ML Thu Jun 11 11:21:01 2009 +0200
@@ -247,7 +247,11 @@
Symbol_Pos.source (Position.line 1) src
|> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
-val tokenize = Source.of_string #> source #> Source.exhaust;
+val tokenize =
+ Source.of_string #>
+ Symbol.source {do_recover = true} #>
+ source #>
+ Source.exhaust;
fun read_antiq (syms, pos) =
(Source.of_list syms
--- a/src/Pure/ML/ml_syntax.ML Wed Jun 10 21:04:36 2009 +0200
+++ b/src/Pure/ML/ml_syntax.ML Thu Jun 11 11:21:01 2009 +0200
@@ -58,7 +58,7 @@
| print_option f (SOME x) = "SOME (" ^ f x ^ ")";
fun print_char s =
- if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
+ if not (Symbol.is_char s) then s
else if s = "\"" then "\\\""
else if s = "\\" then "\\\\"
else
@@ -68,7 +68,7 @@
else "\\" ^ string_of_int c
end;
-val print_string = quote o translate_string print_char;
+val print_string = quote o implode o map print_char o Symbol.explode;
val print_strings = print_list print_string;
val print_properties = print_list (print_pair print_string print_string);
--- a/src/Pure/Syntax/syn_trans.ML Wed Jun 10 21:04:36 2009 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Thu Jun 11 11:21:01 2009 +0200
@@ -223,7 +223,7 @@
fun the_struct structs i =
if 1 <= i andalso i <= length structs then nth structs (i - 1)
- else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
+ else error ("Illegal reference to implicit structure #" ^ string_of_int i);
fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
Lexicon.free (the_struct structs 1)
@@ -503,7 +503,7 @@
val exn_results = map (Exn.capture ast_of) pts;
val exns = map_filter Exn.get_exn exn_results;
val results = map_filter Exn.get_result exn_results
- in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
+ in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
@@ -534,6 +534,6 @@
val exn_results = map (Exn.capture (term_of #> free_fixed)) asts;
val exns = map_filter Exn.get_exn exn_results;
val results = map_filter Exn.get_result exn_results
- in (case (results, exns) of ([], exn :: _) => raise exn | _ => results) end;
+ in (case (results, exns) of ([], exn :: _) => reraise exn | _ => results) end;
end;
--- a/src/Pure/Thy/thy_info.ML Wed Jun 10 21:04:36 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Jun 11 11:21:01 2009 +0200
@@ -387,7 +387,7 @@
(case Graph.get_node tasks name of
Task body =>
let val after_load = body ()
- in after_load () handle exn => (kill_thy name; raise exn) end
+ in after_load () handle exn => (kill_thy name; reraise exn) end
| _ => ()));
in