src/Pure/Isar/outer_keyword.ML
author haftmann
Thu, 24 May 2007 08:37:37 +0200
changeset 23086 12320f6e2523
parent 17270 534b6e5e3736
child 27357 5b3a087ff292
permissions -rw-r--r--
tuned Pure/General/name_space.ML
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17059
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/outer_keyword.ML
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     4
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     5
Isar command keyword classification.
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     6
*)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     7
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     8
signature OUTER_KEYWORD =
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
     9
sig
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    10
  type T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    11
  val kind_of: T -> string
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_switch: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    16
  val thy_end: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    17
  val thy_heading: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    18
  val thy_decl: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    19
  val thy_script: T
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    20
  val thy_goal: T
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
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    41
end;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    42
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    43
structure OuterKeyword: OUTER_KEYWORD =
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    44
struct
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    45
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    46
(* keyword classification *)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    47
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    48
datatype T = Keyword of string * string list;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    49
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    50
fun kind s = Keyword (s, []);
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    51
fun kind_of (Keyword (s, _)) = s;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    52
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    53
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    54
(* kinds *)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    55
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    56
val control = kind "control";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    57
val diag = kind "diag";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    58
val thy_begin = kind "theory-begin";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    59
val thy_switch = kind "theory-switch";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    60
val thy_end = kind "theory-end";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    61
val thy_heading = kind "theory-heading";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    62
val thy_decl = kind "theory-decl";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    63
val thy_script = kind "theory-script";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    64
val thy_goal = kind "theory-goal";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    65
val qed = kind "qed";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    66
val qed_block = kind "qed-block";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    67
val qed_global = kind "qed-global";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    68
val prf_heading = kind "proof-heading";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    69
val prf_goal = kind "proof-goal";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    70
val prf_block = kind "proof-block";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    71
val prf_open = kind "proof-open";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    72
val prf_close = kind "proof-close";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    73
val prf_chain = kind "proof-chain";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    74
val prf_decl = kind "proof-decl";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    75
val prf_asm = kind "proof-asm";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    76
val prf_asm_goal = kind "proof-asm-goal";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    77
val prf_script = kind "proof-script";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    78
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    79
val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    80
  thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    81
  prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    82
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    83
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    84
(* tags *)
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    85
17270
534b6e5e3736 eliminated 1 call to polyEq
haftmann
parents: 17059
diff changeset
    86
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
    87
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    88
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
    89
fun tags_of (Keyword (_, ts)) = ts;
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
val tag_theory = tag "theory";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    92
val tag_proof = tag "proof";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    93
val tag_ml = tag "ML";
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    94
a001a3ebfcfd Isar command keyword classification (from Isar/outer_syntax.ML);
wenzelm
parents:
diff changeset
    95
end;