src/Pure/Isar/keyword.ML
author wenzelm
Fri, 04 Jan 2013 11:21:31 +0100
changeset 50714 2af9e4614ba4
parent 48900 e54cf66928e6
child 51225 3fe0d8d55975
permissions -rw-r--r--
more formal inlining of system information;
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
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 control: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    13
  val diag: T
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
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    16
  val thy_heading1: T
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    17
  val thy_heading2: T
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    18
  val thy_heading3: T
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    19
  val thy_heading4: T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    20
  val thy_decl: T
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    21
  val thy_load: T
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    22
  val thy_load_files: string list -> T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    23
  val thy_script: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    24
  val thy_goal: T
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
    25
  val thy_schematic_goal: T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    26
  val qed: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    27
  val qed_block: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    28
  val qed_global: T
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    29
  val prf_heading2: T
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    30
  val prf_heading3: T
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    31
  val prf_heading4: T
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    32
  val prf_goal: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    33
  val prf_block: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    34
  val prf_open: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    35
  val prf_close: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    36
  val prf_chain: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    37
  val prf_decl: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    38
  val prf_asm: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    39
  val prf_asm_goal: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    40
  val prf_script: T
46968
38aaa08fb37f less redundant data;
wenzelm
parents: 46967
diff changeset
    41
  val kinds: T list
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    42
  val tag: string -> T -> T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    43
  val tags_of: T -> string list
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    44
  val tag_theory: T -> T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    45
  val tag_proof: T -> T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    46
  val tag_ml: T -> T
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    47
  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
    48
  val spec: spec -> T
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 46969
diff changeset
    49
  val command_spec: (string * spec) * Position.T -> (string * T) * Position.T
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    50
  val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    51
  val is_keyword: string -> bool
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    52
  val command_keyword: string -> T option
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
    53
  val command_files: string -> string list
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    54
  val command_tags: string -> string list
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
    55
  val dest: unit -> string list * string list
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
    56
  val status: unit -> unit
46958
0ec8f04e753a define keywords early when processing the theory header, before running the body commands;
wenzelm
parents: 46957
diff changeset
    57
  val define: string * T option -> unit
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    58
  val is_diag: string -> bool
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    59
  val is_control: string -> bool
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    60
  val is_regular: string -> bool
40397
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
    61
  val is_heading: string -> bool
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
    62
  val is_theory_begin: string -> bool
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
    63
  val is_theory_load: string -> bool
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
    64
  val is_theory: string -> bool
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
    65
  val is_proof: string -> bool
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    66
  val is_theory_goal: string -> bool
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    67
  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
    68
  val is_schematic_goal: string -> bool
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    69
  val is_qed: string -> bool
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
    70
  val is_qed_global: string -> bool
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    71
end;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    72
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
    73
structure Keyword: KEYWORD =
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    74
struct
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    75
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
    76
(** keyword classification **)
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
datatype T = Keyword of
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    79
 {kind: string,
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    80
  files: string list,  (*extensions of embedded files*)
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    81
  tags: string list};  (*tags in canonical reverse order*)
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    82
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    83
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
    84
fun kind_of (Keyword {kind, ...}) = kind;
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    85
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
    86
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    87
fun add_files fs (Keyword {kind, files, tags}) =
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
    88
  Keyword {kind = kind, files = files @ fs, tags = tags};
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    89
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    90
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    91
(* kinds *)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    92
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    93
val control = kind "control";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    94
val diag = kind "diag";
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    95
val thy_begin = kind "thy_begin";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
    96
val thy_end = kind "thy_end";
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    97
val thy_heading1 = kind "thy_heading1";
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    98
val thy_heading2 = kind "thy_heading2";
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
    99
val thy_heading3 = kind "thy_heading3";
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   100
val thy_heading4 = kind "thy_heading4";
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
   101
val thy_decl = kind "thy_decl";
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   102
val thy_load = kind "thy_load";
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   103
fun thy_load_files files = Keyword {kind = "thy_load", files = files, tags = []};
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   104
val thy_script = kind "thy_script";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   105
val thy_goal = kind "thy_goal";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   106
val thy_schematic_goal = kind "thy_schematic_goal";
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   107
val qed = kind "qed";
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   108
val qed_block = kind "qed_block";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   109
val qed_global = kind "qed_global";
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   110
val prf_heading2 = kind "prf_heading2";
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   111
val prf_heading3 = kind "prf_heading3";
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   112
val prf_heading4 = kind "prf_heading4";
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   113
val prf_goal = kind "prf_goal";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   114
val prf_block = kind "prf_block";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   115
val prf_open = kind "prf_open";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   116
val prf_close = kind "prf_close";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   117
val prf_chain = kind "prf_chain";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   118
val prf_decl = kind "prf_decl";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   119
val prf_asm = kind "prf_asm";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   120
val prf_asm_goal = kind "prf_asm_goal";
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46961
diff changeset
   121
val prf_script = kind "prf_script";
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   122
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   123
val kinds =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   124
  [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   125
    thy_load, thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   126
    prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
46968
38aaa08fb37f less redundant data;
wenzelm
parents: 46967
diff changeset
   127
    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   128
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   129
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   130
(* tags *)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   131
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   132
fun tag t (Keyword {kind, files, tags}) =
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   133
  Keyword {kind = kind, files = files, tags = update (op =) t tags};
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   134
fun tags_of (Keyword {tags, ...}) = tags;
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   135
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   136
val tag_theory = tag "theory";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   137
val tag_proof = tag "proof";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   138
val tag_ml = tag "ML";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
   139
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   140
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   141
(* external names *)
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   142
46968
38aaa08fb37f less redundant data;
wenzelm
parents: 46967
diff changeset
   143
val name_table = Symtab.make (map (`kind_of) kinds);
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   144
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   145
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
   146
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   147
fun spec ((name, files), tags) =
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   148
  (case Symtab.lookup name_table name of
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   149
    SOME kind =>
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   150
      let val kind' = kind |> fold tag tags in
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   151
        if null files then kind'
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   152
        else if name = kind_of thy_load then kind' |> add_files files
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   153
        else error ("Illegal specification of files for " ^ quote name)
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   154
      end
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   155
  | NONE => error ("Unknown outer syntax keyword kind " ^ quote name));
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   156
48646
91281e9472d8 more official command specifications, including source position;
wenzelm
parents: 46969
diff changeset
   157
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
   158
46938
cda018294515 some support for outer syntax keyword declarations within theory header;
wenzelm
parents: 46924
diff changeset
   159
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   160
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   161
(** global keyword tables **)
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   162
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   163
datatype keywords = Keywords of
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   164
 {lexicons: Scan.lexicon * Scan.lexicon,  (*minor, major*)
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   165
  commands: T Symtab.table};  (*command classification*)
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   166
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   167
fun make_keywords (lexicons, commands) =
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   168
  Keywords {lexicons = lexicons, commands = commands};
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   169
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   170
local
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   171
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   172
val global_keywords =
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   173
  Unsynchronized.ref (make_keywords ((Scan.empty_lexicon, Scan.empty_lexicon), Symtab.empty));
27357
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
in
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   176
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   177
fun get_keywords () = ! global_keywords;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   178
48900
e54cf66928e6 tuned signature (again, cf. ff9cd47be39b);
wenzelm
parents: 48898
diff changeset
   179
fun change_keywords f = CRITICAL (fn () =>
e54cf66928e6 tuned signature (again, cf. ff9cd47be39b);
wenzelm
parents: 48898
diff changeset
   180
  Unsynchronized.change global_keywords
e54cf66928e6 tuned signature (again, cf. ff9cd47be39b);
wenzelm
parents: 48898
diff changeset
   181
    (fn Keywords {lexicons, commands} => make_keywords (f (lexicons, commands))));
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
48900
e54cf66928e6 tuned signature (again, cf. ff9cd47be39b);
wenzelm
parents: 48898
diff changeset
   185
fun get_lexicons () = get_keywords () |> (fn Keywords {lexicons, ...} => lexicons);
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   186
fun get_commands () = get_keywords () |> (fn Keywords {commands, ...} => commands);
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   187
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   188
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   189
(* lookup *)
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   190
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   191
fun is_keyword s =
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   192
  let
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   193
    val (minor, major) = get_lexicons ();
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   194
    val syms = Symbol.explode s;
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   195
  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
   196
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   197
fun command_keyword name = Symtab.lookup (get_commands ()) name;
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
   198
val command_files = these o Option.map (#2 o kind_files_of) o command_keyword;
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
   199
val command_tags = these o Option.map tags_of o command_keyword;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   200
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   201
fun dest () = pairself (sort_strings o Scan.dest_lexicon) (get_lexicons ());
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   202
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   203
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   204
(* status *)
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   205
38236
d8c7be27e01d explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
wenzelm
parents: 36955
diff changeset
   206
fun status () =
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   207
  let
48874
ff9cd47be39b refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents: 48872
diff changeset
   208
    val Keywords {lexicons = (minor, _), commands} = get_keywords ();
48709
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   209
    val _ = sort_strings (Scan.dest_lexicon minor) |> List.app (fn name =>
50714
2af9e4614ba4 more formal inlining of system information;
wenzelm
parents: 48900
diff changeset
   210
      writeln ("\fOuter syntax keyword " ^ quote name));
48709
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   211
    val _ = sort_wrt #1 (Symtab.dest commands) |> List.app (fn (name, kind) =>
50714
2af9e4614ba4 more formal inlining of system information;
wenzelm
parents: 48900
diff changeset
   212
      writeln ("\fOuter syntax keyword " ^ quote name ^ " :: " ^ kind_of kind));
46957
0c15caf47040 clarified Keyword.is_keyword: union of minor and major;
wenzelm
parents: 46950
diff changeset
   213
  in () end;
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   214
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   215
46958
0ec8f04e753a define keywords early when processing the theory header, before running the body commands;
wenzelm
parents: 46957
diff changeset
   216
(* define *)
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   217
48900
e54cf66928e6 tuned signature (again, cf. ff9cd47be39b);
wenzelm
parents: 48898
diff changeset
   218
fun define (name, opt_kind) = change_keywords (fn ((minor, major), commands) =>
48709
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   219
  (case opt_kind of
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   220
    NONE =>
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   221
      let
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   222
        val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   223
      in ((minor', major), commands) end
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   224
  | SOME kind =>
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   225
      let
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   226
        val major' = Scan.extend_lexicon (Symbol.explode name) major;
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   227
        val commands' = Symtab.update (name, kind) commands;
719f458cd89e prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol;
wenzelm
parents: 48646
diff changeset
   228
      in ((minor, major'), commands') end));
46945
26007caf6e9c declare keywords as side-effect of header edit;
wenzelm
parents: 46938
diff changeset
   229
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   230
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   231
(* command categories *)
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   232
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   233
fun command_category ks name =
27433
b82c12e57e79 added datatype category;
wenzelm
parents: 27357
diff changeset
   234
  (case command_keyword name of
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   235
    NONE => false
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   236
  | 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
   237
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   238
val is_diag = command_category [diag];
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   239
val is_control = command_category [control];
40397
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
   240
val is_regular = not o command_category [diag, control];
4ad71312a192 added Keyword.is_heading (cf. Scala version);
wenzelm
parents: 38413
diff changeset
   241
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   242
val is_heading =
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   243
  command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   244
    prf_heading2, prf_heading3, prf_heading4];
29347
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   245
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   246
val is_theory_begin = command_category [thy_begin];
b723fa577aa2 added is_control, is_regular, is_theory_begin;
wenzelm
parents: 28542
diff changeset
   247
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 48864
diff changeset
   248
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
   249
27440
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   250
val is_theory = command_category
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   251
  [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
48864
3ee314ae1e0a added keyword kind "thy_load" (with optional list of file extensions);
wenzelm
parents: 48709
diff changeset
   252
    thy_load, 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
   253
a1eda23752bd replaced datatype category constructivism by is_theory/is_proof;
wenzelm
parents: 27433
diff changeset
   254
val is_proof = command_category
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   255
  [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   256
    prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46968
diff changeset
   257
    prf_asm, prf_asm_goal, prf_script];
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   258
36315
e859879079c8 added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents: 34243
diff changeset
   259
val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   260
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
   261
val is_schematic_goal = command_category [thy_schematic_goal];
28431
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   262
val is_qed = command_category [qed, qed_block];
f12c1c68ec8e more command categories;
wenzelm
parents: 28345
diff changeset
   263
val is_qed_global = command_category [qed_global];
27520
fb07f3b32863 added is_diag;
wenzelm
parents: 27440
diff changeset
   264
27357
5b3a087ff292 moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
wenzelm
parents: 17270
diff changeset
   265
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
   266