src/Pure/Isar/outer_keyword.ML
author wenzelm
Tue Dec 05 22:14:42 2006 +0100 (2006-12-05)
changeset 21658 5e31241e1e3c
parent 17270 534b6e5e3736
child 27357 5b3a087ff292
permissions -rw-r--r--
Attrib.internal: morphism;
wenzelm@17059
     1
(*  Title:      Pure/Isar/outer_keyword.ML
wenzelm@17059
     2
    ID:         $Id$
wenzelm@17059
     3
    Author:     Makarius
wenzelm@17059
     4
wenzelm@17059
     5
Isar command keyword classification.
wenzelm@17059
     6
*)
wenzelm@17059
     7
wenzelm@17059
     8
signature OUTER_KEYWORD =
wenzelm@17059
     9
sig
wenzelm@17059
    10
  type T
wenzelm@17059
    11
  val kind_of: T -> string
wenzelm@17059
    12
  val control: T
wenzelm@17059
    13
  val diag: T
wenzelm@17059
    14
  val thy_begin: T
wenzelm@17059
    15
  val thy_switch: T
wenzelm@17059
    16
  val thy_end: T
wenzelm@17059
    17
  val thy_heading: T
wenzelm@17059
    18
  val thy_decl: T
wenzelm@17059
    19
  val thy_script: T
wenzelm@17059
    20
  val thy_goal: T
wenzelm@17059
    21
  val qed: T
wenzelm@17059
    22
  val qed_block: T
wenzelm@17059
    23
  val qed_global: T
wenzelm@17059
    24
  val prf_heading: T
wenzelm@17059
    25
  val prf_goal: T
wenzelm@17059
    26
  val prf_block: T
wenzelm@17059
    27
  val prf_open: T
wenzelm@17059
    28
  val prf_close: T
wenzelm@17059
    29
  val prf_chain: T
wenzelm@17059
    30
  val prf_decl: T
wenzelm@17059
    31
  val prf_asm: T
wenzelm@17059
    32
  val prf_asm_goal: T
wenzelm@17059
    33
  val prf_script: T
wenzelm@17059
    34
  val kinds: string list
wenzelm@17059
    35
  val update_tags: string -> string list -> string list
wenzelm@17059
    36
  val tag: string -> T -> T
wenzelm@17059
    37
  val tags_of: T -> string list
wenzelm@17059
    38
  val tag_theory: T -> T
wenzelm@17059
    39
  val tag_proof: T -> T
wenzelm@17059
    40
  val tag_ml: T -> T
wenzelm@17059
    41
end;
wenzelm@17059
    42
wenzelm@17059
    43
structure OuterKeyword: OUTER_KEYWORD =
wenzelm@17059
    44
struct
wenzelm@17059
    45
wenzelm@17059
    46
(* keyword classification *)
wenzelm@17059
    47
wenzelm@17059
    48
datatype T = Keyword of string * string list;
wenzelm@17059
    49
wenzelm@17059
    50
fun kind s = Keyword (s, []);
wenzelm@17059
    51
fun kind_of (Keyword (s, _)) = s;
wenzelm@17059
    52
wenzelm@17059
    53
wenzelm@17059
    54
(* kinds *)
wenzelm@17059
    55
wenzelm@17059
    56
val control = kind "control";
wenzelm@17059
    57
val diag = kind "diag";
wenzelm@17059
    58
val thy_begin = kind "theory-begin";
wenzelm@17059
    59
val thy_switch = kind "theory-switch";
wenzelm@17059
    60
val thy_end = kind "theory-end";
wenzelm@17059
    61
val thy_heading = kind "theory-heading";
wenzelm@17059
    62
val thy_decl = kind "theory-decl";
wenzelm@17059
    63
val thy_script = kind "theory-script";
wenzelm@17059
    64
val thy_goal = kind "theory-goal";
wenzelm@17059
    65
val qed = kind "qed";
wenzelm@17059
    66
val qed_block = kind "qed-block";
wenzelm@17059
    67
val qed_global = kind "qed-global";
wenzelm@17059
    68
val prf_heading = kind "proof-heading";
wenzelm@17059
    69
val prf_goal = kind "proof-goal";
wenzelm@17059
    70
val prf_block = kind "proof-block";
wenzelm@17059
    71
val prf_open = kind "proof-open";
wenzelm@17059
    72
val prf_close = kind "proof-close";
wenzelm@17059
    73
val prf_chain = kind "proof-chain";
wenzelm@17059
    74
val prf_decl = kind "proof-decl";
wenzelm@17059
    75
val prf_asm = kind "proof-asm";
wenzelm@17059
    76
val prf_asm_goal = kind "proof-asm-goal";
wenzelm@17059
    77
val prf_script = kind "proof-script";
wenzelm@17059
    78
wenzelm@17059
    79
val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
wenzelm@17059
    80
  thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
wenzelm@17059
    81
  prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
wenzelm@17059
    82
wenzelm@17059
    83
wenzelm@17059
    84
(* tags *)
wenzelm@17059
    85
haftmann@17270
    86
fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
wenzelm@17059
    87
wenzelm@17059
    88
fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
wenzelm@17059
    89
fun tags_of (Keyword (_, ts)) = ts;
wenzelm@17059
    90
wenzelm@17059
    91
val tag_theory = tag "theory";
wenzelm@17059
    92
val tag_proof = tag "proof";
wenzelm@17059
    93
val tag_ml = tag "ML";
wenzelm@17059
    94
wenzelm@17059
    95
end;