# HG changeset patch
# User wenzelm
# Date 1530026757 -7200
# Node ID 0f91ff642658ca2a241862f20d9ca3e6d9d64b6e
# Parent  0799fb9c3b9c704fc115b8692aa9cf3365ae2a14
clarified: more uniform keyword_tags;

diff -r 0799fb9c3b9c -r 0f91ff642658 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Jun 26 17:24:13 2018 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Jun 26 17:25:57 2018 +0200
@@ -263,7 +263,9 @@
       let
         val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
 
-        val keyword_tags = Keyword.command_tags keywords cmd_name;
+        val keyword_tags =
+          if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
+          else Keyword.command_tags keywords cmd_name;
         val command_tags =
           the_list (AList.lookup (op =) document_tags_command cmd_name) @
           map_filter (AList.lookup (op =) document_tags_category) keyword_tags @
@@ -271,7 +273,6 @@
 
         val active_tag' =
           if is_some tag' then tag'
-          else if cmd_name = "end" andalso Toplevel.is_end_theory state' then SOME "theory"
           else
             (case command_tags of
               default_tag :: _ => SOME default_tag