# 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