# HG changeset patch # User wenzelm # Date 1635086634 -7200 # Node ID 40910c47d7a1ce1ead91c6158e5e024b67b528a7 # Parent 8e0f0317e266c991dc5f57e36522ae1dfef32601 tuned signature; diff -r 8e0f0317e266 -r 40910c47d7a1 src/HOL/Tools/Mirabelle/mirabelle.ML --- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Oct 24 16:38:13 2021 +0200 +++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sun Oct 24 16:43:54 2021 +0200 @@ -39,7 +39,7 @@ let val thy = \<^theory>; val ctxt = Proof_Context.init_global thy - val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords thy) + val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords thy) fun read_actions () = Parse.read_embedded ctxt keywords (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params)) diff -r 8e0f0317e266 -r 40910c47d7a1 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Sun Oct 24 16:38:13 2021 +0200 +++ b/src/Pure/Isar/keyword.ML Sun Oct 24 16:43:54 2021 +0200 @@ -47,12 +47,12 @@ 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 * Position.T) * spec) list -> keywords -> keywords val add_minor_keywords: string list -> keywords -> keywords val add_major_keywords: string list -> keywords -> keywords + val no_major_keywords: keywords -> keywords val is_keyword: keywords -> string -> bool val is_command: keywords -> string -> bool val is_literal: keywords -> string -> bool @@ -171,9 +171,6 @@ fun map_keywords f (Keywords {minor, major, commands}) = make_keywords (f (minor, major, commands)); -val no_command_keywords = - map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); - (* build keywords *) @@ -207,6 +204,9 @@ val add_major_keywords = add_keywords o map (fn name => ((name, Position.none), (diag, []))); +val no_major_keywords = + map_keywords (fn (minor, _, _) => (minor, Scan.empty_lexicon, Symtab.empty)); + (* keyword status *) diff -r 8e0f0317e266 -r 40910c47d7a1 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Sun Oct 24 16:38:13 2021 +0200 +++ b/src/Pure/Isar/method.ML Sun Oct 24 16:43:54 2021 +0200 @@ -740,7 +740,7 @@ in (text, src2) end; fun read_closure_input ctxt = - let val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords' ctxt) + let val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt) in Parse.read_embedded ctxt keywords (Scan.many Token.not_eof) #> read_closure ctxt end; val text_closure = diff -r 8e0f0317e266 -r 40910c47d7a1 src/Pure/Isar/parse.ML --- a/src/Pure/Isar/parse.ML Sun Oct 24 16:38:13 2021 +0200 +++ b/src/Pure/Isar/parse.ML Sun Oct 24 16:43:54 2021 +0200 @@ -517,7 +517,7 @@ fun tokenize keywords = Token.tokenize keywords {strict = true} #> filter Token.is_proper; fun read_antiq keywords scan (syms, pos) = - (case Scan.read Token.stopper scan (tokenize (Keyword.no_command_keywords keywords) syms) of + (case Scan.read Token.stopper scan (tokenize (Keyword.no_major_keywords keywords) syms) of SOME res => res | NONE => error ("Malformed antiquotation" ^ Position.here pos)); diff -r 8e0f0317e266 -r 40910c47d7a1 src/Pure/ML/ml_antiquotations.ML --- a/src/Pure/ML/ml_antiquotations.ML Sun Oct 24 16:38:13 2021 +0200 +++ b/src/Pure/ML/ml_antiquotations.ML Sun Oct 24 16:43:54 2021 +0200 @@ -252,7 +252,7 @@ fun make_keywords ctxt = Thy_Header.get_keywords' ctxt - |> Keyword.no_command_keywords + |> Keyword.no_major_keywords |> Keyword.add_major_keywords ["typ", "term", "prop", "ctyp", "cterm", "cprop"]; val parse_inst = diff -r 8e0f0317e266 -r 40910c47d7a1 src/Pure/Thy/document_marker.ML --- a/src/Pure/Thy/document_marker.ML Sun Oct 24 16:38:13 2021 +0200 +++ b/src/Pure/Thy/document_marker.ML Sun Oct 24 16:43:54 2021 +0200 @@ -58,7 +58,7 @@ val _ = Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups Comment.Marker)); - val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords' ctxt); + val keywords = Keyword.no_major_keywords (Thy_Header.get_keywords' ctxt); val body = Symbol_Pos.cartouche_content syms; val markers = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body)