# HG changeset patch
# User wenzelm
# Date 1552333624 -3600
# Node ID 18a61caf5e68f4f4a724a462b3e614789fd3f393
# Parent  27cf4287de43cc0112be6e664e94ba0c2a16da01
support for document meta data in PIDE and RDF;

diff -r 27cf4287de43 -r 18a61caf5e68 src/Pure/General/rdf.scala
--- a/src/Pure/General/rdf.scala	Mon Mar 11 19:14:21 2019 +0100
+++ b/src/Pure/General/rdf.scala	Mon Mar 11 20:47:04 2019 +0100
@@ -84,4 +84,15 @@
     val date: String = dc("date")
     val description: String = dc("description")
   }
+
+  private val meta_data_table =
+    Map(
+      Markup.META_TITLE -> Property.title,
+      Markup.META_CREATOR -> Property.creator,
+      Markup.META_CONTRIBUTOR -> Property.contributor,
+      Markup.META_DATE -> Property.date,
+      Markup.META_DESCRIPTION -> Property.description)
+
+  def meta_data(props: Properties.T): Properties.T =
+    props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) })
 }
diff -r 27cf4287de43 -r 18a61caf5e68 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Mar 11 19:14:21 2019 +0100
+++ b/src/Pure/PIDE/rendering.scala	Mon Mar 11 20:47:04 2019 +0100
@@ -208,6 +208,10 @@
 
   val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
 
+  val meta_data_elements =
+    Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR,
+      Markup.META_DATE, Markup.META_DESCRIPTION)
+
   val markdown_elements =
     Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
       Markup.Markdown_Bullet.name)
@@ -675,4 +679,19 @@
       {
         case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None
       }).headOption.flatMap(_.info)
+
+
+  /* meta data */
+
+  def meta_data(range: Text.Range): Properties.T =
+  {
+    val results =
+      snapshot.cumulate[Properties.T](range, Nil, Rendering.meta_data_elements, _ =>
+        {
+          case (res, Text.Info(_, elem)) =>
+            val plain_text = XML.content(elem)
+            Some((elem.name -> plain_text) :: res)
+        })
+    Library.distinct(results.flatMap(_.info.reverse))
+  }
 }