# 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)