clarified markup range;
authorwenzelm
Fri May 01 14:35:13 2015 +0200 (2015-05-01)
changeset 602124e8d8baa491c
parent 60211 c0f686b39ebb
child 60213 392e5aae3348
clarified markup range;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Fri May 01 13:58:06 2015 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Fri May 01 14:35:13 2015 +0200
     1.3 @@ -535,13 +535,12 @@
     1.4                    Context.mapping I init #>
     1.5                    Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
     1.6  
     1.7 -                val modifier_markup =
     1.8 -                  Markup.properties (Position.def_properties_of pos)
     1.9 -                    (Markup.entity Markup.method_modifierN "");
    1.10 +                val modifier_report =
    1.11 +                  (Position.set_range (Token.range_of modifier_toks),
    1.12 +                    Markup.properties (Position.def_properties_of pos)
    1.13 +                      (Markup.entity Markup.method_modifierN ""));
    1.14                  val _ =
    1.15 -                  Context_Position.reports ctxt
    1.16 -                    (map (fn tok => (Token.pos_of tok, modifier_markup)) modifier_toks @
    1.17 -                      Token.reports_of_value tok0);
    1.18 +                  Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0);
    1.19                  val _ = Token.assign (SOME (Token.Declaration decl)) tok0;
    1.20                in decl end);
    1.21        in (Morphism.form decl context, decl) end));