src/Pure/Isar/keyword.ML
author wenzelm
Thu, 06 Nov 2014 11:44:41 +0100
changeset 58918 8d36bc5eaed3
parent 58906 29788e989d61
child 58919 82a71046dce8
permissions -rw-r--r--
simplified keyword kinds; more explicit bootstrap syntax;
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
58900
1435cc20b022 explicit type Keyword.Keywords;
wenzelm
parents: 58868
diff changeset
     4
Isar keyword classification.
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
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    11
  val kind_files_of: T -> string * string list
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    12
  val diag: T
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
    13
  val heading: T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    14
  val thy_begin: 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_decl: T
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 56944
diff changeset
    17
  val thy_decl_block: T
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    18
  val thy_load: T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    19
  val thy_goal: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    20
  val qed: T
53571
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    21
  val qed_script: T
17059
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_goal: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    25
  val prf_block: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    26
  val prf_open: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    27
  val prf_close: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    28
  val prf_chain: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    29
  val prf_decl: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    30
  val prf_asm: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    31
  val prf_asm_goal: T
53371
47b23c582127 more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents: 52440
diff changeset
    32
  val prf_asm_goal_script: T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    33
  val prf_script: T
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    34
  type spec = (string * string list) * string list
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
    35
  val spec: spec -> T
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 46969
diff changeset
    36
  val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    37
  type keywords
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    38
  val minor_keywords: keywords -> Scan.lexicon
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    39
  val major_keywords: keywords -> Scan.lexicon
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    40
  val empty_keywords: keywords
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    41
  val merge_keywords: keywords * keywords -> keywords
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    42
  val no_command_keywords: keywords -> keywords
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    43
  val add: string * T option -> keywords -> keywords
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    44
  val define: string * T option -> unit
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
    45
  val get_keywords: unit -> keywords
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    46
  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    47
  val is_keyword: string -> bool
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    48
  val command_keyword: string -> T option
54523
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
    49
  val command_files: string -> Path.T -> Path.T list
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    50
  val command_tags: string -> string list
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    51
  val is_diag: string -> bool
40397
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
    52
  val is_heading: string -> bool
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    53
  val is_theory_begin: string -> bool
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
    54
  val is_theory_load: string -> bool
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
    55
  val is_theory: string -> bool
56944
578dc6b4be89 no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents: 56895
diff changeset
    56
  val is_theory_body: string -> bool
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
    57
  val is_proof: string -> bool
51225
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
    58
  val is_proof_body: string -> bool
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    59
  val is_theory_goal: string -> bool
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    60
  val is_proof_goal: string -> bool
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
56895
f058120aaad4 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents: 56146
diff changeset
    63
  val is_printed: string -> bool
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    64
end;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    65
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
    66
structure Keyword: KEYWORD =
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    67
struct
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    68
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    69
(** keyword classification **)
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    70
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
    71
(* kinds *)
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
    72
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    73
datatype T = Keyword of
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    74
 {kind: string,
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    75
  files: string list,  (*extensions of embedded files*)
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
    76
  tags: string list};
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    77
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    78
fun kind s = Keyword {kind = s, files = [], tags = []};
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    79
fun kind_of (Keyword {kind, ...}) = kind;
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    80
fun kind_files_of (Keyword {kind, files, ...}) = (kind, files);
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    81
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    82
val diag = kind "diag";
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
    83
val heading = kind "heading";
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    84
val thy_begin = kind "thy_begin";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    85
val thy_end = kind "thy_end";
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
    86
val thy_decl = kind "thy_decl";
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 56944
diff changeset
    87
val thy_decl_block = kind "thy_decl_block";
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    88
val thy_load = kind "thy_load";
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    89
val thy_goal = kind "thy_goal";
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    90
val qed = kind "qed";
53571
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    91
val qed_script = kind "qed_script";
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    92
val qed_block = kind "qed_block";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    93
val qed_global = kind "qed_global";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    94
val prf_goal = kind "prf_goal";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    95
val prf_block = kind "prf_block";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    96
val prf_open = kind "prf_open";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    97
val prf_close = kind "prf_close";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    98
val prf_chain = kind "prf_chain";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    99
val prf_decl = kind "prf_decl";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   100
val prf_asm = kind "prf_asm";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   101
val prf_asm_goal = kind "prf_asm_goal";
53371
47b23c582127 more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents: 52440
diff changeset
   102
val prf_asm_goal_script = kind "prf_asm_goal_script";
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   103
val prf_script = kind "prf_script";
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   104
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   105
val kinds =
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   106
  [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal,
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   107
    qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   108
    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   109
  |> map kind_of;
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   110
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   111
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   112
(* specifications *)
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   113
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   114
type spec = (string * string list) * string list;
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   115
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   116
fun spec ((kind, files), tags) =
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   117
  if not (member (op =) kinds kind) then
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   118
    error ("Unknown outer syntax keyword kind " ^ quote kind)
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   119
  else if not (null files) andalso kind <> kind_of thy_load then
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   120
    error ("Illegal specification of files for " ^ quote kind)
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   121
  else Keyword {kind = kind, files = files, tags = tags};
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   122
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 46969
diff changeset
   123
fun command_spec ((name, s), pos) = ((name, spec s), pos);
46961
5c6955f487e5 outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents: 46958
diff changeset
   124
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   125
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   126
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   127
(** keyword tables **)
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   128
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   129
(* type keywords *)
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   130
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   131
datatype keywords = Keywords of
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   132
 {minor: Scan.lexicon,
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   133
  major: Scan.lexicon,
58906
wenzelm
parents: 58903
diff changeset
   134
  commands: T Symtab.table};
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   135
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   136
fun minor_keywords (Keywords {minor, ...}) = minor;
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   137
fun major_keywords (Keywords {major, ...}) = major;
58906
wenzelm
parents: 58903
diff changeset
   138
fun commands (Keywords {commands, ...}) = commands;
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   139
58906
wenzelm
parents: 58903
diff changeset
   140
fun make_keywords (minor, major, commands) =
wenzelm
parents: 58903
diff changeset
   141
  Keywords {minor = minor, major = major, commands = commands};
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   142
58906
wenzelm
parents: 58903
diff changeset
   143
fun map_keywords f (Keywords {minor, major, commands}) =
wenzelm
parents: 58903
diff changeset
   144
  make_keywords (f (minor, major, commands));
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   145
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   146
val empty_keywords =
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   147
  make_keywords (Scan.empty_lexicon, Scan.empty_lexicon, Symtab.empty);
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   148
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   149
fun merge_keywords
58906
wenzelm
parents: 58903
diff changeset
   150
  (Keywords {minor = minor1, major = major1, commands = commands1},
wenzelm
parents: 58903
diff changeset
   151
    Keywords {minor = minor2, major = major2, commands = commands2}) =
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   152
  make_keywords
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   153
   (Scan.merge_lexicons (minor1, minor2),
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   154
    Scan.merge_lexicons (major1, major2),
58906
wenzelm
parents: 58903
diff changeset
   155
    Symtab.merge (K true) (commands1, commands2));
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   156
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   157
val no_command_keywords =
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   158
  map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty));
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   159
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   160
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   161
(* add keywords *)
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   162
58906
wenzelm
parents: 58903
diff changeset
   163
fun add (name, opt_kind) = map_keywords (fn (minor, major, commands) =>
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   164
  (case opt_kind of
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   165
    NONE =>
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   166
      let
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   167
        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
58906
wenzelm
parents: 58903
diff changeset
   168
      in (minor', major, commands) end
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   169
  | SOME kind =>
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   170
      let
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   171
        val major' = Scan.extend_lexicon (Symbol.explode name) major;
58906
wenzelm
parents: 58903
diff changeset
   172
        val commands' = Symtab.update (name, kind) commands;
wenzelm
parents: 58903
diff changeset
   173
      in (minor, major', commands') end));
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   174
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   175
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   176
(* global state *)
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   177
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   178
local val global_keywords = Unsynchronized.ref empty_keywords in
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   179
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   180
fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add decl));
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   181
fun get_keywords () = ! global_keywords;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   182
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   183
end;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   184
58903
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   185
fun get_lexicons () =
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   186
  let val keywords = get_keywords ()
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   187
  in (minor_keywords keywords, major_keywords keywords) end;
38c72f5f6c2e explicit type Keyword.keywords;
wenzelm
parents: 58900
diff changeset
   188
58906
wenzelm
parents: 58903
diff changeset
   189
fun get_commands () = commands (get_keywords ());
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   190
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   191
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   192
(* lookup *)
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   193
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   194
fun is_keyword s =
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   195
  let
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   196
    val (minor, major) = get_lexicons ();
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   197
    val syms = Symbol.explode s;
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   198
  in Scan.is_literal minor syms orelse Scan.is_literal major syms end;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   199
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   200
fun command_keyword name = Symtab.lookup (get_commands ()) name;
54523
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   201
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   202
fun command_files name path =
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   203
  (case command_keyword name of
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   204
    NONE => []
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   205
  | SOME (Keyword {kind, files, ...}) =>
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   206
      if kind <> kind_of thy_load then []
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   207
      else if null files then [path]
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   208
      else map (fn ext => Path.ext ext path) files);
11087efad95e more uniform handling of inlined files;
wenzelm
parents: 53571
diff changeset
   209
58918
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   210
fun command_tags name =
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   211
  (case command_keyword name of
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   212
    SOME (Keyword {tags, ...}) => tags
8d36bc5eaed3 simplified keyword kinds;
wenzelm
parents: 58906
diff changeset
   213
  | NONE => []);
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   214
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   215
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   216
(* command categories *)
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   217
51225
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   218
fun command_category ks =
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   219
  let val tab = Symtab.make_set (map kind_of ks) in
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   220
    fn name =>
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   221
      (case command_keyword name of
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   222
        NONE => false
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   223
      | SOME k => Symtab.defined tab (kind_of k))
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   224
  end;
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   225
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   226
val is_diag = command_category [diag];
40397
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
   227
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   228
val is_heading = command_category [heading];
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   229
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   230
val is_theory_begin = command_category [thy_begin];
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   231
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
   232
val is_theory_load = command_category [thy_load];
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
   233
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   234
val is_theory = command_category
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   235
  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   236
56944
578dc6b4be89 no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents: 56895
diff changeset
   237
val is_theory_body = command_category
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   238
  [thy_load, thy_decl, thy_decl_block, thy_goal];
56944
578dc6b4be89 no reset for 'end' -- e.g. relevant for 'notepad';
wenzelm
parents: 56895
diff changeset
   239
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   240
val is_proof = command_category
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   241
  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   242
    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   243
51225
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   244
val is_proof_body = command_category
58868
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   245
  [diag, heading, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm,
c5e1cce7ace3 uniform heading commands work in any context, even in theory header;
wenzelm
parents: 58853
diff changeset
   246
    prf_asm_goal, prf_asm_goal_script, prf_script];
51225
3fe0d8d55975 support nested Thy_Syntax.element;
wenzelm
parents: 50714
diff changeset
   247
51274
cfc83ad52571 discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
wenzelm
parents: 51225
diff changeset
   248
val is_theory_goal = command_category [thy_goal];
53371
47b23c582127 more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents: 52440
diff changeset
   249
val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
53571
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
   250
val is_qed = command_category [qed, qed_script, qed_block];
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   251
val is_qed_global = command_category [qed_global];
27520
fb07f3b32863 added is_diag;
wenzelm
parents: 27440
diff changeset
   252
56895
f058120aaad4 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents: 56146
diff changeset
   253
val is_printed = is_theory_goal orf is_proof;
f058120aaad4 discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;
wenzelm
parents: 56146
diff changeset
   254
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   255
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
   256