src/Pure/Thy/thy_output.ML
changeset 67138 82283d52b4d6
parent 66021 08ab52fb9db5
child 67147 dea94b1aabc3
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Dec 05 15:19:32 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Dec 05 15:29:37 2017 +0100
     1.3 @@ -314,7 +314,8 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
     1.8 +fun present_span keywords document_tags span state state'
     1.9 +    (tag_stack, active_tag, newline, buffer, present_cont) =
    1.10    let
    1.11      val present = fold (fn (tok, (flag, 0)) =>
    1.12          Buffer.add (output_token state' tok)
    1.13 @@ -332,7 +333,7 @@
    1.14        if is_some tag' then tag'
    1.15        else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
    1.16        else
    1.17 -        (case Keyword.command_tags keywords cmd_name of
    1.18 +        (case Keyword.command_tags keywords cmd_name @ document_tags of
    1.19            default_tag :: _ => SOME default_tag
    1.20          | [] =>
    1.21              if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
    1.22 @@ -486,8 +487,10 @@
    1.23  
    1.24      (* present commands *)
    1.25  
    1.26 +    val document_tags = space_explode "," (Options.default_string @{system_option document_tags});
    1.27 +
    1.28      fun present_command tr span st st' =
    1.29 -      Toplevel.setmp_thread_position tr (present_span keywords span st st');
    1.30 +      Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
    1.31  
    1.32      fun present _ [] = I
    1.33        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;