# 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>\<open>lemma\<close>
-    (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
     "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
-    "\<subseteq>" "]" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
+    "\<subseteq>" "]" "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>\<open>lemma\<close>
-    (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)