--- a/src/Pure/Concurrent/isabelle_thread.ML Sun Sep 24 11:42:13 2023 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.ML Sun Sep 24 15:07:40 2023 +0200
@@ -24,6 +24,8 @@
val interrupt_exn: 'a Exn.result
val interrupt_self: unit -> 'a
val interrupt_other: T -> unit
+ val try: (unit -> 'a) -> 'a option
+ val can: (unit -> 'a) -> bool
end;
structure Isabelle_Thread: ISABELLE_THREAD =
@@ -115,4 +117,7 @@
fun interrupt_other t =
Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => ();
+fun try e = Basics.try e ();
+fun can e = Basics.can e ();
+
end;
--- a/src/Pure/ML/ml_antiquotations.ML Sun Sep 24 11:42:13 2023 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Sun Sep 24 15:07:40 2023 +0200
@@ -343,8 +343,8 @@
(* special forms for option type *)
val _ = Theory.setup
- (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "() |> Basics.try" #>
- ML_Antiquotation.special_form \<^binding>\<open>can\<close> "() |> Basics.can" #>
+ (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "Isabelle_Thread.try" #>
+ ML_Antiquotation.special_form \<^binding>\<open>can\<close> "Isabelle_Thread.can" #>
ML_Context.add_antiquotation \<^binding>\<open>if_none\<close> true
(fn _ => fn src => fn ctxt =>
let