--- a/src/Pure/Isar/keyword.ML Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Isar/keyword.ML Mon Apr 06 16:00:19 2015 +0200
@@ -37,10 +37,11 @@
val no_command_keywords: keywords -> keywords
val empty_keywords: keywords
val merge_keywords: keywords * keywords -> keywords
- val add_keywords: (string * spec option) list -> keywords -> keywords
+ val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
val is_keyword: keywords -> string -> bool
val is_command: keywords -> string -> bool
val is_literal: keywords -> string -> bool
+ val command_markup: keywords -> string -> Markup.T option
val command_kind: keywords -> string -> string option
val command_files: keywords -> string -> Path.T -> Path.T list
val command_tags: keywords -> string -> string list
@@ -105,19 +106,21 @@
(* specifications *)
-type T =
- {kind: string,
+type spec = (string * string list) * string list;
+
+type entry =
+ {pos: Position.T,
+ id: serial,
+ kind: string,
files: string list, (*extensions of embedded files*)
tags: string list};
-type spec = (string * string list) * string list;
-
-fun check_spec ((kind, files), tags) : T =
+fun check_spec pos ((kind, files), tags) : entry =
if not (member (op =) kinds kind) then
error ("Unknown outer syntax keyword kind " ^ quote kind)
else if not (null files) andalso kind <> thy_load then
error ("Illegal specification of files for " ^ quote kind)
- else {kind = kind, files = files, tags = tags};
+ else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
@@ -128,7 +131,7 @@
datatype keywords = Keywords of
{minor: Scan.lexicon,
major: Scan.lexicon,
- commands: T Symtab.table};
+ commands: entry Symtab.table};
fun minor_keywords (Keywords {minor, ...}) = minor;
fun major_keywords (Keywords {major, ...}) = major;
@@ -157,7 +160,7 @@
Symtab.merge (K true) (commands1, commands2));
val add_keywords =
- fold (fn (name, opt_spec) => map_keywords (fn (minor, major, commands) =>
+ fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
(case opt_spec of
NONE =>
let
@@ -165,9 +168,9 @@
in (minor', major, commands) end
| SOME spec =>
let
- val kind = check_spec spec;
+ val entry = check_spec pos spec;
val major' = Scan.extend_lexicon (Symbol.explode name) major;
- val commands' = Symtab.update (name, kind) commands;
+ val commands' = Symtab.update (name, entry) commands;
in (minor, major', commands') end)));
@@ -178,10 +181,16 @@
fun is_literal keywords = is_keyword keywords orf is_command keywords;
-(* command kind *)
+(* command keywords *)
fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
+fun command_markup keywords name =
+ lookup_command keywords name
+ |> Option.map (fn {pos, id, ...} =>
+ Markup.properties (Position.entity_properties_of false id pos)
+ (Markup.entity Markup.commandN name));
+
fun command_kind keywords = Option.map #kind o lookup_command keywords;
fun command_files keywords name path =
--- a/src/Pure/ML/ml_antiquotations.ML Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Apr 06 16:00:19 2015 +0200
@@ -254,10 +254,11 @@
"Parse.$$$ " ^ ML_Syntax.print_string name
else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
ML_Antiquotation.value @{binding command_spec}
- (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
- if Keyword.is_command (Thy_Header.get_keywords thy) name then
- ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)
- else error ("Bad outer syntax command " ^ quote name ^ Position.here pos))));
+ (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
+ (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
+ SOME markup =>
+ (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
+ ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
+ | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));
end;
-
--- a/src/Pure/PIDE/document.ML Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/PIDE/document.ML Mon Apr 06 16:00:19 2015 +0200
@@ -125,8 +125,8 @@
NONE => I
| SOME id => Protocol_Message.command_positions_yxml id)
|> error;
- val {name = (name, _), imports, keywords} = header;
- val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
+ val {name = (name, _), imports, ...} = header;
+ val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
fun get_perspective (Node {perspective, ...}) = perspective;
--- a/src/Pure/PIDE/protocol.ML Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/PIDE/protocol.ML Mon Apr 06 16:00:19 2015 +0200
@@ -81,7 +81,8 @@
(option (pair (pair string (list string)) (list string)))))
(list YXML.string_of_body)))) a;
val imports' = map (rpair Position.none) imports;
- val header = Thy_Header.make (name, Position.none) imports' keywords;
+ val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
+ val header = Thy_Header.make (name, Position.none) imports' keywords';
in Document.Deps {master = master, header = header, errors = errors} end,
fn (a :: b, c) =>
Document.Perspective (bool_atom a, map int_atom b,
--- a/src/Pure/Thy/thy_header.ML Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Apr 06 16:00:19 2015 +0200
@@ -6,7 +6,7 @@
signature THY_HEADER =
sig
- type keywords = (string * Keyword.spec option) list
+ type keywords = ((string * Position.T) * Keyword.spec option) list
type header =
{name: string * Position.T,
imports: (string * Position.T) list,
@@ -29,7 +29,7 @@
(* header *)
-type keywords = (string * Keyword.spec option) list;
+type keywords = ((string * Position.T) * Keyword.spec option) list;
type header =
{name: string * Position.T,
@@ -59,26 +59,26 @@
val bootstrap_keywords =
Keyword.empty_keywords
|> Keyword.add_keywords
- [("%", NONE),
- ("(", NONE),
- (")", NONE),
- (",", NONE),
- ("::", NONE),
- ("==", NONE),
- ("and", NONE),
- (beginN, NONE),
- (importsN, NONE),
- (keywordsN, NONE),
- (headerN, SOME ((Keyword.document_heading, []), [])),
- (chapterN, SOME ((Keyword.document_heading, []), [])),
- (sectionN, SOME ((Keyword.document_heading, []), [])),
- (subsectionN, SOME ((Keyword.document_heading, []), [])),
- (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
- (textN, SOME ((Keyword.document_body, []), [])),
- (txtN, SOME ((Keyword.document_body, []), [])),
- (text_rawN, SOME ((Keyword.document_raw, []), [])),
- (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
- ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
+ [(("%", @{here}), NONE),
+ (("(", @{here}), NONE),
+ ((")", @{here}), NONE),
+ ((",", @{here}), NONE),
+ (("::", @{here}), NONE),
+ (("==", @{here}), NONE),
+ (("and", @{here}), NONE),
+ ((beginN, @{here}), NONE),
+ ((importsN, @{here}), NONE),
+ ((keywordsN, @{here}), NONE),
+ ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
+ ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
+ ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
+ ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
+ ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
+ (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
(* theory data *)
@@ -119,7 +119,7 @@
Parse.group (fn () => "outer syntax keyword completion") Parse.name;
val keyword_decl =
- Scan.repeat1 Parse.string --
+ Scan.repeat1 (Parse.position Parse.string) --
Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
>> (fn ((names, spec), _) => map (rpair spec) names);
--- a/src/Pure/Tools/find_consts.ML Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Tools/find_consts.ML Mon Apr 06 16:00:19 2015 +0200
@@ -140,7 +140,7 @@
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
-val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
in
--- a/src/Pure/Tools/find_theorems.ML Mon Apr 06 14:09:31 2015 +0200
+++ b/src/Pure/Tools/find_theorems.ML Mon Apr 06 16:00:19 2015 +0200
@@ -524,7 +524,7 @@
val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
-val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
+val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
in