# HG changeset patch
# User wenzelm
# Date 1430483713 -7200
# Node ID 4e8d8baa491c299a1ab3074a41862ef7a39aa702
# Parent  c0f686b39ebb3343ec195b5811be24e107edd001
clarified markup range;

diff -r c0f686b39ebb -r 4e8d8baa491c src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri May 01 13:58:06 2015 +0200
+++ b/src/Pure/Isar/method.ML	Fri May 01 14:35:13 2015 +0200
@@ -535,13 +535,12 @@
                   Context.mapping I init #>
                   Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd;
 
-                val modifier_markup =
-                  Markup.properties (Position.def_properties_of pos)
-                    (Markup.entity Markup.method_modifierN "");
+                val modifier_report =
+                  (Position.set_range (Token.range_of modifier_toks),
+                    Markup.properties (Position.def_properties_of pos)
+                      (Markup.entity Markup.method_modifierN ""));
                 val _ =
-                  Context_Position.reports ctxt
-                    (map (fn tok => (Token.pos_of tok, modifier_markup)) modifier_toks @
-                      Token.reports_of_value tok0);
+                  Context_Position.reports ctxt (modifier_report :: Token.reports_of_value tok0);
                 val _ = Token.assign (SOME (Token.Declaration decl)) tok0;
               in decl end);
       in (Morphism.form decl context, decl) end));