# HG changeset patch # User wenzelm # Date 1634741110 -7200 # Node ID 9189d949abb90bf64cf54e1f21404db201142ac4 # Parent 44dc1661a5cb442d87691d590c72efe8d0a56bb0 clarified modules; diff -r 44dc1661a5cb -r 9189d949abb9 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Oct 20 16:36:49 2021 +0200 +++ b/src/Pure/Isar/locale.ML Wed Oct 20 16:45:10 2021 +0200 @@ -186,6 +186,11 @@ val intern = Name_Space.intern o locale_space; fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); +val _ = Theory.setup + (ML_Antiquotation.inline_embedded \<^binding>\locale\ + (Args.theory -- Scan.lift Args.embedded_position >> + (ML_Syntax.print_string o uncurry check))); + fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy); fun markup_extern ctxt = diff -r 44dc1661a5cb -r 9189d949abb9 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Oct 20 16:36:49 2021 +0200 +++ b/src/Pure/Isar/method.ML Wed Oct 20 16:45:10 2021 +0200 @@ -426,6 +426,11 @@ | checked_text (Basic _) = true | checked_text (Combinator (_, _, body)) = forall checked_text body; +val _ = Theory.setup + (ML_Antiquotation.inline_embedded \<^binding>\method\ + (Args.context -- Scan.lift Args.embedded_position >> + (ML_Syntax.print_string o uncurry check_name))); + (* method setup *) diff -r 44dc1661a5cb -r 9189d949abb9 src/Pure/ML/ml_antiquotations.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_antiquotations.ML Wed Oct 20 16:45:10 2021 +0200 @@ -0,0 +1,494 @@ +(* Title: Pure/ML/ml_antiquotations.ML + Author: Makarius + +Miscellaneous ML antiquotations. +*) + +signature ML_ANTIQUOTATIONS = +sig + val make_judgment: Proof.context -> term -> term + val dest_judgment: Proof.context -> term -> term +end; + +structure ML_Antiquotations: ML_ANTIQUOTATIONS = +struct + +(* ML support *) + +val _ = Theory.setup + (ML_Antiquotation.inline \<^binding>\undefined\ + (Scan.succeed "(raise General.Match)") #> + + ML_Antiquotation.inline \<^binding>\assert\ + (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> + + ML_Antiquotation.declaration_embedded \<^binding>\print\ + (Scan.lift (Scan.optional Args.embedded "Output.writeln")) + (fn src => fn output => fn ctxt => + let + val struct_name = ML_Context.struct_name ctxt; + val (_, pos) = Token.name_of_src src; + val (a, ctxt') = ML_Context.variant "output" ctxt; + val env = + "val " ^ a ^ ": string -> unit =\n\ + \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ + ML_Syntax.print_position pos ^ "));\n"; + val body = + "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; + in (K (env, body), ctxt') end) #> + + ML_Antiquotation.value \<^binding>\rat\ + (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- + Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => + "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #> + + ML_Antiquotation.conditional \<^binding>\if_linux\ (fn _ => ML_System.platform_is_linux) #> + ML_Antiquotation.conditional \<^binding>\if_macos\ (fn _ => ML_System.platform_is_macos) #> + ML_Antiquotation.conditional \<^binding>\if_windows\ (fn _ => ML_System.platform_is_windows) #> + ML_Antiquotation.conditional \<^binding>\if_unix\ (fn _ => ML_System.platform_is_unix)); + + +(* formal entities *) + +val _ = Theory.setup + (ML_Antiquotation.value_embedded \<^binding>\system_option\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => + (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> + + ML_Antiquotation.value_embedded \<^binding>\theory\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => + (Theory.check {long = false} ctxt (name, pos); + "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.print_string name)) + || Scan.succeed "Proof_Context.theory_of ML_context") #> + + ML_Antiquotation.value_embedded \<^binding>\theory_context\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => + (Theory.check {long = false} ctxt (name, pos); + "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.print_string name))) #> + + ML_Antiquotation.inline \<^binding>\context\ + (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> + + ML_Antiquotation.inline_embedded \<^binding>\typ\ + (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> + + ML_Antiquotation.inline_embedded \<^binding>\term\ + (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> + + ML_Antiquotation.inline_embedded \<^binding>\prop\ + (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> + + ML_Antiquotation.value_embedded \<^binding>\ctyp\ (Args.typ >> (fn T => + "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> + + ML_Antiquotation.value_embedded \<^binding>\cterm\ (Args.term >> (fn t => + "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> + + ML_Antiquotation.value_embedded \<^binding>\cprop\ (Args.prop >> (fn t => + "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> + + ML_Antiquotation.inline_embedded \<^binding>\oracle_name\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => + ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos))))); + + +(* schematic variables *) + +val schematic_input = + Args.context -- Scan.lift Args.embedded_input >> (fn (ctxt, src) => + (Proof_Context.set_mode Proof_Context.mode_schematic ctxt, + (Syntax.implode_input src, Input.pos_of src))); + +val _ = Theory.setup + (ML_Antiquotation.inline_embedded \<^binding>\tvar\ + (schematic_input >> (fn (ctxt, (s, pos)) => + (case Syntax.read_typ ctxt s of + TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v + | _ => error ("Schematic type variable expected" ^ Position.here pos)))) #> + ML_Antiquotation.inline_embedded \<^binding>\var\ + (schematic_input >> (fn (ctxt, (s, pos)) => + (case Syntax.read_term ctxt s of + Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v + | _ => error ("Schematic variable expected" ^ Position.here pos))))); + + +(* type classes *) + +fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => + Proof_Context.read_class ctxt s + |> syn ? Lexicon.mark_class + |> ML_Syntax.print_string); + +val _ = Theory.setup + (ML_Antiquotation.inline_embedded \<^binding>\class\ (class false) #> + ML_Antiquotation.inline_embedded \<^binding>\class_syntax\ (class true) #> + + ML_Antiquotation.inline_embedded \<^binding>\sort\ + (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => + ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); + + +(* type constructors *) + +fun type_name kind check = Args.context -- Scan.lift Args.embedded_token + >> (fn (ctxt, tok) => + let + val s = Token.inner_syntax_of tok; + val (_, pos) = Input.source_content (Token.input_of tok); + val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; + val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); + val res = + (case try check (c, decl) of + SOME res => res + | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); + in ML_Syntax.print_string res end); + +val _ = Theory.setup + (ML_Antiquotation.inline_embedded \<^binding>\type_name\ + (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> + ML_Antiquotation.inline_embedded \<^binding>\type_abbrev\ + (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> + ML_Antiquotation.inline_embedded \<^binding>\nonterminal\ + (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> + ML_Antiquotation.inline_embedded \<^binding>\type_syntax\ + (type_name "type" (fn (c, _) => Lexicon.mark_type c))); + + +(* constants *) + +fun const_name check = Args.context -- Scan.lift Args.embedded_token + >> (fn (ctxt, tok) => + let + val s = Token.inner_syntax_of tok; + val (_, pos) = Input.source_content (Token.input_of tok); + val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; + val res = check (Proof_Context.consts_of ctxt, c) + handle TYPE (msg, _, _) => error (msg ^ Position.here pos); + in ML_Syntax.print_string res end); + +val _ = Theory.setup + (ML_Antiquotation.inline_embedded \<^binding>\const_name\ + (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> + ML_Antiquotation.inline_embedded \<^binding>\const_abbrev\ + (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> + ML_Antiquotation.inline_embedded \<^binding>\const_syntax\ + (const_name (fn (_, c) => Lexicon.mark_const c)) #> + + ML_Antiquotation.inline_embedded \<^binding>\syntax_const\ + (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => + ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #> + + ML_Antiquotation.inline_embedded \<^binding>\const\ + (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional + (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] + >> (fn ((ctxt, (raw_c, pos)), Ts) => + let + val Const (c, _) = + Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; + val consts = Proof_Context.consts_of ctxt; + val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); + val _ = length Ts <> n andalso + error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ + quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); + val const = Const (c, Consts.instance consts (c, Ts)); + in ML_Syntax.atomic (ML_Syntax.print_term const) end))); + + +(* object-logic judgment *) + +fun make_judgment ctxt = + let val const = Object_Logic.judgment_const ctxt + in fn t => Const const $ t end; + +fun dest_judgment ctxt = + let + val is_judgment = Object_Logic.is_judgment ctxt; + val drop_judgment = Object_Logic.drop_judgment ctxt; + in + fn t => + if is_judgment t then drop_judgment t + else raise TERM ("dest_judgment", [t]) + end; + +val _ = Theory.setup + (ML_Antiquotation.value \<^binding>\make_judgment\ + (Scan.succeed "ML_Antiquotations.make_judgment ML_context") #> + ML_Antiquotation.value \<^binding>\dest_judgment\ + (Scan.succeed "ML_Antiquotations.dest_judgment ML_context")); + + +(* type/term constructors *) + +fun read_embedded ctxt keywords src parse = + let + val input = #1 (Token.syntax (Scan.lift Args.embedded_input) src ctxt); + val toks = input + |> Input.source_explode + |> Token.tokenize keywords {strict = true} + |> filter Token.is_proper; + val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks); + in + (case Scan.read Token.stopper parse toks of + SOME res => res + | NONE => error ("Bad input" ^ Position.here (Input.pos_of input))) + end; + +val parse_embedded_ml = + Parse.embedded_input >> ML_Lex.read_source || + Parse.control >> (ML_Lex.read_symbols o Antiquote.control_symbols); + +val parse_embedded_ml_underscore = + Parse.input Parse.underscore >> ML_Lex.read_source || parse_embedded_ml; + +fun ml_args ctxt args = + let + val (decls, ctxt') = fold_map (ML_Context.expand_antiquotes) args ctxt; + fun decl' ctxt'' = map (fn decl => decl ctxt'') decls; + in (decl', ctxt') end + +local + +val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords; + +val parse_name = Parse.input Parse.name; + +val parse_args = Scan.repeat parse_embedded_ml_underscore; +val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) []; + +fun parse_body b = + if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single) + else Scan.succeed []; + +fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_" + | is_dummy _ = false; + +val ml = ML_Lex.tokenize_no_range; +val ml_range = ML_Lex.tokenize_range; +val ml_dummy = ml "_"; +fun ml_enclose range x = ml "(" @ x @ ml_range range ")"; +fun ml_parens x = ml "(" @ x @ ml ")"; +fun ml_bracks x = ml "[" @ x @ ml "]"; +fun ml_commas xs = flat (separate (ml ", ") xs); +val ml_list = ml_bracks o ml_commas; +val ml_string = ml o ML_Syntax.print_string; +fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); + +fun type_antiquotation binding {function} = + ML_Context.add_antiquotation binding true + (fn range => fn src => fn ctxt => + let + val ((s, type_args), fn_body) = + read_embedded ctxt keywords src (parse_name -- parse_args -- parse_body function); + val pos = Input.pos_of s; + + val Type (c, Ts) = + Proof_Context.read_type_name {proper = true, strict = true} ctxt + (Syntax.implode_input s); + val n = length Ts; + val _ = + length type_args = n orelse + error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^ + " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos); + + val (decls1, ctxt1) = ml_args ctxt type_args; + val (decls2, ctxt2) = ml_args ctxt1 fn_body; + fun decl' ctxt' = + let + val (ml_args_env, ml_args_body) = split_list (decls1 ctxt'); + val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt'); + val ml1 = + ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body)); + val ml2 = + if function then + ml_enclose range + (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ + ml "| T => " @ ml_range range "raise" @ + ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])") + else ml1; + in (flat (ml_args_env @ ml_fn_env), ml2) end; + in (decl', ctxt2) end); + +fun const_antiquotation binding {pattern, function} = + ML_Context.add_antiquotation binding true + (fn range => fn src => fn ctxt => + let + val (((s, type_args), term_args), fn_body) = + read_embedded ctxt keywords src + (parse_name -- parse_args -- parse_for_args -- parse_body function); + + val Const (c, T) = + Proof_Context.read_const {proper = true, strict = true} ctxt + (Syntax.implode_input s); + + val consts = Proof_Context.consts_of ctxt; + val type_paths = Consts.type_arguments consts c; + val type_params = map Term.dest_TVar (Consts.typargs consts (c, T)); + + val n = length type_params; + val m = length (Term.binder_types T); + + fun err msg = + error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^ + Position.here (Input.pos_of s)); + val _ = + length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)"); + val _ = + length term_args > m andalso Term.is_Type (Term.body_type T) andalso + err (" cannot have more than " ^ string_of_int m ^ " argument(s)"); + + val (decls1, ctxt1) = ml_args ctxt type_args; + val (decls2, ctxt2) = ml_args ctxt1 term_args; + val (decls3, ctxt3) = ml_args ctxt2 fn_body; + fun decl' ctxt' = + let + val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt'); + val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt'); + val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt'); + + val relevant = map is_dummy type_args ~~ type_paths; + fun relevant_path is = + not pattern orelse + let val p = rev is + in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end; + + val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1); + fun ml_typ is (Type (d, Us)) = + if relevant_path is then + ml "Term.Type " @ + ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us)) + else ml_dummy + | ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy + | ml_typ _ (TFree _) = raise Match; + + fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T) + | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u); + + val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env); + val ml1 = ml_enclose range (ml_app (rev ml_args_body2)); + val ml2 = + if function then + ml_enclose range + (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ + ml "| t => " @ ml_range range "raise" @ + ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])") + else ml1; + in (ml_env, ml2) end; + in (decl', ctxt3) end); + +val _ = Theory.setup + (type_antiquotation \<^binding>\Type\ {function = false} #> + type_antiquotation \<^binding>\Type_fn\ {function = true} #> + const_antiquotation \<^binding>\Const\ {pattern = false, function = false} #> + const_antiquotation \<^binding>\Const_\ {pattern = true, function = false} #> + const_antiquotation \<^binding>\Const_fn\ {pattern = true, function = true}); + +in end; + + +(* special forms *) + +val _ = Theory.setup + (ML_Antiquotation.special_form \<^binding>\try\ "() |> Basics.try" #> + ML_Antiquotation.special_form \<^binding>\can\ "() |> Basics.can"); + + +(* basic combinators *) + +local + +val parameter = Parse.position Parse.nat >> (fn (n, pos) => + if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); + +fun indices n = map string_of_int (1 upto n); + +fun empty n = replicate_string n " []"; +fun dummy n = replicate_string n " _"; +fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); +fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); + +val tuple = enclose "(" ")" o commas; +fun tuple_empty n = tuple (replicate n "[]"); +fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); +fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" +fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); + +in + +val _ = Theory.setup + (ML_Antiquotation.value \<^binding>\map\ + (Scan.lift parameter >> (fn n => + "fn f =>\n\ + \ let\n\ + \ fun map _" ^ empty n ^ " = []\n\ + \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ + \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ + " in map f end")) #> + ML_Antiquotation.value \<^binding>\fold\ + (Scan.lift parameter >> (fn n => + "fn f =>\n\ + \ let\n\ + \ fun fold _" ^ empty n ^ " a = a\n\ + \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ + \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ + " in fold f end")) #> + ML_Antiquotation.value \<^binding>\fold_map\ + (Scan.lift parameter >> (fn n => + "fn f =>\n\ + \ let\n\ + \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ + \ | fold_map f" ^ cons n ^ " a =\n\ + \ let\n\ + \ val (x, a') = f" ^ vars "x" n ^ " a\n\ + \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ + \ in (x :: xs, a'') end\n\ + \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ + " in fold_map f end")) #> + ML_Antiquotation.value \<^binding>\split_list\ + (Scan.lift parameter >> (fn n => + "fn list =>\n\ + \ let\n\ + \ fun split_list [] =" ^ tuple_empty n ^ "\n\ + \ | split_list" ^ tuple_cons n ^ " =\n\ + \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ + \ in " ^ cons_tuple n ^ "end\n\ + \ in split_list list end")) #> + ML_Antiquotation.value \<^binding>\apply\ + (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> + (fn (n, opt_index) => + let + val cond = + (case opt_index of + NONE => K true + | SOME (index, index_pos) => + if 1 <= index andalso index <= n then equal (string_of_int index) + else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos)); + in + "fn f => fn " ^ tuple_vars "x" n ^ " => " ^ + tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n)) + end))); + +end; + + +(* outer syntax *) + +val _ = Theory.setup + (ML_Antiquotation.value_embedded \<^binding>\keyword\ + (Args.context -- + Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true))) + >> (fn (ctxt, (name, pos)) => + if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then + (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); + "Parse.$$$ " ^ ML_Syntax.print_string name) + else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> + ML_Antiquotation.value_embedded \<^binding>\command_keyword\ + (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => + (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of + SOME markup => + (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; + ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) + | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); + +end; diff -r 44dc1661a5cb -r 9189d949abb9 src/Pure/ML/ml_antiquotations1.ML --- a/src/Pure/ML/ml_antiquotations1.ML Wed Oct 20 16:36:49 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,494 +0,0 @@ -(* Title: Pure/ML/ml_antiquotations1.ML - Author: Makarius - -Miscellaneous ML antiquotations: part 1. -*) - -signature ML_ANTIQUOTATIONS1 = -sig - val make_judgment: Proof.context -> term -> term - val dest_judgment: Proof.context -> term -> term -end; - -structure ML_Antiquotations1: ML_ANTIQUOTATIONS1 = -struct - -(* ML support *) - -val _ = Theory.setup - (ML_Antiquotation.inline \<^binding>\undefined\ - (Scan.succeed "(raise General.Match)") #> - - ML_Antiquotation.inline \<^binding>\assert\ - (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> - - ML_Antiquotation.declaration_embedded \<^binding>\print\ - (Scan.lift (Scan.optional Args.embedded "Output.writeln")) - (fn src => fn output => fn ctxt => - let - val struct_name = ML_Context.struct_name ctxt; - val (_, pos) = Token.name_of_src src; - val (a, ctxt') = ML_Context.variant "output" ctxt; - val env = - "val " ^ a ^ ": string -> unit =\n\ - \ (" ^ output ^ ") o (fn s => s ^ Position.here (" ^ - ML_Syntax.print_position pos ^ "));\n"; - val body = - "(fn x => (" ^ struct_name ^ "." ^ a ^ " (" ^ ML_Pretty.make_string_fn ^ " x); x))"; - in (K (env, body), ctxt') end) #> - - ML_Antiquotation.value \<^binding>\rat\ - (Scan.lift (Scan.optional (Args.$$$ "~" >> K ~1) 1 -- Parse.nat -- - Scan.optional (Args.$$$ "/" |-- Parse.nat) 1) >> (fn ((sign, a), b) => - "Rat.make " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int (sign * a, b))) #> - - ML_Antiquotation.conditional \<^binding>\if_linux\ (fn _ => ML_System.platform_is_linux) #> - ML_Antiquotation.conditional \<^binding>\if_macos\ (fn _ => ML_System.platform_is_macos) #> - ML_Antiquotation.conditional \<^binding>\if_windows\ (fn _ => ML_System.platform_is_windows) #> - ML_Antiquotation.conditional \<^binding>\if_unix\ (fn _ => ML_System.platform_is_unix)); - - -(* formal entities *) - -val _ = Theory.setup - (ML_Antiquotation.value_embedded \<^binding>\system_option\ - (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => - (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #> - - ML_Antiquotation.value_embedded \<^binding>\theory\ - (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => - (Theory.check {long = false} ctxt (name, pos); - "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^ - ML_Syntax.print_string name)) - || Scan.succeed "Proof_Context.theory_of ML_context") #> - - ML_Antiquotation.value_embedded \<^binding>\theory_context\ - (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => - (Theory.check {long = false} ctxt (name, pos); - "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ - ML_Syntax.print_string name))) #> - - ML_Antiquotation.inline \<^binding>\context\ - (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #> - - ML_Antiquotation.inline_embedded \<^binding>\typ\ - (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> - - ML_Antiquotation.inline_embedded \<^binding>\term\ - (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> - - ML_Antiquotation.inline_embedded \<^binding>\prop\ - (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> - - ML_Antiquotation.value_embedded \<^binding>\ctyp\ (Args.typ >> (fn T => - "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #> - - ML_Antiquotation.value_embedded \<^binding>\cterm\ (Args.term >> (fn t => - "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> - - ML_Antiquotation.value_embedded \<^binding>\cprop\ (Args.prop >> (fn t => - "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #> - - ML_Antiquotation.inline_embedded \<^binding>\oracle_name\ - (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) => - ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos))))); - - -(* schematic variables *) - -val schematic_input = - Args.context -- Scan.lift Args.embedded_input >> (fn (ctxt, src) => - (Proof_Context.set_mode Proof_Context.mode_schematic ctxt, - (Syntax.implode_input src, Input.pos_of src))); - -val _ = Theory.setup - (ML_Antiquotation.inline_embedded \<^binding>\tvar\ - (schematic_input >> (fn (ctxt, (s, pos)) => - (case Syntax.read_typ ctxt s of - TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v - | _ => error ("Schematic type variable expected" ^ Position.here pos)))) #> - ML_Antiquotation.inline_embedded \<^binding>\var\ - (schematic_input >> (fn (ctxt, (s, pos)) => - (case Syntax.read_term ctxt s of - Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v - | _ => error ("Schematic variable expected" ^ Position.here pos))))); - - -(* type classes *) - -fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => - Proof_Context.read_class ctxt s - |> syn ? Lexicon.mark_class - |> ML_Syntax.print_string); - -val _ = Theory.setup - (ML_Antiquotation.inline_embedded \<^binding>\class\ (class false) #> - ML_Antiquotation.inline_embedded \<^binding>\class_syntax\ (class true) #> - - ML_Antiquotation.inline_embedded \<^binding>\sort\ - (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) => - ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); - - -(* type constructors *) - -fun type_name kind check = Args.context -- Scan.lift Args.embedded_token - >> (fn (ctxt, tok) => - let - val s = Token.inner_syntax_of tok; - val (_, pos) = Input.source_content (Token.input_of tok); - val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; - val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); - val res = - (case try check (c, decl) of - SOME res => res - | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); - in ML_Syntax.print_string res end); - -val _ = Theory.setup - (ML_Antiquotation.inline_embedded \<^binding>\type_name\ - (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> - ML_Antiquotation.inline_embedded \<^binding>\type_abbrev\ - (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> - ML_Antiquotation.inline_embedded \<^binding>\nonterminal\ - (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> - ML_Antiquotation.inline_embedded \<^binding>\type_syntax\ - (type_name "type" (fn (c, _) => Lexicon.mark_type c))); - - -(* constants *) - -fun const_name check = Args.context -- Scan.lift Args.embedded_token - >> (fn (ctxt, tok) => - let - val s = Token.inner_syntax_of tok; - val (_, pos) = Input.source_content (Token.input_of tok); - val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; - val res = check (Proof_Context.consts_of ctxt, c) - handle TYPE (msg, _, _) => error (msg ^ Position.here pos); - in ML_Syntax.print_string res end); - -val _ = Theory.setup - (ML_Antiquotation.inline_embedded \<^binding>\const_name\ - (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> - ML_Antiquotation.inline_embedded \<^binding>\const_abbrev\ - (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> - ML_Antiquotation.inline_embedded \<^binding>\const_syntax\ - (const_name (fn (_, c) => Lexicon.mark_const c)) #> - - ML_Antiquotation.inline_embedded \<^binding>\syntax_const\ - (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) => - ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #> - - ML_Antiquotation.inline_embedded \<^binding>\const\ - (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional - (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] - >> (fn ((ctxt, (raw_c, pos)), Ts) => - let - val Const (c, _) = - Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; - val consts = Proof_Context.consts_of ctxt; - val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); - val _ = length Ts <> n andalso - error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ - quote c ^ enclose "(" ")" (commas (replicate n "_")) ^ Position.here pos); - val const = Const (c, Consts.instance consts (c, Ts)); - in ML_Syntax.atomic (ML_Syntax.print_term const) end))); - - -(* object-logic judgment *) - -fun make_judgment ctxt = - let val const = Object_Logic.judgment_const ctxt - in fn t => Const const $ t end; - -fun dest_judgment ctxt = - let - val is_judgment = Object_Logic.is_judgment ctxt; - val drop_judgment = Object_Logic.drop_judgment ctxt; - in - fn t => - if is_judgment t then drop_judgment t - else raise TERM ("dest_judgment", [t]) - end; - -val _ = Theory.setup - (ML_Antiquotation.value \<^binding>\make_judgment\ - (Scan.succeed "ML_Antiquotations1.make_judgment ML_context") #> - ML_Antiquotation.value \<^binding>\dest_judgment\ - (Scan.succeed "ML_Antiquotations1.dest_judgment ML_context")); - - -(* type/term constructors *) - -fun read_embedded ctxt keywords src parse = - let - val input = #1 (Token.syntax (Scan.lift Args.embedded_input) src ctxt); - val toks = input - |> Input.source_explode - |> Token.tokenize keywords {strict = true} - |> filter Token.is_proper; - val _ = Context_Position.reports_text ctxt (maps (Token.reports keywords) toks); - in - (case Scan.read Token.stopper parse toks of - SOME res => res - | NONE => error ("Bad input" ^ Position.here (Input.pos_of input))) - end; - -val parse_embedded_ml = - Parse.embedded_input >> ML_Lex.read_source || - Parse.control >> (ML_Lex.read_symbols o Antiquote.control_symbols); - -val parse_embedded_ml_underscore = - Parse.input Parse.underscore >> ML_Lex.read_source || parse_embedded_ml; - -fun ml_args ctxt args = - let - val (decls, ctxt') = fold_map (ML_Context.expand_antiquotes) args ctxt; - fun decl' ctxt'' = map (fn decl => decl ctxt'') decls; - in (decl', ctxt') end - -local - -val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords; - -val parse_name = Parse.input Parse.name; - -val parse_args = Scan.repeat parse_embedded_ml_underscore; -val parse_for_args = Scan.optional (Parse.$$$ "for" |-- Parse.!!! parse_args) []; - -fun parse_body b = - if b then Parse.$$$ "=>" |-- Parse.!!! Parse.embedded_input >> (ML_Lex.read_source #> single) - else Scan.succeed []; - -fun is_dummy [Antiquote.Text tok] = ML_Lex.content_of tok = "_" - | is_dummy _ = false; - -val ml = ML_Lex.tokenize_no_range; -val ml_range = ML_Lex.tokenize_range; -val ml_dummy = ml "_"; -fun ml_enclose range x = ml "(" @ x @ ml_range range ")"; -fun ml_parens x = ml "(" @ x @ ml ")"; -fun ml_bracks x = ml "[" @ x @ ml "]"; -fun ml_commas xs = flat (separate (ml ", ") xs); -val ml_list = ml_bracks o ml_commas; -val ml_string = ml o ML_Syntax.print_string; -fun ml_pair (x, y) = ml_parens (ml_commas [x, y]); - -fun type_antiquotation binding {function} = - ML_Context.add_antiquotation binding true - (fn range => fn src => fn ctxt => - let - val ((s, type_args), fn_body) = - read_embedded ctxt keywords src (parse_name -- parse_args -- parse_body function); - val pos = Input.pos_of s; - - val Type (c, Ts) = - Proof_Context.read_type_name {proper = true, strict = true} ctxt - (Syntax.implode_input s); - val n = length Ts; - val _ = - length type_args = n orelse - error ("Type constructor " ^ quote (Proof_Context.markup_type ctxt c) ^ - " takes " ^ string_of_int n ^ " argument(s)" ^ Position.here pos); - - val (decls1, ctxt1) = ml_args ctxt type_args; - val (decls2, ctxt2) = ml_args ctxt1 fn_body; - fun decl' ctxt' = - let - val (ml_args_env, ml_args_body) = split_list (decls1 ctxt'); - val (ml_fn_env, ml_fn_body) = split_list (decls2 ctxt'); - val ml1 = - ml_enclose range (ml "Term.Type " @ ml_pair (ml_string c, ml_list ml_args_body)); - val ml2 = - if function then - ml_enclose range - (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ - ml "| T => " @ ml_range range "raise" @ - ml " Term.TYPE (" @ ml_string ("Type_fn " ^ quote c) @ ml ", [T], [])") - else ml1; - in (flat (ml_args_env @ ml_fn_env), ml2) end; - in (decl', ctxt2) end); - -fun const_antiquotation binding {pattern, function} = - ML_Context.add_antiquotation binding true - (fn range => fn src => fn ctxt => - let - val (((s, type_args), term_args), fn_body) = - read_embedded ctxt keywords src - (parse_name -- parse_args -- parse_for_args -- parse_body function); - - val Const (c, T) = - Proof_Context.read_const {proper = true, strict = true} ctxt - (Syntax.implode_input s); - - val consts = Proof_Context.consts_of ctxt; - val type_paths = Consts.type_arguments consts c; - val type_params = map Term.dest_TVar (Consts.typargs consts (c, T)); - - val n = length type_params; - val m = length (Term.binder_types T); - - fun err msg = - error ("Constant " ^ quote (Proof_Context.markup_const ctxt c) ^ msg ^ - Position.here (Input.pos_of s)); - val _ = - length type_args <> n andalso err (" takes " ^ string_of_int n ^ " type argument(s)"); - val _ = - length term_args > m andalso Term.is_Type (Term.body_type T) andalso - err (" cannot have more than " ^ string_of_int m ^ " argument(s)"); - - val (decls1, ctxt1) = ml_args ctxt type_args; - val (decls2, ctxt2) = ml_args ctxt1 term_args; - val (decls3, ctxt3) = ml_args ctxt2 fn_body; - fun decl' ctxt' = - let - val (ml_args_env1, ml_args_body1) = split_list (decls1 ctxt'); - val (ml_args_env2, ml_args_body2) = split_list (decls2 ctxt'); - val (ml_fn_env, ml_fn_body) = split_list (decls3 ctxt'); - - val relevant = map is_dummy type_args ~~ type_paths; - fun relevant_path is = - not pattern orelse - let val p = rev is - in relevant |> exists (fn (u, q) => not u andalso is_prefix (op =) p q) end; - - val ml_typarg = the o AList.lookup (op =) (type_params ~~ ml_args_body1); - fun ml_typ is (Type (d, Us)) = - if relevant_path is then - ml "Term.Type " @ - ml_pair (ml_string d, ml_list (map_index (fn (i, U) => ml_typ (i :: is) U) Us)) - else ml_dummy - | ml_typ is (TVar arg) = if relevant_path is then ml_typarg arg else ml_dummy - | ml_typ _ (TFree _) = raise Match; - - fun ml_app [] = ml "Term.Const " @ ml_pair (ml_string c, ml_typ [] T) - | ml_app (u :: us) = ml "Term.$ " @ ml_pair (ml_app us, u); - - val ml_env = flat (ml_args_env1 @ ml_args_env2 @ ml_fn_env); - val ml1 = ml_enclose range (ml_app (rev ml_args_body2)); - val ml2 = - if function then - ml_enclose range - (ml_range range "fn " @ ml1 @ ml "=> " @ flat ml_fn_body @ - ml "| t => " @ ml_range range "raise" @ - ml " Term.TERM (" @ ml_string ("Const_fn " ^ quote c) @ ml ", [t])") - else ml1; - in (ml_env, ml2) end; - in (decl', ctxt3) end); - -val _ = Theory.setup - (type_antiquotation \<^binding>\Type\ {function = false} #> - type_antiquotation \<^binding>\Type_fn\ {function = true} #> - const_antiquotation \<^binding>\Const\ {pattern = false, function = false} #> - const_antiquotation \<^binding>\Const_\ {pattern = true, function = false} #> - const_antiquotation \<^binding>\Const_fn\ {pattern = true, function = true}); - -in end; - - -(* special forms *) - -val _ = Theory.setup - (ML_Antiquotation.special_form \<^binding>\try\ "() |> Basics.try" #> - ML_Antiquotation.special_form \<^binding>\can\ "() |> Basics.can"); - - -(* basic combinators *) - -local - -val parameter = Parse.position Parse.nat >> (fn (n, pos) => - if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos)); - -fun indices n = map string_of_int (1 upto n); - -fun empty n = replicate_string n " []"; -fun dummy n = replicate_string n " _"; -fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n)); -fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n)); - -val tuple = enclose "(" ")" o commas; -fun tuple_empty n = tuple (replicate n "[]"); -fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n)); -fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)" -fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n)); - -in - -val _ = Theory.setup - (ML_Antiquotation.value \<^binding>\map\ - (Scan.lift parameter >> (fn n => - "fn f =>\n\ - \ let\n\ - \ fun map _" ^ empty n ^ " = []\n\ - \ | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\ - \ | map _" ^ dummy n ^ " = raise ListPair.UnequalLengths\n" ^ - " in map f end")) #> - ML_Antiquotation.value \<^binding>\fold\ - (Scan.lift parameter >> (fn n => - "fn f =>\n\ - \ let\n\ - \ fun fold _" ^ empty n ^ " a = a\n\ - \ | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\ - \ | fold _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ - " in fold f end")) #> - ML_Antiquotation.value \<^binding>\fold_map\ - (Scan.lift parameter >> (fn n => - "fn f =>\n\ - \ let\n\ - \ fun fold_map _" ^ empty n ^ " a = ([], a)\n\ - \ | fold_map f" ^ cons n ^ " a =\n\ - \ let\n\ - \ val (x, a') = f" ^ vars "x" n ^ " a\n\ - \ val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\ - \ in (x :: xs, a'') end\n\ - \ | fold_map _" ^ dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^ - " in fold_map f end")) #> - ML_Antiquotation.value \<^binding>\split_list\ - (Scan.lift parameter >> (fn n => - "fn list =>\n\ - \ let\n\ - \ fun split_list [] =" ^ tuple_empty n ^ "\n\ - \ | split_list" ^ tuple_cons n ^ " =\n\ - \ let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\ - \ in " ^ cons_tuple n ^ "end\n\ - \ in split_list list end")) #> - ML_Antiquotation.value \<^binding>\apply\ - (Scan.lift (parameter -- Scan.option (Args.parens (Parse.position Parse.nat))) >> - (fn (n, opt_index) => - let - val cond = - (case opt_index of - NONE => K true - | SOME (index, index_pos) => - if 1 <= index andalso index <= n then equal (string_of_int index) - else error ("Bad index: " ^ string_of_int index ^ Position.here index_pos)); - in - "fn f => fn " ^ tuple_vars "x" n ^ " => " ^ - tuple (map (fn a => (if cond a then "f x" else "x") ^ a) (indices n)) - end))); - -end; - - -(* outer syntax *) - -val _ = Theory.setup - (ML_Antiquotation.value_embedded \<^binding>\keyword\ - (Args.context -- - Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true))) - >> (fn (ctxt, (name, pos)) => - if Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name then - (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name); - "Parse.$$$ " ^ ML_Syntax.print_string name) - else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #> - ML_Antiquotation.value_embedded \<^binding>\command_keyword\ - (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) => - (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of - SOME markup => - (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)]; - ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)) - | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos))))); - -end; diff -r 44dc1661a5cb -r 9189d949abb9 src/Pure/ML/ml_antiquotations2.ML --- a/src/Pure/ML/ml_antiquotations2.ML Wed Oct 20 16:36:49 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,19 +0,0 @@ -(* Title: Pure/ML/ml_antiquotations2.ML - Author: Makarius - -Miscellaneous ML antiquotations: part 2. -*) - -structure ML_Antiquotations2: sig end = -struct - -val _ = Theory.setup - (ML_Antiquotation.inline_embedded \<^binding>\method\ - (Args.context -- Scan.lift Args.embedded_position >> - (ML_Syntax.print_string o uncurry Method.check_name)) #> - - ML_Antiquotation.inline_embedded \<^binding>\locale\ - (Args.theory -- Scan.lift Args.embedded_position >> - (ML_Syntax.print_string o uncurry Locale.check))); - -end; diff -r 44dc1661a5cb -r 9189d949abb9 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Oct 20 16:36:49 2021 +0200 +++ b/src/Pure/ROOT.ML Wed Oct 20 16:45:10 2021 +0200 @@ -240,7 +240,7 @@ ML_file "ML/ml_context.ML"; ML_file "ML/ml_antiquotation.ML"; ML_file "ML/ml_compiler2.ML"; -ML_file "ML/ml_antiquotations1.ML"; +ML_file "ML/ml_antiquotations.ML"; section "Bootstrap phase 3: towards theory Pure and final ML toplevel setup"; @@ -303,7 +303,6 @@ (*theory documents*) ML_file "Thy/term_style.ML"; ML_file "Isar/outer_syntax.ML"; -ML_file "ML/ml_antiquotations2.ML"; ML_file "ML/ml_pid.ML"; ML_file "Thy/document_antiquotation.ML"; ML_file "Thy/document_output.ML";