# 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)) + } }