modifier markup for all parsed tokens;
authorwenzelm
Fri May 01 13:58:06 2015 +0200 (2015-05-01)
changeset 60211c0f686b39ebb
parent 60210 3bcd15f14dcb
child 60212 4e8d8baa491c
modifier markup for all parsed tokens;
report literal token markup, before re-assignment;
src/Pure/Isar/method.ML
src/Pure/Isar/token.ML
     1.1 --- a/src/Pure/Isar/method.ML	Fri May 01 00:27:04 2015 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri May 01 13:58:06 2015 +0200
     1.3 @@ -511,11 +511,11 @@
     1.4  local
     1.5  
     1.6  fun sect (modifier : modifier parser) = Scan.depend (fn context =>
     1.7 -  Scan.ahead Parse.not_eof -- modifier -- Scan.repeat (Scan.unless modifier Parse.xthm) >>
     1.8 -    (fn ((tok, {init, attribute, pos}), xthms) =>
     1.9 +  Scan.ahead Parse.not_eof -- Scan.trace modifier -- Scan.repeat (Scan.unless modifier Parse.xthm)
    1.10 +    >> (fn ((tok0, ({init, attribute, pos}, modifier_toks)), xthms) =>
    1.11        let
    1.12          val decl =
    1.13 -          (case Token.get_value tok of
    1.14 +          (case Token.get_value tok0 of
    1.15              SOME (Token.Declaration decl) => decl
    1.16            | _ =>
    1.17                let
    1.18 @@ -530,14 +530,19 @@
    1.19                  val facts =
    1.20                    Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
    1.21                    |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
    1.22 -                val _ =
    1.23 -                  Context_Position.report ctxt (Token.pos_of tok)
    1.24 -                    (Markup.entity Markup.method_modifierN ""
    1.25 -                      |> Markup.properties (Position.def_properties_of pos));
    1.26 +
    1.27                  fun decl phi =
    1.28                    Context.mapping I init #>
    1.29                    Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
    1.30 -                val _ = Token.assign (SOME (Token.Declaration decl)) tok;
    1.31 +
    1.32 +                val modifier_markup =
    1.33 +                  Markup.properties (Position.def_properties_of pos)
    1.34 +                    (Markup.entity Markup.method_modifierN "");
    1.35 +                val _ =
    1.36 +                  Context_Position.reports ctxt
    1.37 +                    (map (fn tok => (Token.pos_of tok, modifier_markup)) modifier_toks @
    1.38 +                      Token.reports_of_value tok0);
    1.39 +                val _ = Token.assign (SOME (Token.Declaration decl)) tok0;
    1.40                in decl end);
    1.41        in (Morphism.form decl context, decl) end));
    1.42  
     2.1 --- a/src/Pure/Isar/token.ML	Fri May 01 00:27:04 2015 +0200
     2.2 +++ b/src/Pure/Isar/token.ML	Fri May 01 13:58:06 2015 +0200
     2.3 @@ -396,8 +396,18 @@
     2.4  fun map_value f (Token (x, y, Value (SOME v))) = Token (x, y, Value (SOME (f v)))
     2.5    | map_value _ tok = tok;
     2.6  
     2.7 +fun map_values f =
     2.8 +  (map_args o map_value) (fn Source src => Source (map_values f src) | x => f x);
     2.9 +
    2.10 +
    2.11 +(* reports of value *)
    2.12 +
    2.13 +fun get_assignable_value (Token (_, _, Assignable r)) = ! r
    2.14 +  | get_assignable_value (Token (_, _, Value v)) = v
    2.15 +  | get_assignable_value _ = NONE;
    2.16 +
    2.17  fun reports_of_value tok =
    2.18 -  (case get_value tok of
    2.19 +  (case get_assignable_value tok of
    2.20      SOME (Literal markup) =>
    2.21        let
    2.22          val pos = pos_of tok;
    2.23 @@ -409,9 +419,6 @@
    2.24        end
    2.25    | _ => []);
    2.26  
    2.27 -fun map_values f =
    2.28 -  (map_args o map_value) (fn Source src => Source (map_values f src) | x => f x);
    2.29 -
    2.30  
    2.31  (* maxidx *)
    2.32