clarified: more uniform keyword_tags;
authorwenzelm
Tue, 26 Jun 2018 17:25:57 +0200
changeset 68509 0f91ff642658
parent 68508 0799fb9c3b9c
child 68510 795f39bfe4e1
clarified: more uniform keyword_tags;
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