--- 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
--- 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
--- 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
--- 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"
--- 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,