# HG changeset patch # User wenzelm # Date 1635415798 -7200 # Node ID b7804cff55d9c897a508c2cd4349d6bd3d7c8730 # Parent c6610137a092e6b749e6b73321190709748f0017 clarified keywords: major take precedence for commands, but not used for antiquotations; clarified modules; diff -r c6610137a092 -r b7804cff55d9 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Oct 28 11:37:49 2021 +0200 +++ b/src/Pure/Isar/method.ML Thu Oct 28 12:09:58 2021 +0200 @@ -90,6 +90,7 @@ val report: text_range -> unit val parser: int -> text_range parser val parse: text_range parser + val parse_by: ((text_range * text_range option) * Position.report list) parser val read: Proof.context -> Token.src -> text val read_closure: Proof.context -> Token.src -> text * Token.src val read_closure_input: Proof.context -> Input.source -> text * Token.src @@ -722,6 +723,10 @@ end; +val parse_by = + Parse.$$$ "by" |-- parse -- Scan.option parse + >> (fn (m1, m2) => ((m1, m2), maps reports_of (m1 :: the_list m2))); + (* read method text *) diff -r c6610137a092 -r b7804cff55d9 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Thu Oct 28 11:37:49 2021 +0200 +++ b/src/Pure/ML/ml_thms.ML Thu Oct 28 12:09:58 2021 +0200 @@ -75,19 +75,12 @@ (* ad-hoc goals *) -val and_ = Args.$$$ "and"; -val by = Parse.reserved "by"; -val goal = Scan.unless (by || and_) Parse.embedded_inner_syntax; - val _ = Theory.setup (ML_Antiquotation.declaration \<^binding>\lemma\ - (Scan.lift (Args.mode "open" -- Parse.enum1 "and" (Scan.repeat1 goal) -- - (Parse.position by -- Method.parse -- Scan.option Method.parse))) - (fn _ => fn ((is_open, raw_propss), (((_, by_pos), m1), m2)) => fn ctxt => + (Scan.lift (Args.mode "open" -- Parse.and_list1 (Scan.repeat1 Parse.embedded_inner_syntax) -- + Method.parse_by)) + (fn _ => fn ((is_open, raw_propss), (methods, reports)) => fn ctxt => let - val reports = - (by_pos, Markup.keyword1 |> Markup.keyword_properties) :: - maps Method.reports_of (m1 :: the_list m2); val _ = Context_Position.reports ctxt reports; val propss = burrow (map (rpair []) o Syntax.read_props ctxt) raw_propss; @@ -98,7 +91,7 @@ val ctxt' = ctxt |> Proof.theorem NONE after_qed propss - |> Proof.global_terminal_proof (m1, m2); + |> Proof.global_terminal_proof methods; val thms = Proof_Context.get_fact ctxt' (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN))); diff -r c6610137a092 -r b7804cff55d9 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Thu Oct 28 11:37:49 2021 +0200 +++ b/src/Pure/Pure.thy Thu Oct 28 12:09:58 2021 +0200 @@ -7,7 +7,7 @@ theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" - "\" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" + "\" "]" "binder" "by" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" diff -r c6610137a092 -r b7804cff55d9 src/Pure/Thy/document_antiquotations.ML --- a/src/Pure/Thy/document_antiquotations.ML Thu Oct 28 11:37:49 2021 +0200 +++ b/src/Pure/Thy/document_antiquotations.ML Thu Oct 28 12:09:58 2021 +0200 @@ -255,19 +255,15 @@ val _ = Theory.setup (Document_Antiquotation.setup \<^binding>\lemma\ - (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- - Scan.lift (Parse.position (Parse.reserved "by") -- Method.parse -- Scan.option Method.parse)) - (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (((_, by_pos), m1), m2))} => + (Scan.lift (Scan.ahead Parse.not_eof) -- Args.prop -- Scan.lift Method.parse_by) + (fn {context = ctxt, source = src, argument = ((prop_tok, prop), (methods, reports))} => let - val reports = - (by_pos, Markup.keyword1 |> Markup.keyword_properties) :: - maps Method.reports_of (m1 :: the_list m2); val _ = Context_Position.reports ctxt reports; (* FIXME check proof!? *) val _ = ctxt |> Proof.theorem NONE (K I) [[(prop, [])]] - |> Proof.global_terminal_proof (m1, m2); + |> Proof.global_terminal_proof methods; in Document_Output.pretty_source ctxt {embedded = false} [hd src, prop_tok] (Document_Output.pretty_term ctxt prop)