--- a/src/HOL/Analysis/measurable.ML Fri Apr 09 22:06:59 2021 +0200
+++ b/src/HOL/Analysis/measurable.ML Sat Apr 10 14:55:50 2021 +0200
@@ -274,7 +274,7 @@
val t = HOLogic.mk_Trueprop (Thm.term_of redex);
fun tac {context = ctxt, prems = _ } =
SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt));
- in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
+ in \<^try>\<open>Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}\<close> end;
end
--- a/src/HOL/Tools/Meson/meson.ML Fri Apr 09 22:06:59 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Sat Apr 10 14:55:50 2021 +0200
@@ -97,7 +97,7 @@
(*FIXME: currently does not "rename variables apart"*)
fun first_order_resolve ctxt thA thB =
(case
- try (fn () =>
+ \<^try>\<open>
let val thy = Proof_Context.theory_of ctxt
val tmA = Thm.concl_of thA
val Const(\<^const_name>\<open>Pure.imp\<close>,_) $ tmB $ _ = Thm.prop_of thB
@@ -105,7 +105,7 @@
Pattern.first_order_match thy (tmB, tmA)
(Vartab.empty, Vartab.empty) |> snd
val insts = Vartab.fold (fn (xi, (_, t)) => cons (xi, Thm.cterm_of ctxt t)) tenv [];
- in thA RS (infer_instantiate ctxt insts thB) end) () of
+ in thA RS (infer_instantiate ctxt insts thB) end\<close> of
SOME th => th
| NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Apr 09 22:06:59 2021 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Apr 10 14:55:50 2021 +0200
@@ -166,9 +166,9 @@
SOME (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ _) => SOME (@{thm refl} RS thm)
| SOME _ => (case body_type (fastype_of lhs) of
Type (typ_name, _) =>
- try (fn () =>
+ \<^try>\<open>
#equiv_thm (the (Quotient_Info.lookup_quotients lthy typ_name))
- RS @{thm Equiv_Relations.equivp_reflp} RS thm) ()
+ RS @{thm Equiv_Relations.equivp_reflp} RS thm\<close>
| _ => NONE
)
| _ => NONE
--- a/src/Pure/General/antiquote.ML Fri Apr 09 22:06:59 2021 +0200
+++ b/src/Pure/General/antiquote.ML Sat Apr 10 14:55:50 2021 +0200
@@ -9,7 +9,8 @@
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
+ val is_text: 'a antiquote -> bool
+ val the_text: string -> '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
@@ -33,10 +34,15 @@
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);
+val is_text = fn Text _ => true | _ => false;
+
+fun the_text msg antiq =
+ let fun err pos = error (msg ^ Position.here pos) in
+ (case antiq of
+ Text x => x
+ | Control {range, ...} => err (#1 range)
+ | Antiq {range, ...} => err (#1 range))
+ end;
type text_antiquote = Symbol_Pos.T list antiquote;
--- a/src/Pure/ML/ml_antiquotation.ML Fri Apr 09 22:06:59 2021 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Sat Apr 10 14:55:50 2021 +0200
@@ -73,15 +73,17 @@
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) =
+
+ val (decl, ctxt') = ML_Context.expand_antiquotes (ML_Lex.read_source s) ctxt;
+ fun decl' ctxt'' =
let
- val expr = ML_Lex.read_source s |> map Antiquote.the_text;
- val ml =
- tokenize "let val expr = (fn () => " @ expr @ tokenize ");" @
+ val (ml_env, ml_body) = decl ctxt'';
+ val ml_body' =
+ tokenize "let val expr = (fn () => " @ ml_body @ tokenize ");" @
tokenize " val " @ tokenize_range "result" @
- tokenize (" = " ^ operator ^ " expr; in result end")
- in ([], ml) end;
- in (decl, ctxt) end);
+ tokenize (" = " ^ operator ^ " expr; in result end");
+ in (ml_env, ml_body') end;
+ in (decl', ctxt') end);
(* basic antiquotations *)
--- a/src/Pure/ML/ml_context.ML Fri Apr 09 22:06:59 2021 +0200
+++ b/src/Pure/ML/ml_context.ML Sat Apr 10 14:55:50 2021 +0200
@@ -13,6 +13,8 @@
type antiquotation = Position.range -> Token.src -> Proof.context -> decl * Proof.context
val add_antiquotation: binding -> bool -> antiquotation -> theory -> theory
val print_antiquotations: bool -> Proof.context -> unit
+ val expand_antiquotes: ML_Lex.token Antiquote.antiquote list ->
+ Proof.context -> decl * Proof.context
val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
val eval_file: ML_Compiler.flags -> Path.T -> unit
val eval_source: ML_Compiler.flags -> Input.source -> unit
@@ -90,13 +92,38 @@
in antiquotation range src' ctxt end;
-(* parsing and evaluation *)
+(* parsing *)
local
val antiq =
Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof);
+fun expand_antiquote ant ctxt =
+ (case ant of
+ Antiquote.Text tok => (K ([], [tok]), ctxt)
+ | Antiquote.Control {name, range, body} =>
+ ctxt |> apply_antiquotation range
+ (Token.make_src name (if null body then [] else [Token.read_cartouche body]))
+ | Antiquote.Antiq {range, body, ...} =>
+ ctxt |> apply_antiquotation range
+ (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)));
+
+in
+
+fun expand_antiquotes ants ctxt =
+ let
+ val (decls, ctxt') = fold_map expand_antiquote ants ctxt;
+ fun decl ctxt'' = decls |> map (fn d => d ctxt'') |> split_list |> apply2 flat;
+ in (decl, ctxt') end;
+
+end;
+
+
+(* evaluation *)
+
+local
+
fun make_env name visible =
(ML_Lex.tokenize
("structure " ^ name ^ " =\nstruct\n\
@@ -106,38 +133,22 @@
fun reset_env name = ML_Lex.tokenize ("structure " ^ name ^ " = struct end");
-fun eval_antiquotes (ants, pos) opt_context =
- let
- val visible =
- (case opt_context of
- SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt
- | _ => true);
- val opt_ctxt = Option.map Context.proof_of opt_context;
-
- val ((ml_env, ml_body), opt_ctxt') =
- if forall (fn Antiquote.Text _ => true | _ => false) ants
- then (([], map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
- else
- let
- fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
- | expand (Antiquote.Control {name, range, body}) ctxt =
- apply_antiquotation range
- (Token.make_src name (if null body then [] else [Token.read_cartouche body])) ctxt
- | expand (Antiquote.Antiq {range, body, ...}) ctxt =
- apply_antiquotation range
- (Token.read_antiq (Thy_Header.get_keywords' ctxt) antiq (body, #1 range)) ctxt;
-
- val ctxt =
- (case opt_ctxt of
- NONE => error ("No context -- cannot expand ML antiquotations" ^ Position.here pos)
- | SOME ctxt => struct_begin ctxt);
-
- val (begin_env, end_env) = make_env (struct_name ctxt) visible;
- val (decls, ctxt') = fold_map expand ants ctxt;
- val (ml_env, ml_body) =
- decls |> map (fn decl => decl ctxt') |> split_list |> apply2 flat;
- in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end;
- in ((ml_env, ml_body), opt_ctxt') end;
+fun eval_antiquotes ants opt_context =
+ if forall Antiquote.is_text ants orelse is_none opt_context then
+ (([], map (Antiquote.the_text "No context -- cannot expand ML antiquotations") ants),
+ Option.map Context.proof_of opt_context)
+ else
+ let
+ val context = the opt_context;
+ val visible =
+ (case context of
+ Context.Proof ctxt => Context_Position.is_visible ctxt
+ | _ => true);
+ val ctxt = struct_begin (Context.proof_of context);
+ val (begin_env, end_env) = make_env (struct_name ctxt) visible;
+ val (decl, ctxt') = expand_antiquotes ants ctxt;
+ val (ml_env, ml_body) = decl ctxt';
+ in ((begin_env @ ml_env @ end_env, ml_body), SOME ctxt') end;
in
@@ -146,7 +157,7 @@
val non_verbose = ML_Compiler.verbose false flags;
(*prepare source text*)
- val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.get_generic_context ());
+ val ((env, body), env_ctxt) = eval_antiquotes ants (Context.get_generic_context ());
val _ =
(case env_ctxt of
SOME ctxt =>