src/Pure/Isar/outer_keyword.ML
changeset 27357 5b3a087ff292
parent 17270 534b6e5e3736
child 27433 b82c12e57e79
equal deleted inserted replaced
27356:cb052da62549 27357:5b3a087ff292
     1 (*  Title:      Pure/Isar/outer_keyword.ML
     1 (*  Title:      Pure/Isar/outer_keyword.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Makarius
     3     Author:     Makarius
     4 
     4 
     5 Isar command keyword classification.
     5 Isar command keyword classification and global keyword tables.
     6 *)
     6 *)
     7 
     7 
     8 signature OUTER_KEYWORD =
     8 signature OUTER_KEYWORD =
     9 sig
     9 sig
    10   type T
    10   type T
    36   val tag: string -> T -> T
    36   val tag: string -> T -> T
    37   val tags_of: T -> string list
    37   val tags_of: T -> string list
    38   val tag_theory: T -> T
    38   val tag_theory: T -> T
    39   val tag_proof: T -> T
    39   val tag_proof: T -> T
    40   val tag_ml: T -> T
    40   val tag_ml: T -> T
       
    41   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
       
    42   val is_keyword: string -> bool
       
    43   val dest_keywords: unit -> string list
       
    44   val dest_commands: unit -> string list
       
    45   val command_keyword: string -> T option
       
    46   val command_tags: string -> string list
       
    47   val report: unit -> unit
       
    48   val keyword: string -> unit
       
    49   val command: string -> T -> unit
    41 end;
    50 end;
    42 
    51 
    43 structure OuterKeyword: OUTER_KEYWORD =
    52 structure OuterKeyword: OUTER_KEYWORD =
    44 struct
    53 struct
    45 
    54 
    46 (* keyword classification *)
    55 (** keyword classification **)
    47 
    56 
    48 datatype T = Keyword of string * string list;
    57 datatype T = Keyword of string * string list;
    49 
    58 
    50 fun kind s = Keyword (s, []);
    59 fun kind s = Keyword (s, []);
    51 fun kind_of (Keyword (s, _)) = s;
    60 fun kind_of (Keyword (s, _)) = s;
    90 
    99 
    91 val tag_theory = tag "theory";
   100 val tag_theory = tag "theory";
    92 val tag_proof = tag "proof";
   101 val tag_proof = tag "proof";
    93 val tag_ml = tag "ML";
   102 val tag_ml = tag "ML";
    94 
   103 
       
   104 
       
   105 
       
   106 (** global keyword tables **)
       
   107 
       
   108 local
       
   109 
       
   110 val global_commands = ref (Symtab.empty: T Symtab.table);
       
   111 val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
       
   112 
       
   113 in
       
   114 
       
   115 fun get_commands () = CRITICAL (fn () => ! global_commands);
       
   116 fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
       
   117 
       
   118 fun change_commands f = CRITICAL (fn () => change global_commands f);
       
   119 
       
   120 fun change_lexicons f = CRITICAL (fn () =>
       
   121   (change global_lexicons f;
       
   122     (case (op inter_string) (pairself Scan.dest_lexicon (get_lexicons ())) of
       
   123       [] => ()
       
   124     | clash => warning ("Overlapping outer syntax commands and keywords: " ^ commas_quote clash))));
       
   125 
    95 end;
   126 end;
       
   127 
       
   128 
       
   129 (* lookup *)
       
   130 
       
   131 fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
       
   132 fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
       
   133 
       
   134 fun dest_commands () = Symtab.keys (get_commands ());
       
   135 fun command_keyword name = Symtab.lookup (get_commands ()) name;
       
   136 fun command_tags name = these (Option.map tags_of (command_keyword name));
       
   137 
       
   138 
       
   139 (* report *)
       
   140 
       
   141 fun report_keyword name =
       
   142   Pretty.mark (Markup.keyword_decl name)
       
   143     (Pretty.str ("Outer syntax keyword: " ^ quote name));
       
   144 
       
   145 fun report_command (name, kind) =
       
   146   Pretty.mark (Markup.command_decl name (kind_of kind))
       
   147     (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
       
   148 
       
   149 fun report () =
       
   150   let val (keywords, commands) = CRITICAL (fn () =>
       
   151     (dest_keywords (), Symtab.dest (get_commands ())))
       
   152   in map report_keyword keywords @ map report_command commands end
       
   153   |> Pretty.chunks |> Pretty.writeln;
       
   154 
       
   155 
       
   156 (* augment tables *)
       
   157 
       
   158 fun keyword name =
       
   159  (change_lexicons (apfst (Scan.extend_lexicon [Symbol.explode name]));
       
   160   Pretty.writeln (report_keyword name));
       
   161 
       
   162 fun command name kind =
       
   163  (change_lexicons (apsnd (Scan.extend_lexicon [Symbol.explode name]));
       
   164   change_commands (Symtab.update (name, kind));
       
   165   Pretty.writeln (report_command (name, kind)));
       
   166 
       
   167 end;