--- a/NEWS Fri Apr 09 21:07:11 2021 +0200
+++ b/NEWS Fri Apr 09 22:06:59 2021 +0200
@@ -88,6 +88,10 @@
*** ML ***
+* ML antiquotations \<^try>\<open>expr\<close> and \<^can>\<open>expr\<close> operate directly on
+the given ML expression, in contrast to functions "try" and "can" that
+modify application of a function.
+
* External bash processes are always managed by Isabelle/Scala, in
contrast to Isabelle2021 where this was only done for macOS on Apple
Silicon.
--- a/etc/symbols Fri Apr 09 21:07:11 2021 +0200
+++ b/etc/symbols Fri Apr 09 22:06:59 2021 +0200
@@ -442,6 +442,7 @@
\<^action> code: 0x00261b group: icon argument: cartouche font: Isabelle␣DejaVu␣Sans␣Mono
\<^assert>
\<^binding> argument: cartouche
+\<^can> argument: cartouche
\<^class> argument: cartouche
\<^class_syntax> argument: cartouche
\<^command_keyword> argument: cartouche
@@ -480,6 +481,7 @@
\<^theory> argument: cartouche
\<^theory_context> argument: cartouche
\<^tool> argument: cartouche
+\<^try> argument: cartouche
\<^typ> argument: cartouche
\<^type_abbrev> argument: cartouche
\<^type_name> argument: cartouche
--- a/src/HOL/Library/Countable.thy Fri Apr 09 21:07:11 2021 +0200
+++ b/src/HOL/Library/Countable.thy Fri Apr 09 22:06:59 2021 +0200
@@ -204,7 +204,7 @@
ML \<open>
fun countable_datatype_tac ctxt st =
- (case try (fn () => HEADGOAL (old_countable_datatype_tac ctxt) st) () of
+ (case \<^try>\<open>HEADGOAL (old_countable_datatype_tac ctxt) st\<close> of
SOME res => res
| NONE => BNF_LFP_Countable.countable_datatype_tac ctxt st);
--- a/src/HOL/Tools/Qelim/cooper.ML Fri Apr 09 21:07:11 2021 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri Apr 09 22:06:59 2021 +0200
@@ -739,8 +739,7 @@
in
if ntac then no_tac
else
- (case try (fn () =>
- Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))) () of
+ (case \<^try>\<open>Goal.prove_internal ctxt [] g (K (blast_tac (put_claset HOL_cs ctxt) 1))\<close> of
NONE => no_tac
| SOME r => resolve_tac ctxt [r] i)
end)
--- a/src/Pure/General/antiquote.ML Fri Apr 09 21:07:11 2021 +0200
+++ b/src/Pure/General/antiquote.ML Fri Apr 09 22:06:59 2021 +0200
@@ -9,6 +9,7 @@
type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
+ val the_text: 'a antiquote -> 'a
type text_antiquote = Symbol_Pos.T list antiquote
val text_antiquote_range: text_antiquote -> Position.range
val text_range: text_antiquote list -> Position.range
@@ -32,6 +33,11 @@
type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
+fun bad_text pos = error ("Unexpected antiquotation" ^ Position.here pos);
+fun the_text (Text x) = x
+ | the_text (Control {range, ...}) = bad_text (#1 range)
+ | the_text (Antiq {range, ...}) = bad_text (#1 range);
+
type text_antiquote = Symbol_Pos.T list antiquote;
fun text_antiquote_range (Text ss) = Symbol_Pos.range ss
--- a/src/Pure/ML/ml_antiquotation.ML Fri Apr 09 21:07:11 2021 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Fri Apr 09 22:06:59 2021 +0200
@@ -18,6 +18,7 @@
val inline_embedded: binding -> string context_parser -> theory -> theory
val value: binding -> string context_parser -> theory -> theory
val value_embedded: binding -> string context_parser -> theory -> theory
+ val special_form: binding -> string -> theory -> theory
end;
structure ML_Antiquotation: ML_ANTIQUOTATION =
@@ -63,6 +64,26 @@
end;
+(* ML special form *)
+
+fun special_form binding operator =
+ ML_Context.add_antiquotation binding true
+ (fn _ => fn src => fn ctxt =>
+ let
+ val (s, _) = Token.syntax (Scan.lift Args.embedded_input) src ctxt;
+ val tokenize = ML_Lex.tokenize_range Position.no_range;
+ val tokenize_range = ML_Lex.tokenize_range (Input.range_of s);
+ fun decl (_: Proof.context) =
+ let
+ val expr = ML_Lex.read_source s |> map Antiquote.the_text;
+ val ml =
+ tokenize "let val expr = (fn () => " @ expr @ tokenize ");" @
+ tokenize " val " @ tokenize_range "result" @
+ tokenize (" = " ^ operator ^ " expr; in result end")
+ in ([], ml) end;
+ in (decl, ctxt) end);
+
+
(* basic antiquotations *)
val _ = Theory.setup
--- a/src/Pure/ML/ml_antiquotations.ML Fri Apr 09 21:07:11 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Fri Apr 09 22:06:59 2021 +0200
@@ -180,6 +180,13 @@
in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
+(* special forms *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.special_form \<^binding>\<open>try\<close> "() |> Basics.try" #>
+ ML_Antiquotation.special_form \<^binding>\<open>can\<close> "() |> Basics.can");
+
+
(* basic combinators *)
local