--- 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;
--- 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 *)
--- 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};