support for document meta data in PIDE and RDF;
authorwenzelm
Mon Mar 11 20:47:04 2019 +0100 (6 weeks ago ago)
changeset 7008118a61caf5e68
parent 70080 27cf4287de43
child 70082 20b32ade0024
support for document meta data in PIDE and RDF;
src/Pure/General/rdf.scala
src/Pure/PIDE/rendering.scala
     1.1 --- a/src/Pure/General/rdf.scala	Mon Mar 11 19:14:21 2019 +0100
     1.2 +++ b/src/Pure/General/rdf.scala	Mon Mar 11 20:47:04 2019 +0100
     1.3 @@ -84,4 +84,15 @@
     1.4      val date: String = dc("date")
     1.5      val description: String = dc("description")
     1.6    }
     1.7 +
     1.8 +  private val meta_data_table =
     1.9 +    Map(
    1.10 +      Markup.META_TITLE -> Property.title,
    1.11 +      Markup.META_CREATOR -> Property.creator,
    1.12 +      Markup.META_CONTRIBUTOR -> Property.contributor,
    1.13 +      Markup.META_DATE -> Property.date,
    1.14 +      Markup.META_DESCRIPTION -> Property.description)
    1.15 +
    1.16 +  def meta_data(props: Properties.T): Properties.T =
    1.17 +    props.flatMap({ case (a, b) => meta_data_table.get(a).map((_, b)) })
    1.18  }
     2.1 --- a/src/Pure/PIDE/rendering.scala	Mon Mar 11 19:14:21 2019 +0100
     2.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Mar 11 20:47:04 2019 +0100
     2.3 @@ -208,6 +208,10 @@
     2.4  
     2.5    val antiquoted_elements = Markup.Elements(Markup.ANTIQUOTED)
     2.6  
     2.7 +  val meta_data_elements =
     2.8 +    Markup.Elements(Markup.META_TITLE, Markup.META_CREATOR, Markup.META_CONTRIBUTOR,
     2.9 +      Markup.META_DATE, Markup.META_DESCRIPTION)
    2.10 +
    2.11    val markdown_elements =
    2.12      Markup.Elements(Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name,
    2.13        Markup.Markdown_Bullet.name)
    2.14 @@ -675,4 +679,19 @@
    2.15        {
    2.16          case (res, info) => if (res.isEmpty) Some(Some(info.range)) else None
    2.17        }).headOption.flatMap(_.info)
    2.18 +
    2.19 +
    2.20 +  /* meta data */
    2.21 +
    2.22 +  def meta_data(range: Text.Range): Properties.T =
    2.23 +  {
    2.24 +    val results =
    2.25 +      snapshot.cumulate[Properties.T](range, Nil, Rendering.meta_data_elements, _ =>
    2.26 +        {
    2.27 +          case (res, Text.Info(_, elem)) =>
    2.28 +            val plain_text = XML.content(elem)
    2.29 +            Some((elem.name -> plain_text) :: res)
    2.30 +        })
    2.31 +    Library.distinct(results.flatMap(_.info.reverse))
    2.32 +  }
    2.33  }