report document tags as seen in the text (not the active tag of Thy_Output.present_thy);

--- a/src/Pure/PIDE/markup.ML	Fri Apr 12 17:09:21 2019 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Apr 12 19:48:29 2019 +0200
@@ -132,6 +132,7 @@
   val plain_textN: string val plain_text: T
   val paragraphN: string val paragraph: T
   val text_foldN: string val text_fold: T
+  val document_tagN: string val document_tag: string -> T
   val markdown_paragraphN: string val markdown_paragraph: T
   val markdown_itemN: string val markdown_item: T
   val markdown_bulletN: string val markdown_bullet: int -> T
@@ -512,17 +513,16 @@
 val document_antiquotation_optionN = "document_antiquotation_option";
 
 
-(* text kind *)
+(* document text *)
 
 val (raw_textN, raw_text) = markup_elem "raw_text";
 val (plain_textN, plain_text) = markup_elem "plain_text";
 
-
-(* text structure *)
-
 val (paragraphN, paragraph) = markup_elem "paragraph";
 val (text_foldN, text_fold) = markup_elem "text_fold";
 
+val (document_tagN, document_tag) = markup_string "document_tag" nameN;
+
 
 (* Markdown document structure *)
 

--- a/src/Pure/PIDE/markup.scala	Fri Apr 12 17:09:21 2019 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Apr 12 19:48:29 2019 +0200
@@ -307,17 +307,27 @@
   val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
 
 
-  /* text kind */
+  /* document text */
 
   val RAW_TEXT = "raw_text"
   val PLAIN_TEXT = "plain_text"
 
-
-  /* text structure */
-
   val PARAGRAPH = "paragraph"
   val TEXT_FOLD = "text_fold"
 
+  object Document_Tag
+  {
+    val ELEMENT = "document_tag"
+    val IMPORTANT = "important"
+    val UNIMPORTANT = "unimportant"
+
+    def unapply(markup: Markup): Option[String] =
+      markup match {
+        case Markup(ELEMENT, Name(name)) => Some(name)
+        case _ => None
+      }
+  }
+
 
   /* Markdown document structure */
 

--- a/src/Pure/PIDE/rendering.scala	Fri Apr 12 17:09:21 2019 +0200
+++ b/src/Pure/PIDE/rendering.scala	Fri Apr 12 19:48:29 2019 +0200
@@ -216,6 +216,9 @@
     Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR,
       Markup.META_DATE, Markup.META_DESCRIPTION, Markup.META_LICENSE)
 
+  val document_tag_elements =
+    Markup.Elements(Markup.Document_Tag.ELEMENT)
+
   val markdown_elements =
     Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
       Markup.Markdown_Bullet.name)
@@ -698,4 +701,18 @@
         })
     Library.distinct(results.flatMap(_.info.reverse))
   }
+
+
+  /* document tags */
+
+  def document_tags(range: Text.Range): List[String] =
+  {
+    val results =
+      snapshot.cumulate[List[String]](range, Nil, Rendering.document_tag_elements, _ =>
+        {
+          case (res, Text.Info(_, XML.Elem(Markup.Document_Tag(name), _))) => Some(name :: res)
+          case _ => None
+        })
+    Library.distinct(results.flatMap(_.info.reverse))
+  }
 }

--- a/src/Pure/Thy/document_marker.ML	Fri Apr 12 17:09:21 2019 +0200
+++ b/src/Pure/Thy/document_marker.ML	Fri Apr 12 19:48:29 2019 +0200
@@ -83,7 +83,11 @@
         then Document_Source.Command
         else Document_Source.Proof;
       val tag = Scan.optional Document_Source.tag_scope scope0 -- Document_Source.tag_name >> swap;
-    in Scan.lift tag end);
+    in Scan.lift (Parse.position tag) end);
+
+fun update_tags (tag as (name, _), pos) ctxt =
+ (Context_Position.report ctxt pos (Markup.document_tag name);
+  Document_Source.update_tags tag ctxt);
 
 
 (* concrete markers *)
@@ -93,7 +97,7 @@
 
 val _ =
   Theory.setup
-    (setup (Binding.make ("tag", \<^here>)) parse_tag Document_Source.update_tags #>
+    (setup (Binding.make ("tag", \<^here>)) parse_tag update_tags #>
      setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
      setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
      setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>