src/Pure/Isar/outer_keyword.ML
author wenzelm
Thu Aug 07 13:45:03 2008 +0200 (2008-08-07)
changeset 27768 398c64b2acef
parent 27526 69618a03b6f7
child 27805 2e533bcd1343
permissions -rw-r--r--
adapted Scan.extend_lexicon/merge_lexicons;
     1 (*  Title:      Pure/Isar/outer_keyword.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Isar command keyword classification and global keyword tables.
     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   val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
    42   val is_keyword: string -> bool
    43   val dest_keywords: unit -> string list
    44   val dest_commands: unit -> string list
    45   val command_keyword: string -> T option
    46   val command_tags: string -> string list
    47   val report: unit -> unit
    48   val keyword: string -> unit
    49   val command: string -> T -> unit
    50   val is_theory: string -> bool
    51   val is_proof: string -> bool
    52   val is_diag: string -> bool
    53 end;
    54 
    55 structure OuterKeyword: OUTER_KEYWORD =
    56 struct
    57 
    58 (** keyword classification **)
    59 
    60 datatype T = Keyword of string * string list;
    61 
    62 fun kind s = Keyword (s, []);
    63 fun kind_of (Keyword (s, _)) = s;
    64 
    65 
    66 (* kinds *)
    67 
    68 val control = kind "control";
    69 val diag = kind "diag";
    70 val thy_begin = kind "theory-begin";
    71 val thy_switch = kind "theory-switch";
    72 val thy_end = kind "theory-end";
    73 val thy_heading = kind "theory-heading";
    74 val thy_decl = kind "theory-decl";
    75 val thy_script = kind "theory-script";
    76 val thy_goal = kind "theory-goal";
    77 val qed = kind "qed";
    78 val qed_block = kind "qed-block";
    79 val qed_global = kind "qed-global";
    80 val prf_heading = kind "proof-heading";
    81 val prf_goal = kind "proof-goal";
    82 val prf_block = kind "proof-block";
    83 val prf_open = kind "proof-open";
    84 val prf_close = kind "proof-close";
    85 val prf_chain = kind "proof-chain";
    86 val prf_decl = kind "proof-decl";
    87 val prf_asm = kind "proof-asm";
    88 val prf_asm_goal = kind "proof-asm-goal";
    89 val prf_script = kind "proof-script";
    90 
    91 val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
    92   thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    93   prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
    94 
    95 
    96 (* tags *)
    97 
    98 fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
    99 
   100 fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
   101 fun tags_of (Keyword (_, ts)) = ts;
   102 
   103 val tag_theory = tag "theory";
   104 val tag_proof = tag "proof";
   105 val tag_ml = tag "ML";
   106 
   107 
   108 
   109 (** global keyword tables **)
   110 
   111 local
   112 
   113 val global_commands = ref (Symtab.empty: T Symtab.table);
   114 val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
   115 
   116 in
   117 
   118 fun get_commands () = CRITICAL (fn () => ! global_commands);
   119 fun get_lexicons () = CRITICAL (fn () => ! global_lexicons);
   120 
   121 fun change_commands f = CRITICAL (fn () => change global_commands f);
   122 fun change_lexicons f = CRITICAL (fn () => change global_lexicons f);
   123 
   124 end;
   125 
   126 
   127 (* lookup *)
   128 
   129 fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
   130 fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
   131 
   132 fun dest_commands () = Symtab.keys (get_commands ());
   133 fun command_keyword name = Symtab.lookup (get_commands ()) name;
   134 fun command_tags name = these (Option.map tags_of (command_keyword name));
   135 
   136 
   137 (* report *)
   138 
   139 fun report_keyword name =
   140   Pretty.mark (Markup.keyword_decl name)
   141     (Pretty.str ("Outer syntax keyword: " ^ quote name));
   142 
   143 fun report_command (name, kind) =
   144   Pretty.mark (Markup.command_decl name (kind_of kind))
   145     (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
   146 
   147 fun report () =
   148   let val (keywords, commands) = CRITICAL (fn () =>
   149     (dest_keywords (), Symtab.dest (get_commands ())))
   150   in map report_keyword keywords @ map report_command commands end
   151   |> Pretty.chunks |> Pretty.writeln;
   152 
   153 
   154 (* augment tables *)
   155 
   156 fun keyword name =
   157  (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
   158   Pretty.writeln (report_keyword name));
   159 
   160 fun command name kind =
   161  (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   162   change_commands (Symtab.update (name, kind));
   163   Pretty.writeln (report_command (name, kind)));
   164 
   165 
   166 (* overall category *)
   167 
   168 fun command_category ks name =
   169   (case command_keyword name of
   170     NONE => false
   171   | SOME k => member (op =) ks (kind_of k));
   172 
   173 val is_theory = command_category
   174   (map kind_of [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal]);
   175 
   176 val is_proof = command_category
   177   (map kind_of [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
   178     prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]);
   179 
   180 val is_diag = command_category [kind_of diag];
   181 
   182 end;