system option for default command tags;
authorwenzelm
Tue Dec 05 15:29:37 2017 +0100 (7 months ago)
changeset 6713882283d52b4d6
parent 67137 f2384ad1dff4
child 67139 8fe0aba577af
system option for default command tags;
etc/options
src/Pure/ROOT.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/etc/options	Tue Dec 05 15:19:32 2017 +0100
     1.2 +++ b/etc/options	Tue Dec 05 15:29:37 2017 +0100
     1.3 @@ -11,6 +11,8 @@
     1.4    -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
     1.5  option document_variants : string = "document"
     1.6    -- "alternative document variants (separated by colons)"
     1.7 +option document_tags : string = ""
     1.8 +  -- "default command tags (separated by commas)"
     1.9  
    1.10  option thy_output_display : bool = false
    1.11    -- "indicate output as multi-line display-style material"
     2.1 --- a/src/Pure/ROOT.ML	Tue Dec 05 15:19:32 2017 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Tue Dec 05 15:29:37 2017 +0100
     2.3 @@ -280,6 +280,7 @@
     2.4  (*theory documents*)
     2.5  ML_file "Thy/term_style.ML";
     2.6  ML_file "Isar/outer_syntax.ML";
     2.7 +ML_file "ML/ml_antiquotations.ML";
     2.8  ML_file "Thy/thy_output.ML";
     2.9  ML_file "Thy/document_antiquotations.ML";
    2.10  ML_file "General/graph_display.ML";
    2.11 @@ -311,7 +312,6 @@
    2.12  subsection "Miscellaneous tools and packages for Pure Isabelle";
    2.13  
    2.14  ML_file "ML/ml_pp.ML";
    2.15 -ML_file "ML/ml_antiquotations.ML";
    2.16  ML_file "ML/ml_thms.ML";
    2.17  ML_file "ML/ml_file.ML";
    2.18  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Tue Dec 05 15:19:32 2017 +0100
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Dec 05 15:29:37 2017 +0100
     3.3 @@ -314,7 +314,8 @@
     3.4  
     3.5  in
     3.6  
     3.7 -fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
     3.8 +fun present_span keywords document_tags span state state'
     3.9 +    (tag_stack, active_tag, newline, buffer, present_cont) =
    3.10    let
    3.11      val present = fold (fn (tok, (flag, 0)) =>
    3.12          Buffer.add (output_token state' tok)
    3.13 @@ -332,7 +333,7 @@
    3.14        if is_some tag' then tag'
    3.15        else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
    3.16        else
    3.17 -        (case Keyword.command_tags keywords cmd_name of
    3.18 +        (case Keyword.command_tags keywords cmd_name @ document_tags of
    3.19            default_tag :: _ => SOME default_tag
    3.20          | [] =>
    3.21              if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
    3.22 @@ -486,8 +487,10 @@
    3.23  
    3.24      (* present commands *)
    3.25  
    3.26 +    val document_tags = space_explode "," (Options.default_string @{system_option document_tags});
    3.27 +
    3.28      fun present_command tr span st st' =
    3.29 -      Toplevel.setmp_thread_position tr (present_span keywords span st st');
    3.30 +      Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
    3.31  
    3.32      fun present _ [] = I
    3.33        | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;