# HG changeset patch
# User wenzelm
# Date 1394479628 -3600
# Node ID 513c2b0ea565b49a21deaf4a6bbfde98de389886
# Parent  b034b9f0fa2a956804f67ac5070fdc777b5c6e8d
more markup;

diff -r b034b9f0fa2a -r 513c2b0ea565 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Mon Mar 10 18:06:23 2014 +0100
+++ b/src/Pure/Isar/args.ML	Mon Mar 10 20:27:08 2014 +0100
@@ -11,6 +11,7 @@
   val src: xstring * Position.T -> Token.T list -> src
   val name_of_src: src -> string * Position.T
   val args_of_src: src -> Token.T list
+  val range_of_src: src -> Position.T
   val unparse_src: src -> string list
   val pretty_src: Proof.context -> src -> Pretty.T
   val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
@@ -90,6 +91,10 @@
 fun name_of_src (Src {name, ...}) = name;
 fun args_of_src (Src {args, ...}) = args;
 
+fun range_of_src (Src {name = (_, pos), args, ...}) =
+  if null args then pos
+  else Position.set_range (pos, #2 (Token.range_of args));
+
 fun unparse_src (Src {args, ...}) = map Token.unparse args;
 
 fun pretty_name (Src {name = (name, _), output_info, ...}) =
@@ -113,7 +118,7 @@
 
 (* check *)
 
-fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
+fun check_src ctxt table (Src {name = (xname, pos), args, output_info}) =
   let
     val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
     val space = Name_Space.space_of_table table;
diff -r b034b9f0fa2a -r 513c2b0ea565 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Mar 10 18:06:23 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 20:27:08 2014 +0100
@@ -119,7 +119,9 @@
 fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
 val check_name = check_name_generic o Context.Proof;
 
-fun check_src ctxt src = #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src);
+fun check_src ctxt src =
+ (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
+  #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src));
 
 
 (* pretty printing *)
diff -r b034b9f0fa2a -r 513c2b0ea565 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Mar 10 18:06:23 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Mon Mar 10 20:27:08 2014 +0100
@@ -27,6 +27,7 @@
   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
   val language_method: T
+  val language_attribute: T
   val language_sort: bool -> T
   val language_type: bool -> T
   val language_term: bool -> T
@@ -277,6 +278,8 @@
 
 val language_method =
   language {name = "method", symbols = true, antiquotes = false, delimited = false};
+val language_attribute =
+  language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
 val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
 val language_type = language' {name = "type", symbols = true, antiquotes = false};
 val language_term = language' {name = "term", symbols = true, antiquotes = false};