# HG changeset patch # User wenzelm # Date 1244640409 -7200 # Node ID ef8163cfc540c34922f5aa787ac3082061e42ffd # Parent f7379ea2c9494575c3d48c831b0dfbf4a017446c# Parent 2db8db85c053bf2f1cb6fd7ea470d5d2049ce528 merged diff -r f7379ea2c949 -r ef8163cfc540 NEWS --- a/NEWS Wed Jun 10 10:42:24 2009 +0200 +++ b/NEWS Wed Jun 10 15:26:49 2009 +0200 @@ -4,28 +4,38 @@ New in this Isabelle version ---------------------------- +*** General *** + +* Discontinued old form of "escaped symbols" such as \\. 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 *** diff -r f7379ea2c949 -r ef8163cfc540 doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Wed Jun 10 10:42:24 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Wed Jun 10 15:26:49 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;\\ diff -r f7379ea2c949 -r ef8163cfc540 doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Wed Jun 10 10:42:24 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Program.tex Wed Jun 10 15:26:49 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% diff -r f7379ea2c949 -r ef8163cfc540 doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Wed Jun 10 10:42:24 2009 +0200 +++ b/doc-src/Codegen/Thy/examples/Example.hs Wed Jun 10 15:26:49 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; diff -r f7379ea2c949 -r ef8163cfc540 doc-src/antiquote_setup.ML --- a/doc-src/antiquote_setup.ML Wed Jun 10 10:42:24 2009 +0200 +++ b/doc-src/antiquote_setup.ML Wed Jun 10 15:26:49 2009 +0200 @@ -19,16 +19,16 @@ | "{" => "\\{" | "|" => "$\\mid$" | "}" => "\\}" - | "\\" => "-" + | "\" => "-" | c => c); -fun clean_name "\\" = "dots" +fun clean_name "\" = "dots" | clean_name ".." = "ddot" | clean_name "." = "dot" | clean_name "_" = "underscore" | clean_name "{" = "braceleft" | clean_name "}" = "braceright" - | clean_name s = s |> translate (fn "_" => "-" | "\\" => "-" | c => c); + | clean_name s = s |> translate (fn "_" => "-" | "\" => "-" | c => c); (* verbatim text *) diff -r f7379ea2c949 -r ef8163cfc540 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Wed Jun 10 10:42:24 2009 +0200 +++ b/src/Pure/General/symbol.ML Wed Jun 10 15:26:49 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]); diff -r f7379ea2c949 -r ef8163cfc540 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Jun 10 10:42:24 2009 +0200 +++ b/src/Pure/General/symbol.scala Wed Jun 10 15:26:49 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) diff -r f7379ea2c949 -r ef8163cfc540 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Wed Jun 10 10:42:24 2009 +0200 +++ b/src/Pure/ML/ml_lex.ML Wed Jun 10 15:26:49 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 diff -r f7379ea2c949 -r ef8163cfc540 src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Wed Jun 10 10:42:24 2009 +0200 +++ b/src/Pure/ML/ml_syntax.ML Wed Jun 10 15:26:49 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); diff -r f7379ea2c949 -r ef8163cfc540 src/Pure/Syntax/syn_trans.ML --- a/src/Pure/Syntax/syn_trans.ML Wed Jun 10 10:42:24 2009 +0200 +++ b/src/Pure/Syntax/syn_trans.ML Wed Jun 10 15:26:49 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; diff -r f7379ea2c949 -r ef8163cfc540 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Wed Jun 10 10:42:24 2009 +0200 +++ b/src/Pure/Thy/thy_info.ML Wed Jun 10 15:26:49 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