# HG changeset patch
# User wenzelm
# Date 1393407613 -3600
# Node ID 213b9811f59f41305877ec807fb939cbda744d74
# Parent  e5128a9c431133e56f6e6f18724d7006d21d4fde
method language markup, e.g. relevant to prevent outer keyword completion;

diff -r e5128a9c4311 -r 213b9811f59f src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Feb 25 23:14:51 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Feb 26 10:40:13 2014 +0100
@@ -620,11 +620,11 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "qed"} "conclude proof"
-    (Scan.option Method.parse >> Isar_Cmd.qed);
+    (Scan.option Method.parse_report >> Isar_Cmd.qed);
 
 val _ =
   Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
-    (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
+    (Method.parse_report -- Scan.option Method.parse_report >> Isar_Cmd.terminal_proof);
 
 val _ =
   Outer_Syntax.command @{command_spec ".."} "default proof"
@@ -659,15 +659,15 @@
 
 val _ =
   Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
+    (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
-    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
+    (Method.parse_report >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
 
 val _ =
   Outer_Syntax.command @{command_spec "proof"} "backward proof step"
-    (Scan.option Method.parse >> (fn m => Toplevel.print o
+    (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)));
 
diff -r e5128a9c4311 -r 213b9811f59f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue Feb 25 23:14:51 2014 +0100
+++ b/src/Pure/Isar/method.ML	Wed Feb 26 10:40:13 2014 +0100
@@ -72,9 +72,11 @@
   val section: modifier parser list -> thm list context_parser
   val sections: modifier parser list -> thm list list context_parser
   type text_range = text * Position.range
-  val parse: text_range parser
   val text: text_range option -> text option
   val position: text_range option -> Position.T
+  val parse: text_range parser
+  val parse_report: text_range parser
+  val parse_context_report: text_range context_parser
 end;
 
 structure Method: METHOD =
@@ -396,6 +398,19 @@
   (fn (n, ths) => fn ctxt => meth ctxt n ths);
 
 
+(* text range *)
+
+type text_range = text * Position.range;
+
+fun reports (text, (pos, _)) = [(pos, Markup.language_method)];
+
+fun text NONE = NONE
+  | text (SOME (txt, _)) = SOME txt;
+
+fun position NONE = Position.none
+  | position (SOME (_, (pos, _))) = pos;
+
+
 (* outer parser *)
 
 fun is_symid_meth s =
@@ -425,18 +440,13 @@
 val parse =
   Scan.trace meth3 >> (fn (m, toks) => (m, Token.range_of toks));
 
-end;
-
-
-(* text position *)
+(*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));
 
-type text_range = text * Position.range;
-
-fun text NONE = NONE
-  | text (SOME (txt, _)) = SOME txt;
-
-fun position NONE = Position.none
-  | position (SOME (_, (pos, _))) = pos;
+end;
 
 
 (* theory setup *)
diff -r e5128a9c4311 -r 213b9811f59f src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Tue Feb 25 23:14:51 2014 +0100
+++ b/src/Pure/ML/ml_thms.ML	Wed Feb 26 10:40:13 2014 +0100
@@ -92,8 +92,9 @@
   (ML_Context.add_antiq @{binding lemma}
     (Scan.depend (fn context =>
       Args.mode "open" -- goals1 -- Scan.repeat (Parse.position and_ -- Parse.!!! goals1) --
-      (Parse.position by -- (Method.parse -- Scan.option Method.parse)) >>
-        (fn (((is_open, raw_props), and_propss), ((_, by_pos), methods)) =>
+      (Parse.position by --
+        Scan.pass context (Method.parse_context_report -- Scan.option Method.parse_context_report))
+     >> (fn (((is_open, raw_props), and_propss), ((_, by_pos), methods)) =>
           let
             val ctxt = Context.proof_of context;
 
diff -r e5128a9c4311 -r 213b9811f59f src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Feb 25 23:14:51 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Wed Feb 26 10:40:13 2014 +0100
@@ -23,6 +23,7 @@
   val symbolsN: string
   val languageN: string
   val language: {name: string, symbols: bool, antiquotes: bool} -> T
+  val language_method: T
   val language_sort: T
   val language_type: T
   val language_term: T
@@ -257,6 +258,7 @@
   (languageN,
     [(nameN, name), (symbolsN, print_bool symbols), (antiquotesN, print_bool antiquotes)]);
 
+val language_method = language {name = "method", symbols = true, antiquotes = false};
 val language_sort = language {name = "sort", symbols = true, antiquotes = false};
 val language_type = language {name = "type", symbols = true, antiquotes = false};
 val language_term = language {name = "term", symbols = true, antiquotes = false};
diff -r e5128a9c4311 -r 213b9811f59f src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Feb 25 23:14:51 2014 +0100
+++ b/src/Pure/Thy/thy_output.ML	Wed Feb 26 10:40:13 2014 +0100
@@ -616,8 +616,9 @@
 val _ = Theory.setup
   (antiquotation (Binding.name "lemma")
     (Args.prop --
-      Scan.lift (Parse.position (Args.$$$ "by") -- (Method.parse -- Scan.option Method.parse)))
-    (fn {source, context = ctxt, ...} => fn (prop, ((_, by_pos), methods)) =>
+      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) =>
       let
         val prop_src =
           (case Args.dest_src source of ((a, arg :: _), pos) => Args.src ((a, [arg]), pos));