--- a/NEWS Thu Sep 28 19:40:20 2023 +0200
+++ b/NEWS Thu Sep 28 20:07:30 2023 +0200
@@ -14,6 +14,13 @@
before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY.
+*** ML ***
+
+* Isabelle/ML explicitly rejects 'handle' with catch-all patterns.
+INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or
+as last resort declare [[ML_catch_all]] within the theory context.
+
+
New in Isabelle2023 (September 2023)
------------------------------------
--- a/src/HOL/Library/code_test.ML Thu Sep 28 19:40:20 2023 +0200
+++ b/src/HOL/Library/code_test.ML Thu Sep 28 20:07:30 2023 +0200
@@ -311,8 +311,8 @@
val _ = File.write driver_path driver
val _ =
ML_Context.eval
- {environment = ML_Env.SML, redirect = false, verbose = false, debug = NONE,
- writeln = writeln, warning = warning}
+ {environment = ML_Env.SML, redirect = false, verbose = false, catch_all = true,
+ debug = NONE, writeln = writeln, warning = warning}
Position.none
(ML_Lex.read_text (code, Position.file (File.symbolic_path code_path)) @
ML_Lex.read_text (driver, Position.file (File.symbolic_path driver_path)) @
--- a/src/HOL/Metis.thy Thu Sep 28 19:40:20 2023 +0200
+++ b/src/HOL/Metis.thy Thu Sep 28 20:07:30 2023 +0200
@@ -10,7 +10,10 @@
imports ATP
begin
-ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+context notes [[ML_catch_all]]
+begin
+ ML_file \<open>~~/src/Tools/Metis/metis.ML\<close>
+end
subsection \<open>Literal selection and lambda-lifting helpers\<close>
--- a/src/Pure/Isar/attrib.ML Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Sep 28 20:07:30 2023 +0200
@@ -613,6 +613,7 @@
register_config_string ML_Env.ML_environment #>
register_config_bool ML_Env.ML_read_global #>
register_config_bool ML_Env.ML_write_global #>
+ register_config_bool ML_Compiler.ML_catch_all #>
register_config_bool ML_Options.source_trace #>
register_config_bool ML_Options.exception_trace #>
register_config_bool ML_Options.exception_debugger #>
--- a/src/Pure/ML/ml_compiler.ML Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/ML/ml_compiler.ML Thu Sep 28 20:07:30 2023 +0200
@@ -7,11 +7,12 @@
signature ML_COMPILER =
sig
type flags =
- {environment: string, redirect: bool, verbose: bool,
+ {environment: string, redirect: bool, verbose: bool, catch_all: bool,
debug: bool option, writeln: string -> unit, warning: string -> unit}
val debug_flags: bool option -> flags
val flags: flags
val verbose: bool -> flags -> flags
+ val ML_catch_all: bool Config.T
val eval: flags -> Position.T -> ML_Lex.token list -> unit
end;
@@ -21,18 +22,18 @@
(* flags *)
type flags =
- {environment: string, redirect: bool, verbose: bool,
+ {environment: string, redirect: bool, verbose: bool, catch_all: bool,
debug: bool option, writeln: string -> unit, warning: string -> unit};
fun debug_flags opt_debug : flags =
- {environment = "", redirect = false, verbose = false,
+ {environment = "", redirect = false, verbose = false, catch_all = false,
debug = opt_debug, writeln = writeln, warning = warning};
val flags = debug_flags NONE;
-fun verbose b (flags: flags) =
- {environment = #environment flags, redirect = #redirect flags, verbose = b,
- debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
+fun verbose b ({environment, redirect, verbose = _, catch_all, debug, writeln, warning}: flags) =
+ {environment = environment, redirect = redirect, verbose = b, catch_all = catch_all,
+ debug = debug, writeln = writeln, warning = warning};
(* parse trees *)
@@ -147,6 +148,8 @@
(* eval ML source tokens *)
+val ML_catch_all = Config.declare_bool ("ML_catch_all", \<^here>) (K false);
+
fun eval (flags: flags) pos toks =
let
val opt_context = Context.get_generic_context ();
@@ -212,10 +215,18 @@
fun message {message = msg, hard, location = loc, context = _} =
let
val pos = Exn_Properties.position_of_polyml_location loc;
- val txt =
- (if hard then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^
- Pretty.string_of (Pretty.from_polyml msg);
- in if hard then err txt else warn txt end;
+ val s = Pretty.string_of (Pretty.from_polyml msg);
+ val catch_all =
+ #catch_all flags orelse
+ (case opt_context of
+ NONE => false
+ | SOME context => Config.get_generic context ML_catch_all);
+ val is_err =
+ hard orelse
+ (not catch_all andalso
+ String.isPrefix "Handler catches all exceptions" (XML.content_of (YXML.parse_body s)));
+ val txt = (if is_err then "ML error" else "ML warning") ^ Position.here pos ^ ":\n" ^ s;
+ in if is_err then err txt else warn txt end;
(* results *)
--- a/src/Pure/ML/ml_context.ML Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/ML/ml_context.ML Thu Sep 28 20:07:30 2023 +0200
@@ -238,3 +238,4 @@
end;
val ML = ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags);
+val ML_command = ML_Context.eval_source ML_Compiler.flags;
--- a/src/Pure/ML/ml_file.ML Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/ML/ml_file.ML Thu Sep 28 20:07:30 2023 +0200
@@ -6,7 +6,7 @@
signature ML_FILE =
sig
- val command: string -> bool option -> (theory -> Token.file) ->
+ val command: string -> bool -> bool option -> (theory -> Token.file) ->
Toplevel.transition -> Toplevel.transition
val ML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
val SML: bool option -> (theory -> Token.file) -> Toplevel.transition -> Toplevel.transition
@@ -15,7 +15,7 @@
structure ML_File: ML_FILE =
struct
-fun command environment debug get_file = Toplevel.generic_theory (fn gthy =>
+fun command environment catch_all debug get_file = Toplevel.generic_theory (fn gthy =>
let
val file = get_file (Context.theory_of gthy);
val provide = Resources.provide_file file;
@@ -24,7 +24,7 @@
val _ = Document_Output.check_comments (Context.proof_of gthy) (Input.source_explode source);
val flags: ML_Compiler.flags =
- {environment = environment, redirect = true, verbose = true,
+ {environment = environment, redirect = true, verbose = true, catch_all = catch_all,
debug = debug, writeln = writeln, warning = warning};
in
gthy
@@ -34,7 +34,7 @@
|> Context.mapping provide (Local_Theory.background_theory provide)
end);
-val ML = command "";
-val SML = command ML_Env.SML;
+val ML = command "" false;
+val SML = command ML_Env.SML true;
end;
--- a/src/Pure/ML_Bootstrap.thy Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/ML_Bootstrap.thy Thu Sep 28 20:07:30 2023 +0200
@@ -35,6 +35,6 @@
setup \<open>Context.theory_map ML_Env.bootstrap_name_space\<close>
-declare [[ML_read_global = false]]
+declare [[ML_read_global = false, ML_catch_all = true]]
end
--- a/src/Pure/Pure.thy Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/Pure.thy Thu Sep 28 20:07:30 2023 +0200
@@ -246,7 +246,7 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {environment = ML_Env.SML_export, redirect = false, verbose = true,
+ {environment = ML_Env.SML_export, redirect = false, verbose = true, catch_all = true,
debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.theory
@@ -258,7 +258,7 @@
(Parse.ML_source >> (fn source =>
let
val flags: ML_Compiler.flags =
- {environment = ML_Env.SML_import, redirect = false, verbose = true,
+ {environment = ML_Env.SML_import, redirect = false, verbose = true, catch_all = true,
debug = NONE, writeln = writeln, warning = warning};
in
Toplevel.generic_theory
@@ -1558,4 +1558,6 @@
declare [[ML_write_global = false]]
+ML_command \<open>\<^assert> (not (can ML_command \<open>() handle _ => ()\<close>))\<close>
+
end
--- a/src/Pure/Tools/debugger.ML Thu Sep 28 19:40:20 2023 +0200
+++ b/src/Pure/Tools/debugger.ML Thu Sep 28 20:07:30 2023 +0200
@@ -137,7 +137,7 @@
fun evaluate {SML, verbose} =
ML_Context.eval
- {environment = environment SML, redirect = false, verbose = verbose,
+ {environment = environment SML, redirect = false, verbose = verbose, catch_all = SML,
debug = SOME false, writeln = writeln_message, warning = warning_message}
Position.none;