# HG changeset patch
# User wenzelm
# Date 1393412315 -3600
# Node ID ec7ca5388dead9ebbbab9dae66e76203978c2fe2
# Parent  484cd3a304a84d2259392fffdc2039399759210f
markup for method combinators;

diff -r 484cd3a304a8 -r ec7ca5388dea src/HOL/Tools/try0.ML
--- a/src/HOL/Tools/try0.ML	Wed Feb 26 11:14:38 2014 +0100
+++ b/src/HOL/Tools/try0.ML	Wed Feb 26 11:58:35 2014 +0100
@@ -60,7 +60,7 @@
   #> Method.check_source ctxt
   #> Method.the_method ctxt
   #> Method.Basic
-  #> curry Method.Select_Goals 1
+  #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m))
   #> Proof.refine;
 
 fun add_attr_text (NONE, _) s = s
diff -r 484cd3a304a8 -r ec7ca5388dea src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Feb 26 11:14:38 2014 +0100
+++ b/src/Pure/Isar/method.ML	Wed Feb 26 11:58:35 2014 +0100
@@ -45,14 +45,16 @@
   val tactic: string * Position.T -> Proof.context -> method
   val raw_tactic: string * Position.T -> Proof.context -> method
   type src = Args.src
+  type combinator_info
+  val no_combinator_info: combinator_info
   datatype text =
     Source of src |
     Basic of Proof.context -> method |
-    Then of text list |
-    Orelse of text list |
-    Try of text |
-    Repeat1 of text |
-    Select_Goals of int * text
+    Then of combinator_info * text list |
+    Orelse of combinator_info * text list |
+    Try of combinator_info * text |
+    Repeat1 of combinator_info * text |
+    Select_Goals of combinator_info * int * text
   val primitive_text: (Proof.context -> thm -> thm) -> text
   val succeed_text: text
   val default_text: text
@@ -283,14 +285,31 @@
 
 type src = Args.src;
 
+datatype combinator_info = Combinator_Info of {keywords: Position.T list};
+fun combinator_info keywords = Combinator_Info {keywords = keywords};
+val no_combinator_info = combinator_info [];
+
 datatype text =
   Source of src |
   Basic of Proof.context -> method |
-  Then of text list |
-  Orelse of text list |
-  Try of text |
-  Repeat1 of text |
-  Select_Goals of int * text;
+  Then of combinator_info * text list |
+  Orelse of combinator_info * text list |
+  Try of combinator_info * text |
+  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);
@@ -300,7 +319,7 @@
 fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
 
 fun finish_text (NONE, immed) = Basic (finish immed)
-  | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];
+  | finish_text (SOME txt, immed) = Then (no_combinator_info, [txt, Basic (finish immed)]);
 
 
 (* method definitions *)
@@ -402,7 +421,8 @@
 
 type text_range = text * Position.range;
 
-fun reports (text, (pos, _)) = [(pos, Markup.language_method)];
+fun reports (text, (pos, _)) =
+  (pos, Markup.language_method) :: map (rpair Markup.keyword3) (keyword_positions text);
 
 fun text NONE = NONE
   | text (SOME (txt, _)) = SOME txt;
@@ -424,16 +444,24 @@
     Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
   Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
 and meth3 x =
- (meth4 --| Parse.$$$ "?" >> Try ||
-  meth4 --| Parse.$$$ "+" >> Repeat1 ||
-  meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]")
-    >> (Select_Goals o swap) ||
+ (meth4 -- Parse.position (Parse.$$$ "?")
+    >> (fn (m, (_, pos)) => Try (combinator_info [pos], m)) ||
+  meth4 -- Parse.position (Parse.$$$ "+")
+    >> (fn (m, (_, pos)) => Repeat1 (combinator_info [pos], m)) ||
+  meth4 --
+    (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
+    >> (fn (m, (((_, pos1), n), (_, pos2))) =>
+        Select_Goals (combinator_info [pos1, pos2], n, m)) ||
   meth4) x
 and meth2 x =
  (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
   meth3) x
-and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
-and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
+and meth1 x =
+  (Parse.enum1_positions "," meth2
+    >> (fn ([m], _) => m | (ms, ps) => Then (combinator_info ps, ms))) x
+and meth0 x =
+  (Parse.enum1_positions "|" meth1
+    >> (fn ([m], _) => m | (ms, ps) => Orelse (combinator_info ps, ms))) x;
 
 in
 
diff -r 484cd3a304a8 -r ec7ca5388dea src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Feb 26 11:14:38 2014 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Feb 26 11:58:35 2014 +0100
@@ -423,11 +423,11 @@
     fun eval (Method.Basic m) = apply_method current_context m
       | eval (Method.Source src) =
           apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src))
-      | eval (Method.Then txts) = Seq.EVERY (map eval txts)
-      | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
-      | eval (Method.Try txt) = Seq.TRY (eval txt)
-      | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt)
-      | eval (Method.Select_Goals (n, txt)) = select_goals n (eval txt);
+      | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts)
+      | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts)
+      | eval (Method.Try (_, txt)) = Seq.TRY (eval txt)
+      | eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt)
+      | eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt);
   in eval text state end;
 
 in
diff -r 484cd3a304a8 -r ec7ca5388dea src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Feb 26 11:14:38 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Feb 26 11:58:35 2014 +0100
@@ -210,9 +210,9 @@
   /* outer syntax */
 
   val COMMAND = "command"
-
   val KEYWORD1 = "keyword1"
   val KEYWORD2 = "keyword2"
+  val KEYWORD3 = "keyword3"
   val OPERATOR = "operator"
   val STRING = "string"
   val ALTSTRING = "altstring"
diff -r 484cd3a304a8 -r ec7ca5388dea src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Feb 26 11:14:38 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Feb 26 11:58:35 2014 +0100
@@ -682,6 +682,7 @@
   private lazy val text_colors: Map[String, Color] = Map(
       Markup.KEYWORD1 -> keyword1_color,
       Markup.KEYWORD2 -> keyword2_color,
+      Markup.KEYWORD3 -> keyword3_color,
       Markup.STRING -> Color.BLACK,
       Markup.ALTSTRING -> Color.BLACK,
       Markup.VERBATIM -> Color.BLACK,