src/Pure/Isar/keyword.ML
author wenzelm
Fri Apr 08 16:34:14 2011 +0200 (2011-04-08)
changeset 42290 b1f544c84040
parent 40397 4ad71312a192
child 45666 d83797ef0d2d
permissions -rw-r--r--
discontinued special treatment of structure Lexicon;
wenzelm@36949
     1
(*  Title:      Pure/Isar/keyword.ML
wenzelm@17059
     2
    Author:     Makarius
wenzelm@17059
     3
wenzelm@27357
     4
Isar command keyword classification and global keyword tables.
wenzelm@17059
     5
*)
wenzelm@17059
     6
wenzelm@36949
     7
signature KEYWORD =
wenzelm@17059
     8
sig
wenzelm@17059
     9
  type T
wenzelm@17059
    10
  val kind_of: T -> string
wenzelm@17059
    11
  val control: T
wenzelm@17059
    12
  val diag: T
wenzelm@17059
    13
  val thy_begin: T
wenzelm@17059
    14
  val thy_switch: T
wenzelm@17059
    15
  val thy_end: T
wenzelm@17059
    16
  val thy_heading: T
wenzelm@17059
    17
  val thy_decl: T
wenzelm@17059
    18
  val thy_script: T
wenzelm@17059
    19
  val thy_goal: T
wenzelm@36315
    20
  val thy_schematic_goal: T
wenzelm@17059
    21
  val qed: T
wenzelm@17059
    22
  val qed_block: T
wenzelm@17059
    23
  val qed_global: T
wenzelm@17059
    24
  val prf_heading: T
wenzelm@17059
    25
  val prf_goal: T
wenzelm@17059
    26
  val prf_block: T
wenzelm@17059
    27
  val prf_open: T
wenzelm@17059
    28
  val prf_close: T
wenzelm@17059
    29
  val prf_chain: T
wenzelm@17059
    30
  val prf_decl: T
wenzelm@17059
    31
  val prf_asm: T
wenzelm@17059
    32
  val prf_asm_goal: T
wenzelm@17059
    33
  val prf_script: T
wenzelm@17059
    34
  val kinds: string list
wenzelm@17059
    35
  val update_tags: string -> string list -> string list
wenzelm@17059
    36
  val tag: string -> T -> T
wenzelm@17059
    37
  val tags_of: T -> string list
wenzelm@17059
    38
  val tag_theory: T -> T
wenzelm@17059
    39
  val tag_proof: T -> T
wenzelm@17059
    40
  val tag_ml: T -> T
wenzelm@27357
    41
  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
wenzelm@27357
    42
  val is_keyword: string -> bool
wenzelm@27357
    43
  val dest_keywords: unit -> string list
wenzelm@27357
    44
  val dest_commands: unit -> string list
wenzelm@27357
    45
  val command_keyword: string -> T option
wenzelm@27357
    46
  val command_tags: string -> string list
wenzelm@38236
    47
  val keyword_statusN: string
wenzelm@38236
    48
  val status: unit -> unit
wenzelm@27357
    49
  val keyword: string -> unit
wenzelm@27357
    50
  val command: string -> T -> unit
wenzelm@29347
    51
  val is_diag: string -> bool
wenzelm@29347
    52
  val is_control: string -> bool
wenzelm@29347
    53
  val is_regular: string -> bool
wenzelm@40397
    54
  val is_heading: string -> bool
wenzelm@29347
    55
  val is_theory_begin: string -> bool
wenzelm@27440
    56
  val is_theory: string -> bool
wenzelm@27440
    57
  val is_proof: string -> bool
wenzelm@28431
    58
  val is_theory_goal: string -> bool
wenzelm@28431
    59
  val is_proof_goal: string -> bool
wenzelm@36315
    60
  val is_schematic_goal: string -> bool
wenzelm@28431
    61
  val is_qed: string -> bool
wenzelm@28431
    62
  val is_qed_global: string -> bool
wenzelm@17059
    63
end;
wenzelm@17059
    64
wenzelm@36949
    65
structure Keyword: KEYWORD =
wenzelm@17059
    66
struct
wenzelm@17059
    67
wenzelm@27357
    68
(** keyword classification **)
wenzelm@17059
    69
wenzelm@17059
    70
datatype T = Keyword of string * string list;
wenzelm@17059
    71
wenzelm@17059
    72
fun kind s = Keyword (s, []);
wenzelm@17059
    73
fun kind_of (Keyword (s, _)) = s;
wenzelm@17059
    74
wenzelm@17059
    75
wenzelm@17059
    76
(* kinds *)
wenzelm@17059
    77
wenzelm@17059
    78
val control = kind "control";
wenzelm@17059
    79
val diag = kind "diag";
wenzelm@17059
    80
val thy_begin = kind "theory-begin";
wenzelm@17059
    81
val thy_switch = kind "theory-switch";
wenzelm@17059
    82
val thy_end = kind "theory-end";
wenzelm@17059
    83
val thy_heading = kind "theory-heading";
wenzelm@17059
    84
val thy_decl = kind "theory-decl";
wenzelm@17059
    85
val thy_script = kind "theory-script";
wenzelm@17059
    86
val thy_goal = kind "theory-goal";
wenzelm@36315
    87
val thy_schematic_goal = kind "theory-schematic-goal";
wenzelm@17059
    88
val qed = kind "qed";
wenzelm@17059
    89
val qed_block = kind "qed-block";
wenzelm@17059
    90
val qed_global = kind "qed-global";
wenzelm@17059
    91
val prf_heading = kind "proof-heading";
wenzelm@17059
    92
val prf_goal = kind "proof-goal";
wenzelm@17059
    93
val prf_block = kind "proof-block";
wenzelm@17059
    94
val prf_open = kind "proof-open";
wenzelm@17059
    95
val prf_close = kind "proof-close";
wenzelm@17059
    96
val prf_chain = kind "proof-chain";
wenzelm@17059
    97
val prf_decl = kind "proof-decl";
wenzelm@17059
    98
val prf_asm = kind "proof-asm";
wenzelm@17059
    99
val prf_asm_goal = kind "proof-asm-goal";
wenzelm@17059
   100
val prf_script = kind "proof-script";
wenzelm@17059
   101
wenzelm@36315
   102
val kinds =
wenzelm@36315
   103
  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
wenzelm@36315
   104
    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
wenzelm@36315
   105
    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
wenzelm@36315
   106
 |> map kind_of;
wenzelm@17059
   107
wenzelm@17059
   108
wenzelm@17059
   109
(* tags *)
wenzelm@17059
   110
haftmann@17270
   111
fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
wenzelm@17059
   112
wenzelm@17059
   113
fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
wenzelm@17059
   114
fun tags_of (Keyword (_, ts)) = ts;
wenzelm@17059
   115
wenzelm@17059
   116
val tag_theory = tag "theory";
wenzelm@17059
   117
val tag_proof = tag "proof";
wenzelm@17059
   118
val tag_ml = tag "ML";
wenzelm@17059
   119
wenzelm@27357
   120
wenzelm@27357
   121
wenzelm@27357
   122
(** global keyword tables **)
wenzelm@27357
   123
wenzelm@27357
   124
local
wenzelm@27357
   125
wenzelm@32738
   126
val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
wenzelm@32738
   127
val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
wenzelm@27357
   128
wenzelm@27357
   129
in
wenzelm@27357
   130
wenzelm@33223
   131
fun get_commands () = ! global_commands;
wenzelm@33223
   132
fun get_lexicons () = ! global_lexicons;
wenzelm@27357
   133
wenzelm@32738
   134
fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
wenzelm@32738
   135
fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
wenzelm@27357
   136
wenzelm@17059
   137
end;
wenzelm@27357
   138
wenzelm@27357
   139
wenzelm@27357
   140
(* lookup *)
wenzelm@27357
   141
wenzelm@27357
   142
fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
wenzelm@27805
   143
fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
wenzelm@27357
   144
wenzelm@27805
   145
fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
wenzelm@27357
   146
fun command_keyword name = Symtab.lookup (get_commands ()) name;
wenzelm@27357
   147
fun command_tags name = these (Option.map tags_of (command_keyword name));
wenzelm@27357
   148
wenzelm@27357
   149
wenzelm@38236
   150
(* status *)
wenzelm@27357
   151
wenzelm@38236
   152
val keyword_statusN = "keyword_status";
wenzelm@34243
   153
wenzelm@38236
   154
fun status_message s =
wenzelm@38413
   155
  Position.setmp_thread_data Position.none
wenzelm@38413
   156
    (if print_mode_active keyword_statusN then Output.status else writeln) s;
wenzelm@34243
   157
wenzelm@38236
   158
fun keyword_status name =
wenzelm@38236
   159
  status_message (Markup.markup (Markup.keyword_decl name)
wenzelm@34243
   160
    ("Outer syntax keyword: " ^ quote name));
wenzelm@27357
   161
wenzelm@38236
   162
fun command_status (name, kind) =
wenzelm@38236
   163
  status_message (Markup.markup (Markup.command_decl name (kind_of kind))
wenzelm@34243
   164
    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
wenzelm@30670
   165
wenzelm@38236
   166
fun status () =
wenzelm@27357
   167
  let val (keywords, commands) = CRITICAL (fn () =>
wenzelm@27805
   168
    (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
wenzelm@34243
   169
  in
wenzelm@38236
   170
    List.app keyword_status keywords;
wenzelm@38236
   171
    List.app command_status commands
wenzelm@34243
   172
  end;
wenzelm@27357
   173
wenzelm@27357
   174
wenzelm@27357
   175
(* augment tables *)
wenzelm@27357
   176
wenzelm@27357
   177
fun keyword name =
wenzelm@27768
   178
 (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
wenzelm@38236
   179
  keyword_status name);
wenzelm@27357
   180
wenzelm@27357
   181
fun command name kind =
wenzelm@27768
   182
 (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
wenzelm@27357
   183
  change_commands (Symtab.update (name, kind));
wenzelm@38236
   184
  command_status (name, kind));
wenzelm@27357
   185
wenzelm@27433
   186
wenzelm@28431
   187
(* command categories *)
wenzelm@27433
   188
wenzelm@27440
   189
fun command_category ks name =
wenzelm@27433
   190
  (case command_keyword name of
wenzelm@27440
   191
    NONE => false
wenzelm@28431
   192
  | SOME k => member (op = o pairself kind_of) ks k);
wenzelm@27440
   193
wenzelm@29347
   194
val is_diag = command_category [diag];
wenzelm@29347
   195
val is_control = command_category [control];
wenzelm@40397
   196
val is_regular = not o command_category [diag, control];
wenzelm@40397
   197
wenzelm@40397
   198
val is_heading = command_category [thy_heading, prf_heading];
wenzelm@29347
   199
wenzelm@29347
   200
val is_theory_begin = command_category [thy_begin];
wenzelm@29347
   201
wenzelm@27440
   202
val is_theory = command_category
wenzelm@36315
   203
  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
wenzelm@27440
   204
wenzelm@27440
   205
val is_proof = command_category
wenzelm@28431
   206
  [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
wenzelm@28431
   207
    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
wenzelm@28431
   208
wenzelm@36315
   209
val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
wenzelm@28431
   210
val is_proof_goal = command_category [prf_goal, prf_asm_goal];
wenzelm@36315
   211
val is_schematic_goal = command_category [thy_schematic_goal];
wenzelm@28431
   212
val is_qed = command_category [qed, qed_block];
wenzelm@28431
   213
val is_qed_global = command_category [qed_global];
wenzelm@27520
   214
wenzelm@27357
   215
end;
wenzelm@36949
   216