more position information and PIDE markup for command keywords;
authorwenzelm
Mon Apr 06 16:00:19 2015 +0200 (2015-04-06)
changeset 59934b65c4370f831
parent 59933 07a7544c0535
child 59935 343905de27b1
more position information and PIDE markup for command keywords;
src/Pure/Isar/keyword.ML
src/Pure/ML/ml_antiquotations.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/Thy/thy_header.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Isar/keyword.ML	Mon Apr 06 14:09:31 2015 +0200
     1.2 +++ b/src/Pure/Isar/keyword.ML	Mon Apr 06 16:00:19 2015 +0200
     1.3 @@ -37,10 +37,11 @@
     1.4    val no_command_keywords: keywords -> keywords
     1.5    val empty_keywords: keywords
     1.6    val merge_keywords: keywords * keywords -> keywords
     1.7 -  val add_keywords: (string * spec option) list -> keywords -> keywords
     1.8 +  val add_keywords: ((string * Position.T) * spec option) list -> keywords -> keywords
     1.9    val is_keyword: keywords -> string -> bool
    1.10    val is_command: keywords -> string -> bool
    1.11    val is_literal: keywords -> string -> bool
    1.12 +  val command_markup: keywords -> string -> Markup.T option
    1.13    val command_kind: keywords -> string -> string option
    1.14    val command_files: keywords -> string -> Path.T -> Path.T list
    1.15    val command_tags: keywords -> string -> string list
    1.16 @@ -105,19 +106,21 @@
    1.17  
    1.18  (* specifications *)
    1.19  
    1.20 -type T =
    1.21 - {kind: string,
    1.22 +type spec = (string * string list) * string list;
    1.23 +
    1.24 +type entry =
    1.25 + {pos: Position.T,
    1.26 +  id: serial,
    1.27 +  kind: string,
    1.28    files: string list,  (*extensions of embedded files*)
    1.29    tags: string list};
    1.30  
    1.31 -type spec = (string * string list) * string list;
    1.32 -
    1.33 -fun check_spec ((kind, files), tags) : T =
    1.34 +fun check_spec pos ((kind, files), tags) : entry =
    1.35    if not (member (op =) kinds kind) then
    1.36      error ("Unknown outer syntax keyword kind " ^ quote kind)
    1.37    else if not (null files) andalso kind <> thy_load then
    1.38      error ("Illegal specification of files for " ^ quote kind)
    1.39 -  else {kind = kind, files = files, tags = tags};
    1.40 +  else {pos = pos, id = serial (), kind = kind, files = files, tags = tags};
    1.41  
    1.42  
    1.43  
    1.44 @@ -128,7 +131,7 @@
    1.45  datatype keywords = Keywords of
    1.46   {minor: Scan.lexicon,
    1.47    major: Scan.lexicon,
    1.48 -  commands: T Symtab.table};
    1.49 +  commands: entry Symtab.table};
    1.50  
    1.51  fun minor_keywords (Keywords {minor, ...}) = minor;
    1.52  fun major_keywords (Keywords {major, ...}) = major;
    1.53 @@ -157,7 +160,7 @@
    1.54      Symtab.merge (K true) (commands1, commands2));
    1.55  
    1.56  val add_keywords =
    1.57 -  fold (fn (name, opt_spec) => map_keywords (fn (minor, major, commands) =>
    1.58 +  fold (fn ((name, pos), opt_spec) => map_keywords (fn (minor, major, commands) =>
    1.59      (case opt_spec of
    1.60        NONE =>
    1.61          let
    1.62 @@ -165,9 +168,9 @@
    1.63          in (minor', major, commands) end
    1.64      | SOME spec =>
    1.65          let
    1.66 -          val kind = check_spec spec;
    1.67 +          val entry = check_spec pos spec;
    1.68            val major' = Scan.extend_lexicon (Symbol.explode name) major;
    1.69 -          val commands' = Symtab.update (name, kind) commands;
    1.70 +          val commands' = Symtab.update (name, entry) commands;
    1.71          in (minor, major', commands') end)));
    1.72  
    1.73  
    1.74 @@ -178,10 +181,16 @@
    1.75  fun is_literal keywords = is_keyword keywords orf is_command keywords;
    1.76  
    1.77  
    1.78 -(* command kind *)
    1.79 +(* command keywords *)
    1.80  
    1.81  fun lookup_command (Keywords {commands, ...}) = Symtab.lookup commands;
    1.82  
    1.83 +fun command_markup keywords name =
    1.84 +  lookup_command keywords name
    1.85 +  |> Option.map (fn {pos, id, ...} =>
    1.86 +      Markup.properties (Position.entity_properties_of false id pos)
    1.87 +        (Markup.entity Markup.commandN name));
    1.88 +
    1.89  fun command_kind keywords = Option.map #kind o lookup_command keywords;
    1.90  
    1.91  fun command_files keywords name path =
     2.1 --- a/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 14:09:31 2015 +0200
     2.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Mon Apr 06 16:00:19 2015 +0200
     2.3 @@ -254,10 +254,11 @@
     2.4          "Parse.$$$ " ^ ML_Syntax.print_string name
     2.5        else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
     2.6    ML_Antiquotation.value @{binding command_spec}
     2.7 -    (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
     2.8 -      if Keyword.is_command (Thy_Header.get_keywords thy) name then
     2.9 -        ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos)
    2.10 -      else error ("Bad outer syntax command " ^ quote name ^ Position.here pos))));
    2.11 +    (Args.context -- Scan.lift (Parse.position Parse.name) >> (fn (ctxt, (name, pos)) =>
    2.12 +      (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
    2.13 +        SOME markup =>
    2.14 +         (Context_Position.reports ctxt [(pos, markup), (pos, Markup.keyword1)];
    2.15 +          ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position (name, pos))
    2.16 +      | NONE => error ("Bad outer syntax command " ^ quote name ^ Position.here pos)))));
    2.17  
    2.18  end;
    2.19 -
     3.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 06 14:09:31 2015 +0200
     3.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 06 16:00:19 2015 +0200
     3.3 @@ -125,8 +125,8 @@
     3.4            NONE => I
     3.5          | SOME id => Protocol_Message.command_positions_yxml id)
     3.6          |> error;
     3.7 -    val {name = (name, _), imports, keywords} = header;
     3.8 -    val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
     3.9 +    val {name = (name, _), imports, ...} = header;
    3.10 +    val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
    3.11    in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
    3.12  
    3.13  fun get_perspective (Node {perspective, ...}) = perspective;
     4.1 --- a/src/Pure/PIDE/protocol.ML	Mon Apr 06 14:09:31 2015 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.ML	Mon Apr 06 16:00:19 2015 +0200
     4.3 @@ -81,7 +81,8 @@
     4.4                                (option (pair (pair string (list string)) (list string)))))
     4.5                                (list YXML.string_of_body)))) a;
     4.6                          val imports' = map (rpair Position.none) imports;
     4.7 -                        val header = Thy_Header.make (name, Position.none) imports' keywords;
     4.8 +                        val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords;
     4.9 +                        val header = Thy_Header.make (name, Position.none) imports' keywords';
    4.10                        in Document.Deps {master = master, header = header, errors = errors} end,
    4.11                      fn (a :: b, c) =>
    4.12                        Document.Perspective (bool_atom a, map int_atom b,
     5.1 --- a/src/Pure/Thy/thy_header.ML	Mon Apr 06 14:09:31 2015 +0200
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Apr 06 16:00:19 2015 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  signature THY_HEADER =
     5.6  sig
     5.7 -  type keywords = (string * Keyword.spec option) list
     5.8 +  type keywords = ((string * Position.T) * Keyword.spec option) list
     5.9    type header =
    5.10     {name: string * Position.T,
    5.11      imports: (string * Position.T) list,
    5.12 @@ -29,7 +29,7 @@
    5.13  
    5.14  (* header *)
    5.15  
    5.16 -type keywords = (string * Keyword.spec option) list;
    5.17 +type keywords = ((string * Position.T) * Keyword.spec option) list;
    5.18  
    5.19  type header =
    5.20   {name: string * Position.T,
    5.21 @@ -59,26 +59,26 @@
    5.22  val bootstrap_keywords =
    5.23    Keyword.empty_keywords
    5.24    |> Keyword.add_keywords
    5.25 -    [("%", NONE),
    5.26 -     ("(", NONE),
    5.27 -     (")", NONE),
    5.28 -     (",", NONE),
    5.29 -     ("::", NONE),
    5.30 -     ("==", NONE),
    5.31 -     ("and", NONE),
    5.32 -     (beginN, NONE),
    5.33 -     (importsN, NONE),
    5.34 -     (keywordsN, NONE),
    5.35 -     (headerN, SOME ((Keyword.document_heading, []), [])),
    5.36 -     (chapterN, SOME ((Keyword.document_heading, []), [])),
    5.37 -     (sectionN, SOME ((Keyword.document_heading, []), [])),
    5.38 -     (subsectionN, SOME ((Keyword.document_heading, []), [])),
    5.39 -     (subsubsectionN, SOME ((Keyword.document_heading, []), [])),
    5.40 -     (textN, SOME ((Keyword.document_body, []), [])),
    5.41 -     (txtN, SOME ((Keyword.document_body, []), [])),
    5.42 -     (text_rawN, SOME ((Keyword.document_raw, []), [])),
    5.43 -     (theoryN, SOME ((Keyword.thy_begin, []), ["theory"])),
    5.44 -     ("ML_file", SOME ((Keyword.thy_load, []), ["ML"]))];
    5.45 +    [(("%", @{here}), NONE),
    5.46 +     (("(", @{here}), NONE),
    5.47 +     ((")", @{here}), NONE),
    5.48 +     ((",", @{here}), NONE),
    5.49 +     (("::", @{here}), NONE),
    5.50 +     (("==", @{here}), NONE),
    5.51 +     (("and", @{here}), NONE),
    5.52 +     ((beginN, @{here}), NONE),
    5.53 +     ((importsN, @{here}), NONE),
    5.54 +     ((keywordsN, @{here}), NONE),
    5.55 +     ((headerN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.56 +     ((chapterN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.57 +     ((sectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.58 +     ((subsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.59 +     ((subsubsectionN, @{here}), SOME ((Keyword.document_heading, []), [])),
    5.60 +     ((textN, @{here}), SOME ((Keyword.document_body, []), [])),
    5.61 +     ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
    5.62 +     ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
    5.63 +     ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
    5.64 +     (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
    5.65  
    5.66  
    5.67  (* theory data *)
    5.68 @@ -119,7 +119,7 @@
    5.69    Parse.group (fn () => "outer syntax keyword completion") Parse.name;
    5.70  
    5.71  val keyword_decl =
    5.72 -  Scan.repeat1 Parse.string --
    5.73 +  Scan.repeat1 (Parse.position Parse.string) --
    5.74    Scan.option (Parse.$$$ "::" |-- Parse.!!! keyword_spec) --
    5.75    Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
    5.76    >> (fn ((names, spec), _) => map (rpair spec) names);
     6.1 --- a/src/Pure/Tools/find_consts.ML	Mon Apr 06 14:09:31 2015 +0200
     6.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Apr 06 16:00:19 2015 +0200
     6.3 @@ -140,7 +140,7 @@
     6.4  
     6.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
     6.6  
     6.7 -val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
     6.8 +val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
     6.9  
    6.10  in
    6.11  
     7.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Apr 06 14:09:31 2015 +0200
     7.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Apr 06 16:00:19 2015 +0200
     7.3 @@ -524,7 +524,7 @@
     7.4  
     7.5  val query = Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion);
     7.6  
     7.7 -val query_keywords = Keyword.add_keywords [(":", NONE)] Keyword.empty_keywords;
     7.8 +val query_keywords = Keyword.add_keywords [((":", @{here}), NONE)] Keyword.empty_keywords;
     7.9  
    7.10  in
    7.11