src/Pure/Isar/keyword.ML
author wenzelm
Mon Nov 14 16:52:19 2011 +0100 (2011-11-14 ago)
changeset 45488 6d71d9e52369
parent 40397 4ad71312a192
child 45666 d83797ef0d2d
permissions -rw-r--r--
pass positions for named targets, for formal links in the document model;
     1 (*  Title:      Pure/Isar/keyword.ML
     2     Author:     Makarius
     3 
     4 Isar command keyword classification and global keyword tables.
     5 *)
     6 
     7 signature KEYWORD =
     8 sig
     9   type T
    10   val kind_of: T -> string
    11   val control: T
    12   val diag: T
    13   val thy_begin: T
    14   val thy_switch: T
    15   val thy_end: T
    16   val thy_heading: T
    17   val thy_decl: T
    18   val thy_script: T
    19   val thy_goal: T
    20   val thy_schematic_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 keyword_statusN: string
    48   val status: unit -> unit
    49   val keyword: string -> unit
    50   val command: string -> T -> unit
    51   val is_diag: string -> bool
    52   val is_control: string -> bool
    53   val is_regular: string -> bool
    54   val is_heading: string -> bool
    55   val is_theory_begin: string -> bool
    56   val is_theory: string -> bool
    57   val is_proof: string -> bool
    58   val is_theory_goal: string -> bool
    59   val is_proof_goal: string -> bool
    60   val is_schematic_goal: string -> bool
    61   val is_qed: string -> bool
    62   val is_qed_global: string -> bool
    63 end;
    64 
    65 structure Keyword: KEYWORD =
    66 struct
    67 
    68 (** keyword classification **)
    69 
    70 datatype T = Keyword of string * string list;
    71 
    72 fun kind s = Keyword (s, []);
    73 fun kind_of (Keyword (s, _)) = s;
    74 
    75 
    76 (* kinds *)
    77 
    78 val control = kind "control";
    79 val diag = kind "diag";
    80 val thy_begin = kind "theory-begin";
    81 val thy_switch = kind "theory-switch";
    82 val thy_end = kind "theory-end";
    83 val thy_heading = kind "theory-heading";
    84 val thy_decl = kind "theory-decl";
    85 val thy_script = kind "theory-script";
    86 val thy_goal = kind "theory-goal";
    87 val thy_schematic_goal = kind "theory-schematic-goal";
    88 val qed = kind "qed";
    89 val qed_block = kind "qed-block";
    90 val qed_global = kind "qed-global";
    91 val prf_heading = kind "proof-heading";
    92 val prf_goal = kind "proof-goal";
    93 val prf_block = kind "proof-block";
    94 val prf_open = kind "proof-open";
    95 val prf_close = kind "proof-close";
    96 val prf_chain = kind "proof-chain";
    97 val prf_decl = kind "proof-decl";
    98 val prf_asm = kind "proof-asm";
    99 val prf_asm_goal = kind "proof-asm-goal";
   100 val prf_script = kind "proof-script";
   101 
   102 val kinds =
   103   [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
   104     thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
   105     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
   106  |> map kind_of;
   107 
   108 
   109 (* tags *)
   110 
   111 fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;
   112 
   113 fun tag t (Keyword (s, ts)) = Keyword (s, update_tags t ts);
   114 fun tags_of (Keyword (_, ts)) = ts;
   115 
   116 val tag_theory = tag "theory";
   117 val tag_proof = tag "proof";
   118 val tag_ml = tag "ML";
   119 
   120 
   121 
   122 (** global keyword tables **)
   123 
   124 local
   125 
   126 val global_commands = Unsynchronized.ref (Symtab.empty: T Symtab.table);
   127 val global_lexicons = Unsynchronized.ref (Scan.empty_lexicon, Scan.empty_lexicon);
   128 
   129 in
   130 
   131 fun get_commands () = ! global_commands;
   132 fun get_lexicons () = ! global_lexicons;
   133 
   134 fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);
   135 fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);
   136 
   137 end;
   138 
   139 
   140 (* lookup *)
   141 
   142 fun is_keyword s = Scan.is_literal (#1 (get_lexicons ())) (Symbol.explode s);
   143 fun dest_keywords () = sort_strings (Scan.dest_lexicon (#1 (get_lexicons ())));
   144 
   145 fun dest_commands () = sort_strings (Symtab.keys (get_commands ()));
   146 fun command_keyword name = Symtab.lookup (get_commands ()) name;
   147 fun command_tags name = these (Option.map tags_of (command_keyword name));
   148 
   149 
   150 (* status *)
   151 
   152 val keyword_statusN = "keyword_status";
   153 
   154 fun status_message s =
   155   Position.setmp_thread_data Position.none
   156     (if print_mode_active keyword_statusN then Output.status else writeln) s;
   157 
   158 fun keyword_status name =
   159   status_message (Markup.markup (Markup.keyword_decl name)
   160     ("Outer syntax keyword: " ^ quote name));
   161 
   162 fun command_status (name, kind) =
   163   status_message (Markup.markup (Markup.command_decl name (kind_of kind))
   164     ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
   165 
   166 fun status () =
   167   let val (keywords, commands) = CRITICAL (fn () =>
   168     (dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
   169   in
   170     List.app keyword_status keywords;
   171     List.app command_status commands
   172   end;
   173 
   174 
   175 (* augment tables *)
   176 
   177 fun keyword name =
   178  (change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
   179   keyword_status name);
   180 
   181 fun command name kind =
   182  (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
   183   change_commands (Symtab.update (name, kind));
   184   command_status (name, kind));
   185 
   186 
   187 (* command categories *)
   188 
   189 fun command_category ks name =
   190   (case command_keyword name of
   191     NONE => false
   192   | SOME k => member (op = o pairself kind_of) ks k);
   193 
   194 val is_diag = command_category [diag];
   195 val is_control = command_category [control];
   196 val is_regular = not o command_category [diag, control];
   197 
   198 val is_heading = command_category [thy_heading, prf_heading];
   199 
   200 val is_theory_begin = command_category [thy_begin];
   201 
   202 val is_theory = command_category
   203   [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
   204 
   205 val is_proof = command_category
   206   [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
   207     prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
   208 
   209 val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
   210 val is_proof_goal = command_category [prf_goal, prf_asm_goal];
   211 val is_schematic_goal = command_category [thy_schematic_goal];
   212 val is_qed = command_category [qed, qed_block];
   213 val is_qed_global = command_category [qed_global];
   214 
   215 end;
   216