markup for method combinators;
authorwenzelm
Wed Feb 26 11:58:35 2014 +0100 (2014-02-26 ago)
changeset 55765ec7ca5388dea
parent 55764 484cd3a304a8
child 55766 6a16443e520e
markup for method combinators;
src/HOL/Tools/try0.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/HOL/Tools/try0.ML	Wed Feb 26 11:14:38 2014 +0100
     1.2 +++ b/src/HOL/Tools/try0.ML	Wed Feb 26 11:58:35 2014 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4    #> Method.check_source ctxt
     1.5    #> Method.the_method ctxt
     1.6    #> Method.Basic
     1.7 -  #> curry Method.Select_Goals 1
     1.8 +  #> (fn m => Method.Select_Goals (Method.no_combinator_info, 1, m))
     1.9    #> Proof.refine;
    1.10  
    1.11  fun add_attr_text (NONE, _) s = s
     2.1 --- a/src/Pure/Isar/method.ML	Wed Feb 26 11:14:38 2014 +0100
     2.2 +++ b/src/Pure/Isar/method.ML	Wed Feb 26 11:58:35 2014 +0100
     2.3 @@ -45,14 +45,16 @@
     2.4    val tactic: string * Position.T -> Proof.context -> method
     2.5    val raw_tactic: string * Position.T -> Proof.context -> method
     2.6    type src = Args.src
     2.7 +  type combinator_info
     2.8 +  val no_combinator_info: combinator_info
     2.9    datatype text =
    2.10      Source of src |
    2.11      Basic of Proof.context -> method |
    2.12 -    Then of text list |
    2.13 -    Orelse of text list |
    2.14 -    Try of text |
    2.15 -    Repeat1 of text |
    2.16 -    Select_Goals of int * text
    2.17 +    Then of combinator_info * text list |
    2.18 +    Orelse of combinator_info * text list |
    2.19 +    Try of combinator_info * text |
    2.20 +    Repeat1 of combinator_info * text |
    2.21 +    Select_Goals of combinator_info * int * text
    2.22    val primitive_text: (Proof.context -> thm -> thm) -> text
    2.23    val succeed_text: text
    2.24    val default_text: text
    2.25 @@ -283,14 +285,31 @@
    2.26  
    2.27  type src = Args.src;
    2.28  
    2.29 +datatype combinator_info = Combinator_Info of {keywords: Position.T list};
    2.30 +fun combinator_info keywords = Combinator_Info {keywords = keywords};
    2.31 +val no_combinator_info = combinator_info [];
    2.32 +
    2.33  datatype text =
    2.34    Source of src |
    2.35    Basic of Proof.context -> method |
    2.36 -  Then of text list |
    2.37 -  Orelse of text list |
    2.38 -  Try of text |
    2.39 -  Repeat1 of text |
    2.40 -  Select_Goals of int * text;
    2.41 +  Then of combinator_info * text list |
    2.42 +  Orelse of combinator_info * text list |
    2.43 +  Try of combinator_info * text |
    2.44 +  Repeat1 of combinator_info * text |
    2.45 +  Select_Goals of combinator_info * int * text;
    2.46 +
    2.47 +fun keyword_positions (Source _) = []
    2.48 +  | keyword_positions (Basic _) = []
    2.49 +  | keyword_positions (Then (Combinator_Info {keywords}, texts)) =
    2.50 +      keywords @ maps keyword_positions texts
    2.51 +  | keyword_positions (Orelse (Combinator_Info {keywords}, texts)) =
    2.52 +      keywords @ maps keyword_positions texts
    2.53 +  | keyword_positions (Try (Combinator_Info {keywords}, text)) =
    2.54 +      keywords @ keyword_positions text
    2.55 +  | keyword_positions (Repeat1 (Combinator_Info {keywords}, text)) =
    2.56 +      keywords @ keyword_positions text
    2.57 +  | keyword_positions (Select_Goals (Combinator_Info {keywords}, _, text)) =
    2.58 +      keywords @ keyword_positions text;
    2.59  
    2.60  fun primitive_text r = Basic (SIMPLE_METHOD o PRIMITIVE o r);
    2.61  val succeed_text = Basic (K succeed);
    2.62 @@ -300,7 +319,7 @@
    2.63  fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
    2.64  
    2.65  fun finish_text (NONE, immed) = Basic (finish immed)
    2.66 -  | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];
    2.67 +  | finish_text (SOME txt, immed) = Then (no_combinator_info, [txt, Basic (finish immed)]);
    2.68  
    2.69  
    2.70  (* method definitions *)
    2.71 @@ -402,7 +421,8 @@
    2.72  
    2.73  type text_range = text * Position.range;
    2.74  
    2.75 -fun reports (text, (pos, _)) = [(pos, Markup.language_method)];
    2.76 +fun reports (text, (pos, _)) =
    2.77 +  (pos, Markup.language_method) :: map (rpair Markup.keyword3) (keyword_positions text);
    2.78  
    2.79  fun text NONE = NONE
    2.80    | text (SOME (txt, _)) = SOME txt;
    2.81 @@ -424,16 +444,24 @@
    2.82      Source (Args.src (("cartouche", [tok]), Token.pos_of tok))) ||
    2.83    Parse.$$$ "(" |-- Parse.!!! (meth0 --| Parse.$$$ ")")) x
    2.84  and meth3 x =
    2.85 - (meth4 --| Parse.$$$ "?" >> Try ||
    2.86 -  meth4 --| Parse.$$$ "+" >> Repeat1 ||
    2.87 -  meth4 -- (Parse.$$$ "[" |-- Scan.optional Parse.nat 1 --| Parse.$$$ "]")
    2.88 -    >> (Select_Goals o swap) ||
    2.89 + (meth4 -- Parse.position (Parse.$$$ "?")
    2.90 +    >> (fn (m, (_, pos)) => Try (combinator_info [pos], m)) ||
    2.91 +  meth4 -- Parse.position (Parse.$$$ "+")
    2.92 +    >> (fn (m, (_, pos)) => Repeat1 (combinator_info [pos], m)) ||
    2.93 +  meth4 --
    2.94 +    (Parse.position (Parse.$$$ "[") -- Scan.optional Parse.nat 1 -- Parse.position (Parse.$$$ "]"))
    2.95 +    >> (fn (m, (((_, pos1), n), (_, pos2))) =>
    2.96 +        Select_Goals (combinator_info [pos1, pos2], n, m)) ||
    2.97    meth4) x
    2.98  and meth2 x =
    2.99   (Parse.position (Parse.xname -- Args.parse1 is_symid_meth) >> (Source o Args.src) ||
   2.100    meth3) x
   2.101 -and meth1 x = (Parse.enum1 "," meth2 >> (fn [m] => m | ms => Then ms)) x
   2.102 -and meth0 x = (Parse.enum1 "|" meth1 >> (fn [m] => m | ms => Orelse ms)) x;
   2.103 +and meth1 x =
   2.104 +  (Parse.enum1_positions "," meth2
   2.105 +    >> (fn ([m], _) => m | (ms, ps) => Then (combinator_info ps, ms))) x
   2.106 +and meth0 x =
   2.107 +  (Parse.enum1_positions "|" meth1
   2.108 +    >> (fn ([m], _) => m | (ms, ps) => Orelse (combinator_info ps, ms))) x;
   2.109  
   2.110  in
   2.111  
     3.1 --- a/src/Pure/Isar/proof.ML	Wed Feb 26 11:14:38 2014 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Wed Feb 26 11:58:35 2014 +0100
     3.3 @@ -423,11 +423,11 @@
     3.4      fun eval (Method.Basic m) = apply_method current_context m
     3.5        | eval (Method.Source src) =
     3.6            apply_method current_context (Method.the_method ctxt (Method.check_source ctxt src))
     3.7 -      | eval (Method.Then txts) = Seq.EVERY (map eval txts)
     3.8 -      | eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
     3.9 -      | eval (Method.Try txt) = Seq.TRY (eval txt)
    3.10 -      | eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt)
    3.11 -      | eval (Method.Select_Goals (n, txt)) = select_goals n (eval txt);
    3.12 +      | eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts)
    3.13 +      | eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts)
    3.14 +      | eval (Method.Try (_, txt)) = Seq.TRY (eval txt)
    3.15 +      | eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt)
    3.16 +      | eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt);
    3.17    in eval text state end;
    3.18  
    3.19  in
     4.1 --- a/src/Pure/PIDE/markup.scala	Wed Feb 26 11:14:38 2014 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Wed Feb 26 11:58:35 2014 +0100
     4.3 @@ -210,9 +210,9 @@
     4.4    /* outer syntax */
     4.5  
     4.6    val COMMAND = "command"
     4.7 -
     4.8    val KEYWORD1 = "keyword1"
     4.9    val KEYWORD2 = "keyword2"
    4.10 +  val KEYWORD3 = "keyword3"
    4.11    val OPERATOR = "operator"
    4.12    val STRING = "string"
    4.13    val ALTSTRING = "altstring"
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Feb 26 11:14:38 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Feb 26 11:58:35 2014 +0100
     5.3 @@ -682,6 +682,7 @@
     5.4    private lazy val text_colors: Map[String, Color] = Map(
     5.5        Markup.KEYWORD1 -> keyword1_color,
     5.6        Markup.KEYWORD2 -> keyword2_color,
     5.7 +      Markup.KEYWORD3 -> keyword3_color,
     5.8        Markup.STRING -> Color.BLACK,
     5.9        Markup.ALTSTRING -> Color.BLACK,
    5.10        Markup.VERBATIM -> Color.BLACK,