clarified: more uniform keyword_tags;
authorwenzelm
Tue Jun 26 17:25:57 2018 +0200 (14 months ago)
changeset 685090f91ff642658
parent 68508 0799fb9c3b9c
child 68510 795f39bfe4e1
clarified: more uniform keyword_tags;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Jun 26 17:24:13 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Jun 26 17:25:57 2018 +0200
     1.3 @@ -263,7 +263,9 @@
     1.4        let
     1.5          val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag));
     1.6  
     1.7 -        val keyword_tags = Keyword.command_tags keywords cmd_name;
     1.8 +        val keyword_tags =
     1.9 +          if cmd_name = "end" andalso Toplevel.is_end_theory state' then ["theory"]
    1.10 +          else Keyword.command_tags keywords cmd_name;
    1.11          val command_tags =
    1.12            the_list (AList.lookup (op =) document_tags_command cmd_name) @
    1.13            map_filter (AList.lookup (op =) document_tags_category) keyword_tags @
    1.14 @@ -271,7 +273,6 @@
    1.15  
    1.16          val active_tag' =
    1.17            if is_some tag' then tag'
    1.18 -          else if cmd_name = "end" andalso Toplevel.is_end_theory state' then SOME "theory"
    1.19            else
    1.20              (case command_tags of
    1.21                default_tag :: _ => SOME default_tag