diff -r cf47382db395 -r 23d0ffd48006 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Fri Nov 07 16:22:25 2014 +0100 +++ b/src/Pure/Isar/keyword.ML Fri Nov 07 16:36:55 2014 +0100 @@ -6,43 +6,38 @@ signature KEYWORD = sig - type T - val kind_of: T -> string - val kind_files_of: T -> string * string list - val diag: T - val heading: T - val thy_begin: T - val thy_end: T - val thy_decl: T - val thy_decl_block: T - val thy_load: T - val thy_goal: T - val qed: T - val qed_script: T - val qed_block: T - val qed_global: T - val prf_goal: T - val prf_block: T - val prf_open: T - val prf_close: T - val prf_chain: T - val prf_decl: T - val prf_asm: T - val prf_asm_goal: T - val prf_asm_goal_script: T - val prf_script: T + val diag: string + val heading: string + val thy_begin: string + val thy_end: string + val thy_decl: string + val thy_decl_block: string + val thy_load: string + val thy_goal: string + val qed: string + val qed_script: string + val qed_block: string + val qed_global: string + val prf_goal: string + val prf_block: string + val prf_open: string + val prf_close: string + val prf_chain: string + val prf_decl: string + val prf_asm: string + val prf_asm_goal: string + val prf_asm_goal_script: string + val prf_script: string type spec = (string * string list) * string list - val check_spec: spec -> T - val command_spec: (string * spec) * Position.T -> (string * T) * Position.T type keywords val minor_keywords: keywords -> Scan.lexicon val major_keywords: keywords -> Scan.lexicon val no_command_keywords: keywords -> keywords val empty_keywords: keywords val merge_keywords: keywords * keywords -> keywords - val add_keywords: string * T option -> keywords -> keywords - val is_keyword: keywords -> string -> bool - val command_keyword: keywords -> string -> T option + val add_keywords: (string * spec option) list -> keywords -> keywords + val is_literal: keywords -> string -> bool + val is_command: keywords -> string -> bool val command_files: keywords -> string -> Path.T -> Path.T list val command_tags: keywords -> string -> string list val is_diag: keywords -> string -> bool @@ -58,8 +53,6 @@ val is_qed: keywords -> string -> bool val is_qed_global: keywords -> string -> bool val is_printed: keywords -> string -> bool - val define: string * T option -> unit - val get_keywords: unit -> keywords end; structure Keyword: KEYWORD = @@ -69,57 +62,50 @@ (* kinds *) -datatype T = Keyword of +val diag = "diag"; +val heading = "heading"; +val thy_begin = "thy_begin"; +val thy_end = "thy_end"; +val thy_decl = "thy_decl"; +val thy_decl_block = "thy_decl_block"; +val thy_load = "thy_load"; +val thy_goal = "thy_goal"; +val qed = "qed"; +val qed_script = "qed_script"; +val qed_block = "qed_block"; +val qed_global = "qed_global"; +val prf_goal = "prf_goal"; +val prf_block = "prf_block"; +val prf_open = "prf_open"; +val prf_close = "prf_close"; +val prf_chain = "prf_chain"; +val prf_decl = "prf_decl"; +val prf_asm = "prf_asm"; +val prf_asm_goal = "prf_asm_goal"; +val prf_asm_goal_script = "prf_asm_goal_script"; +val prf_script = "prf_script"; + +val kinds = + [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal, + qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, + prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script]; + + +(* specifications *) + +type T = {kind: string, files: string list, (*extensions of embedded files*) tags: string list}; -fun kind s = Keyword {kind = s, files = [], tags = []}; -fun kind_of (Keyword {kind, ...}) = kind; -fun kind_files_of (Keyword {kind, files, ...}) = (kind, files); - -val diag = kind "diag"; -val heading = kind "heading"; -val thy_begin = kind "thy_begin"; -val thy_end = kind "thy_end"; -val thy_decl = kind "thy_decl"; -val thy_decl_block = kind "thy_decl_block"; -val thy_load = kind "thy_load"; -val thy_goal = kind "thy_goal"; -val qed = kind "qed"; -val qed_script = kind "qed_script"; -val qed_block = kind "qed_block"; -val qed_global = kind "qed_global"; -val prf_goal = kind "prf_goal"; -val prf_block = kind "prf_block"; -val prf_open = kind "prf_open"; -val prf_close = kind "prf_close"; -val prf_chain = kind "prf_chain"; -val prf_decl = kind "prf_decl"; -val prf_asm = kind "prf_asm"; -val prf_asm_goal = kind "prf_asm_goal"; -val prf_asm_goal_script = kind "prf_asm_goal_script"; -val prf_script = kind "prf_script"; - -val kinds = - [diag, heading, thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal, - qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, - prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script] - |> map kind_of; - - -(* specifications *) - type spec = (string * string list) * string list; -fun check_spec ((kind, files), tags) = +fun check_spec ((kind, files), tags) : T = if not (member (op =) kinds kind) then error ("Unknown outer syntax keyword kind " ^ quote kind) - else if not (null files) andalso kind <> kind_of thy_load then + else if not (null files) andalso kind <> thy_load then error ("Illegal specification of files for " ^ quote kind) - else Keyword {kind = kind, files = files, tags = tags}; - -fun command_spec ((name, s), pos) = ((name, check_spec s), pos); + else {kind = kind, files = files, tags = tags}; @@ -158,41 +144,45 @@ Scan.merge_lexicons (major1, major2), Symtab.merge (K true) (commands1, commands2)); -fun add_keywords (name, opt_kind) = map_keywords (fn (minor, major, commands) => - (case opt_kind of - NONE => - let - val minor' = Scan.extend_lexicon (Symbol.explode name) minor; - in (minor', major, commands) end - | SOME kind => - let - val major' = Scan.extend_lexicon (Symbol.explode name) major; - val commands' = Symtab.update (name, kind) commands; - in (minor, major', commands') end)); +val add_keywords = + fold (fn (name, opt_spec) => map_keywords (fn (minor, major, commands) => + (case opt_spec of + NONE => + let + val minor' = Scan.extend_lexicon (Symbol.explode name) minor; + in (minor', major, commands) end + | SOME spec => + let + val kind = check_spec spec; + val major' = Scan.extend_lexicon (Symbol.explode name) major; + val commands' = Symtab.update (name, kind) commands; + in (minor, major', commands') end))); -(* lookup *) +(* lookup keywords *) -fun is_keyword keywords s = +fun is_literal keywords s = let val minor = minor_keywords keywords; val major = major_keywords keywords; val syms = Symbol.explode s; in Scan.is_literal minor syms orelse Scan.is_literal major syms end; +fun is_command (Keywords {commands, ...}) = Symtab.defined commands; + fun command_keyword (Keywords {commands, ...}) = Symtab.lookup commands; fun command_files keywords name path = (case command_keyword keywords name of NONE => [] - | SOME (Keyword {kind, files, ...}) => - if kind <> kind_of thy_load then [] + | SOME {kind, files, ...} => + if kind <> thy_load then [] else if null files then [path] else map (fn ext => Path.ext ext path) files); fun command_tags keywords name = (case command_keyword keywords name of - SOME (Keyword {tags, ...}) => tags + SOME {tags, ...} => tags | NONE => []); @@ -200,11 +190,11 @@ fun command_category ks = let - val tab = Symtab.make_set (map kind_of ks); + val tab = Symtab.make_set ks; fun pred keywords name = (case command_keyword keywords name of NONE => false - | SOME k => Symtab.defined tab (kind_of k)); + | SOME {kind, ...} => Symtab.defined tab kind); in pred end; val is_diag = command_category [diag]; @@ -236,16 +226,5 @@ fun is_printed keywords = is_theory_goal keywords orf is_proof keywords; - - -(** global state **) - -local val global_keywords = Unsynchronized.ref empty_keywords in - -fun define decl = CRITICAL (fn () => Unsynchronized.change global_keywords (add_keywords decl)); -fun get_keywords () = ! global_keywords; - end; -end; -