# HG changeset patch # User wenzelm # Date 1428328819 -7200 # Node ID b65c4370f8314e4d7b3afa01ac59fcabebaac6bb # Parent 07a7544c05351272a25b333e252626c77209b0d7 more position information and PIDE markup for command keywords; diff -r 07a7544c0535 -r b65c4370f831 src/Pure/Isar/keyword.ML --- 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 = diff -r 07a7544c0535 -r b65c4370f831 src/Pure/ML/ml_antiquotations.ML --- 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; - diff -r 07a7544c0535 -r b65c4370f831 src/Pure/PIDE/document.ML --- 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; diff -r 07a7544c0535 -r b65c4370f831 src/Pure/PIDE/protocol.ML --- 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, diff -r 07a7544c0535 -r b65c4370f831 src/Pure/Thy/thy_header.ML --- 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); diff -r 07a7544c0535 -r b65c4370f831 src/Pure/Tools/find_consts.ML --- 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 diff -r 07a7544c0535 -r b65c4370f831 src/Pure/Tools/find_theorems.ML --- 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