system option for default command tags;

--- a/etc/options	Tue Dec 05 15:19:32 2017 +0100
+++ b/etc/options	Tue Dec 05 15:29:37 2017 +0100
@@ -11,6 +11,8 @@
   -- "document output directory (default within $ISABELLE_BROWSER_INFO tree)"
 option document_variants : string = "document"
   -- "alternative document variants (separated by colons)"
+option document_tags : string = ""
+  -- "default command tags (separated by commas)"
 
 option thy_output_display : bool = false
   -- "indicate output as multi-line display-style material"

--- a/src/Pure/ROOT.ML	Tue Dec 05 15:19:32 2017 +0100
+++ b/src/Pure/ROOT.ML	Tue Dec 05 15:29:37 2017 +0100
@@ -280,6 +280,7 @@
 (*theory documents*)
 ML_file "Thy/term_style.ML";
 ML_file "Isar/outer_syntax.ML";
+ML_file "ML/ml_antiquotations.ML";
 ML_file "Thy/thy_output.ML";
 ML_file "Thy/document_antiquotations.ML";
 ML_file "General/graph_display.ML";
@@ -311,7 +312,6 @@
 subsection "Miscellaneous tools and packages for Pure Isabelle";
 
 ML_file "ML/ml_pp.ML";
-ML_file "ML/ml_antiquotations.ML";
 ML_file "ML/ml_thms.ML";
 ML_file "ML/ml_file.ML";
 

--- a/src/Pure/Thy/thy_output.ML	Tue Dec 05 15:19:32 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Dec 05 15:29:37 2017 +0100
@@ -314,7 +314,8 @@
 
 in
 
-fun present_span keywords span state state' (tag_stack, active_tag, newline, buffer, present_cont) =
+fun present_span keywords document_tags span state state'
+    (tag_stack, active_tag, newline, buffer, present_cont) =
   let
     val present = fold (fn (tok, (flag, 0)) =>
         Buffer.add (output_token state' tok)
@@ -332,7 +333,7 @@
       if is_some tag' then tag'
       else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE
       else
-        (case Keyword.command_tags keywords cmd_name of
+        (case Keyword.command_tags keywords cmd_name @ document_tags of
           default_tag :: _ => SOME default_tag
         | [] =>
             if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state
@@ -486,8 +487,10 @@
 
     (* present commands *)
 
+    val document_tags = space_explode "," (Options.default_string @{system_option document_tags});
+
     fun present_command tr span st st' =
-      Toplevel.setmp_thread_position tr (present_span keywords span st st');
+      Toplevel.setmp_thread_position tr (present_span keywords document_tags span st st');
 
     fun present _ [] = I
       | present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest;