more markup;
authorwenzelm
Mon Mar 10 20:27:08 2014 +0100 (2014-03-10)
changeset 56033513c2b0ea565
parent 56032 b034b9f0fa2a
child 56034 1c59b555ac4a
more markup;
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/PIDE/markup.ML
     1.1 --- a/src/Pure/Isar/args.ML	Mon Mar 10 18:06:23 2014 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Mon Mar 10 20:27:08 2014 +0100
     1.3 @@ -11,6 +11,7 @@
     1.4    val src: xstring * Position.T -> Token.T list -> src
     1.5    val name_of_src: src -> string * Position.T
     1.6    val args_of_src: src -> Token.T list
     1.7 +  val range_of_src: src -> Position.T
     1.8    val unparse_src: src -> string list
     1.9    val pretty_src: Proof.context -> src -> Pretty.T
    1.10    val check_src: Proof.context -> 'a Name_Space.table -> src -> src * 'a
    1.11 @@ -90,6 +91,10 @@
    1.12  fun name_of_src (Src {name, ...}) = name;
    1.13  fun args_of_src (Src {args, ...}) = args;
    1.14  
    1.15 +fun range_of_src (Src {name = (_, pos), args, ...}) =
    1.16 +  if null args then pos
    1.17 +  else Position.set_range (pos, #2 (Token.range_of args));
    1.18 +
    1.19  fun unparse_src (Src {args, ...}) = map Token.unparse args;
    1.20  
    1.21  fun pretty_name (Src {name = (name, _), output_info, ...}) =
    1.22 @@ -113,7 +118,7 @@
    1.23  
    1.24  (* check *)
    1.25  
    1.26 -fun check_src ctxt table (Src {name = (xname, pos), args, output_info = _}) =
    1.27 +fun check_src ctxt table (Src {name = (xname, pos), args, output_info}) =
    1.28    let
    1.29      val (name, x) = Name_Space.check (Context.Proof ctxt) table (xname, pos);
    1.30      val space = Name_Space.space_of_table table;
     2.1 --- a/src/Pure/Isar/attrib.ML	Mon Mar 10 18:06:23 2014 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Mon Mar 10 20:27:08 2014 +0100
     2.3 @@ -119,7 +119,9 @@
     2.4  fun check_name_generic context = #1 o Name_Space.check context (get_attributes context);
     2.5  val check_name = check_name_generic o Context.Proof;
     2.6  
     2.7 -fun check_src ctxt src = #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src);
     2.8 +fun check_src ctxt src =
     2.9 + (Context_Position.report ctxt (Args.range_of_src src) Markup.language_attribute;
    2.10 +  #1 (Args.check_src ctxt (get_attributes (Context.Proof ctxt)) src));
    2.11  
    2.12  
    2.13  (* pretty printing *)
     3.1 --- a/src/Pure/PIDE/markup.ML	Mon Mar 10 18:06:23 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Mon Mar 10 20:27:08 2014 +0100
     3.3 @@ -27,6 +27,7 @@
     3.4    val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
     3.5    val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
     3.6    val language_method: T
     3.7 +  val language_attribute: T
     3.8    val language_sort: bool -> T
     3.9    val language_type: bool -> T
    3.10    val language_term: bool -> T
    3.11 @@ -277,6 +278,8 @@
    3.12  
    3.13  val language_method =
    3.14    language {name = "method", symbols = true, antiquotes = false, delimited = false};
    3.15 +val language_attribute =
    3.16 +  language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
    3.17  val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
    3.18  val language_type = language' {name = "type", symbols = true, antiquotes = false};
    3.19  val language_term = language' {name = "term", symbols = true, antiquotes = false};