more explicit method reports;
avoid combinator parsers with observable effect -- unreliable due to backtracking (Scan.FAIL) and incremental input (Scan.MORE);

--- a/src/Pure/Isar/isar_syn.ML	Thu Feb 27 21:36:40 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Feb 28 10:40:04 2014 +0100
@@ -620,11 +620,12 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "qed"} "conclude proof"
-    (Scan.option Method.parse_report >> Isar_Cmd.qed);
+    (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m)));
 
 val _ =
   Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
-    (Method.parse_report -- Scan.option Method.parse_report >> Isar_Cmd.terminal_proof);
+    (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
+      (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2))));
 
 val _ =
   Outer_Syntax.command @{command_spec ".."} "default proof"
@@ -659,17 +660,21 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
-    (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
+    (Method.parse >> (fn m =>
+      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_results m))));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
-    (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
+    (Method.parse >> (fn m =>
+      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_end_results m))));
 
 val _ =
   Outer_Syntax.command @{command_spec "proof"} "backward proof step"
-    (Scan.option Method.parse_report >> (fn m => Toplevel.print o
-      Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
-      Toplevel.skip_proof (fn i => i + 1)));
+    (Scan.option Method.parse >> (fn m =>
+      (Option.map Method.report m;
+        Toplevel.print o
+        Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
+        Toplevel.skip_proof (fn i => i + 1))));
 
 
 (* proof navigation *)

--- a/src/Pure/Isar/method.ML	Thu Feb 27 21:36:40 2014 +0100
+++ b/src/Pure/Isar/method.ML	Fri Feb 28 10:40:04 2014 +0100
@@ -76,9 +76,9 @@
   type text_range = text * Position.range
   val text: text_range option -> text option
   val position: text_range option -> Position.T
+  val reports_of: text_range -> Position.report list
+  val report: text_range -> unit
   val parse: text_range parser
-  val parse_report: text_range parser
-  val parse_context_report: text_range context_parser
 end;
 
 structure Method: METHOD =
@@ -298,19 +298,6 @@
   Repeat1 of combinator_info * text |
   Select_Goals of combinator_info * int * text;
 
-fun keyword_positions (Source _) = []
-  | keyword_positions (Basic _) = []
-  | keyword_positions (Then (Combinator_Info {keywords}, texts)) =
-      keywords @ maps keyword_positions texts
-  | keyword_positions (Orelse (Combinator_Info {keywords}, texts)) =
-      keywords @ maps keyword_positions texts
-  | keyword_positions (Try (Combinator_Info {keywords}, text)) =
-      keywords @ keyword_positions text
-  | keyword_positions (Repeat1 (Combinator_Info {keywords}, text)) =
-      keywords @ keyword_positions text
-  | keyword_positions (Select_Goals (Combinator_Info {keywords}, _, text)) =
-      keywords @ keyword_positions text;
-
 fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
 val succeed_text = Basic (K succeed);
 val default_text = Source (Args.src (("default", []), Position.none));
@@ -421,9 +408,6 @@
 
 type text_range = text * Position.range;
 
-fun reports (text, (pos, _)) =
-  (pos, Markup.language_method) :: map (rpair Markup.keyword3) (keyword_positions text);
-
 fun text NONE = NONE
   | text (SOME (txt, _)) = SOME txt;
 
@@ -431,6 +415,34 @@
   | position (SOME (_, (pos, _))) = pos;
 
 
+(* reports *)
+
+local
+
+fun keyword_positions (Source _) = []
+  | keyword_positions (Basic _) = []
+  | keyword_positions (Then (Combinator_Info {keywords}, texts)) =
+      keywords @ maps keyword_positions texts
+  | keyword_positions (Orelse (Combinator_Info {keywords}, texts)) =
+      keywords @ maps keyword_positions texts
+  | keyword_positions (Try (Combinator_Info {keywords}, text)) =
+      keywords @ keyword_positions text
+  | keyword_positions (Repeat1 (Combinator_Info {keywords}, text)) =
+      keywords @ keyword_positions text
+  | keyword_positions (Select_Goals (Combinator_Info {keywords}, _, text)) =
+      keywords @ keyword_positions text;
+
+in
+
+fun reports_of ((text, (pos, _)): text_range) =
+  (pos, Markup.language_method) ::
+    map (rpair Markup.keyword3) (keyword_positions text);
+
+val report = Position.reports o reports_of;
+
+end;
+
+
 (* outer parser *)
 
 fun is_symid_meth s =
@@ -468,12 +480,6 @@
 val parse =
   Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
 
-(*parse with observable effect!*)
-val parse_report = parse >> (tap (Position.reports o reports));
-val parse_context_report =
-  Args.context -- Scan.lift parse >>
-    (fn (ctxt, text_range) => (Context_Position.reports ctxt (reports text_range); text_range));
-
 end;
 
 

--- a/src/Pure/ML/ml_thms.ML	Thu Feb 27 21:36:40 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Fri Feb 28 10:40:04 2014 +0100
@@ -91,13 +91,15 @@
   (ML_Context.add_antiq @{binding lemma}
     (Scan.depend (fn context =>
       Args.mode "open" -- Parse.enum1_positions "and" (Scan.repeat1 goal) --
-      (Parse.position by --
-        Scan.pass context (Method.parse_context_report -- Scan.option Method.parse_context_report))
-     >> (fn ((is_open, (raw_propss, and_positions)), ((_, by_pos), methods)) =>
+      Parse.position by -- Method.parse -- Scan.option Method.parse
+     >> (fn ((((is_open, (raw_propss, and_positions)), (_, by_pos)), m1), m2) =>
           let
             val ctxt = Context.proof_of context;
 
-            val reports = (by_pos, Markup.keyword1) :: map (rpair Markup.keyword2) and_positions;
+            val reports =
+              (by_pos, Markup.keyword1) ::
+                map (rpair Markup.keyword2) and_positions @
+                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;
@@ -108,7 +110,7 @@
 
             val ctxt' = ctxt
               |> Proof.theorem NONE after_qed propss
-              |> Proof.global_terminal_proof methods;
+              |> Proof.global_terminal_proof (m1, m2);
             val thms =
               Proof_Context.get_fact ctxt'
                 (Facts.named (Proof_Context.full_name ctxt' (Binding.name Auto_Bind.thisN)));

--- a/src/Pure/Thy/thy_output.ML	Thu Feb 27 21:36:40 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Feb 28 10:40:04 2014 +0100
@@ -616,17 +616,19 @@
 val _ = Theory.setup
   (antiquotation (Binding.name "lemma")
     (Args.prop --
-      Scan.lift (Parse.position (Args.$$$ "by")) --
-      (Method.parse_context_report -- Scan.option Method.parse_context_report))
-    (fn {source, context = ctxt, ...} => fn ((prop, (_, by_pos)), methods) =>
+      Scan.lift (Parse.position (Args.$$$ "by") -- Method.parse -- Scan.option Method.parse))
+    (fn {source, context = ctxt, ...} => fn (prop, (((_, by_pos), m1), m2)) =>
       let
         val prop_src =
           (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));
-        val _ = Context_Position.report ctxt by_pos Markup.keyword1;
+
+        val reports = (by_pos, Markup.keyword1) :: 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 methods;
+          |> Proof.global_terminal_proof (m1, m2);
       in output ctxt (maybe_pretty_source pretty_term ctxt prop_src [prop]) end));