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