src/Pure/Isar/keyword.ML
author wenzelm
Sat, 03 Mar 2012 18:18:39 +0100
changeset 46774 38f113b052b1
parent 46123 aa5c367ee579
child 46924 f2c60ad58374
permissions -rw-r--r--
clarified terminology of raw protocol messages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 36681
diff changeset
     1
(*  Title:      Pure/Isar/keyword.ML
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     3
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
     4
Isar command keyword classification and global keyword tables.
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     5
*)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     6
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 36681
diff changeset
     7
signature KEYWORD =
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     8
sig
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     9
  type T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    10
  val kind_of: T -> string
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    11
  val control: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    12
  val diag: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    13
  val thy_begin: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    14
  val thy_switch: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    15
  val thy_end: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    16
  val thy_heading: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    17
  val thy_decl: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    18
  val thy_script: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    19
  val thy_goal: T
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
    20
  val thy_schematic_goal: T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    21
  val qed: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    22
  val qed_block: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    23
  val qed_global: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    24
  val prf_heading: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    25
  val prf_goal: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    26
  val prf_block: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    27
  val prf_open: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    28
  val prf_close: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    29
  val prf_chain: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    30
  val prf_decl: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    31
  val prf_asm: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    32
  val prf_asm_goal: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    33
  val prf_script: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    34
  val kinds: string list
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    35
  val update_tags: string -> string list -> string list
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    36
  val tag: string -> T -> T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    37
  val tags_of: T -> string list
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    38
  val tag_theory: T -> T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    39
  val tag_proof: T -> T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    40
  val tag_ml: T -> T
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    41
  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    42
  val is_keyword: string -> bool
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    43
  val dest_keywords: unit -> string list
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    44
  val dest_commands: unit -> string list
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    45
  val command_keyword: string -> T option
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    46
  val command_tags: string -> string list
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
    47
  val keyword_statusN: string
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
    48
  val status: unit -> unit
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    49
  val keyword: string -> unit
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    50
  val command: string -> T -> unit
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    51
  val is_diag: string -> bool
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    52
  val is_control: string -> bool
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    53
  val is_regular: string -> bool
40397
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
    54
  val is_heading: string -> bool
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    55
  val is_theory_begin: string -> bool
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
    56
  val is_theory: string -> bool
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
    57
  val is_proof: string -> bool
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    58
  val is_theory_goal: string -> bool
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    59
  val is_proof_goal: string -> bool
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
    60
  val is_schematic_goal: string -> bool
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    61
  val is_qed: string -> bool
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    62
  val is_qed_global: string -> bool
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    63
end;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    64
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 36681
diff changeset
    65
structure Keyword: KEYWORD =
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    66
struct
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    67
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    68
(** keyword classification **)
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    69
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    70
datatype T = Keyword of string * string list;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    71
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    72
fun kind s = Keyword (s, []);
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    73
fun kind_of (Keyword (s, _)) = s;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    74
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    75
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    76
(* kinds *)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    77
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    78
val control = kind "control";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    79
val diag = kind "diag";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    80
val thy_begin = kind "theory-begin";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    81
val thy_switch = kind "theory-switch";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    82
val thy_end = kind "theory-end";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    83
val thy_heading = kind "theory-heading";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    84
val thy_decl = kind "theory-decl";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    85
val thy_script = kind "theory-script";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    86
val thy_goal = kind "theory-goal";
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
    87
val thy_schematic_goal = kind "theory-schematic-goal";
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    88
val qed = kind "qed";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    89
val qed_block = kind "qed-block";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    90
val qed_global = kind "qed-global";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    91
val prf_heading = kind "proof-heading";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    92
val prf_goal = kind "proof-goal";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    93
val prf_block = kind "proof-block";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    94
val prf_open = kind "proof-open";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    95
val prf_close = kind "proof-close";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    96
val prf_chain = kind "proof-chain";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    97
val prf_decl = kind "proof-decl";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    98
val prf_asm = kind "proof-asm";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    99
val prf_asm_goal = kind "proof-asm-goal";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   100
val prf_script = kind "proof-script";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   101
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   102
val kinds =
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   103
  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   104
    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   105
    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   106
 |> map kind_of;
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   107
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   108
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   109
(* tags *)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   110
17270
534b6e5e3736 eliminated 1 call to polyEq
haftmann
parents: 17059
diff changeset
   111
fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   112
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   113
fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   114
fun tags_of (Keyword (_, ts)) = ts;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   115
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   116
val tag_theory = tag "theory";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   117
val tag_proof = tag "proof";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   118
val tag_ml = tag "ML";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   119
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   120
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   121
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   122
(** global keyword tables **)
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   123
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   124
local
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   125
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30670
diff changeset
   126
val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30670
diff changeset
   127
val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   128
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   129
in
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   130
33223
d27956b4d3b4 non-critical atomic accesses;
wenzelm
parents: 32738
diff changeset
   131
fun get_commands () = ! global_commands;
d27956b4d3b4 non-critical atomic accesses;
wenzelm
parents: 32738
diff changeset
   132
fun get_lexicons () = ! global_lexicons;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   133
32738
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30670
diff changeset
   134
fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
15bb09ca0378 explicit indication of Unsynchronized.ref;
wenzelm
parents: 30670
diff changeset
   135
fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   136
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   137
end;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   138
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   139
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   140
(* lookup *)
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   141
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   142
fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
27805
2e533bcd1343 dest: sort strings;
wenzelm
parents: 27768
diff changeset
   143
fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   144
27805
2e533bcd1343 dest: sort strings;
wenzelm
parents: 27768
diff changeset
   145
fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   146
fun command_keyword name = Symtab.lookup (get_commands ()) name;
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   147
fun command_tags name = these (Option.map tags_of (command_keyword name));
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   148
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   149
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   150
(* status *)
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   151
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   152
val keyword_statusN = "keyword_status";
34243
8821e3293702 report keywords as singleton messages, control message kind via print mode;
wenzelm
parents: 33223
diff changeset
   153
46123
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 45666
diff changeset
   154
fun status_message m s =
38413
224efb14f258 Keyword.status: always suppress position;
wenzelm
parents: 38236
diff changeset
   155
  Position.setmp_thread_data Position.none
46774
38f113b052b1 clarified terminology of raw protocol messages;
wenzelm
parents: 46123
diff changeset
   156
    (if print_mode_active keyword_statusN then Output.protocol_message m else writeln) s;
34243
8821e3293702 report keywords as singleton messages, control message kind via print mode;
wenzelm
parents: 33223
diff changeset
   157
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   158
fun keyword_status name =
46123
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 45666
diff changeset
   159
  status_message (Isabelle_Markup.keyword_decl name)
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 45666
diff changeset
   160
    ("Outer syntax keyword: " ^ quote name);
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   161
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   162
fun command_status (name, kind) =
46123
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 45666
diff changeset
   163
  status_message (Isabelle_Markup.command_decl name (kind_of kind))
aa5c367ee579 prefer raw_message for protocol implementation;
wenzelm
parents: 45666
diff changeset
   164
    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
30670
9bb872667af6 suppress status output for traditional tty modes (including Proof General);
wenzelm
parents: 29347
diff changeset
   165
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   166
fun status () =
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   167
  let val (keywords, commands) = CRITICAL (fn () =>
27805
2e533bcd1343 dest: sort strings;
wenzelm
parents: 27768
diff changeset
   168
    (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
34243
8821e3293702 report keywords as singleton messages, control message kind via print mode;
wenzelm
parents: 33223
diff changeset
   169
  in
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   170
    List.app keyword_status keywords;
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   171
    List.app command_status commands
34243
8821e3293702 report keywords as singleton messages, control message kind via print mode;
wenzelm
parents: 33223
diff changeset
   172
  end;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   173
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   174
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   175
(* augment tables *)
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   176
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   177
fun keyword name =
27768
398c64b2acef adapted Scan.extend_lexicon/merge_lexicons;
wenzelm
parents: 27526
diff changeset
   178
 (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   179
  keyword_status name);
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   180
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   181
fun command name kind =
27768
398c64b2acef adapted Scan.extend_lexicon/merge_lexicons;
wenzelm
parents: 27526
diff changeset
   182
 (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   183
  change_commands (Symtab.update (name, kind));
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   184
  command_status (name, kind));
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   185
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   186
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   187
(* command categories *)
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   188
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   189
fun command_category ks name =
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   190
  (case command_keyword name of
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   191
    NONE => false
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   192
  | SOME k => member (op = o pairself kind_of) ks k);
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   193
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   194
val is_diag = command_category [diag];
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   195
val is_control = command_category [control];
40397
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
   196
val is_regular = not o command_category [diag, control];
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
   197
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
   198
val is_heading = command_category [thy_heading, prf_heading];
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   199
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   200
val is_theory_begin = command_category [thy_begin];
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   201
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   202
val is_theory = command_category
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   203
  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   204
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   205
val is_proof = command_category
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   206
  [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   207
    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   208
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   209
val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   210
val is_proof_goal = command_category [prf_goal, prf_asm_goal];
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   211
val is_schematic_goal = command_category [thy_schematic_goal];
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   212
val is_qed = command_category [qed, qed_block];
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   213
val is_qed_global = command_category [qed_global];
27520
fb07f3b32863 added is_diag;
wenzelm
parents: 27440
diff changeset
   214
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   215
end;
36949
080e85d46108 renamed structure OuterKeyword to Keyword and OuterParse to Parse, keeping the old names as legacy aliases for some time;
wenzelm
parents: 36681
diff changeset
   216