markup and document markers for some meta data from "Dublin Core Metadata Element Set";
authorwenzelm
Sun Mar 10 14:19:30 2019 +0100 (3 months ago ago)
changeset 70070be04e9a053a7
parent 70069 6db51f45b5f9
child 70071 cb643a1a5313
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/document_marker.ML
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Mar 10 00:23:52 2019 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Mar 10 14:19:30 2019 +0100
     1.3 @@ -16,6 +16,11 @@
     1.4    val serialN: string
     1.5    val serial_properties: int -> Properties.T
     1.6    val instanceN: string
     1.7 +  val meta_titleN: string val meta_title: T
     1.8 +  val meta_creatorN: string val meta_creator: T
     1.9 +  val meta_contributorN: string val meta_contributor: T
    1.10 +  val meta_dateN: string val meta_date: T
    1.11 +  val meta_descriptionN: string val meta_description: T
    1.12    val languageN: string
    1.13    val symbolsN: string
    1.14    val delimitedN: string
    1.15 @@ -283,6 +288,15 @@
    1.16  val instanceN = "instance";
    1.17  
    1.18  
    1.19 +(* meta data -- see http://dublincore.org/documents/dces *)
    1.20 +
    1.21 +val (meta_titleN, meta_title) = markup_elem "meta_title";
    1.22 +val (meta_creatorN, meta_creator) = markup_elem "meta_creator";
    1.23 +val (meta_contributorN, meta_contributor) = markup_elem "meta_contributor";
    1.24 +val (meta_dateN, meta_date) = markup_elem "meta_date";
    1.25 +val (meta_descriptionN, meta_description) = markup_elem "meta_description";
    1.26 +
    1.27 +
    1.28  (* embedded languages *)
    1.29  
    1.30  val languageN = "language";
     2.1 --- a/src/Pure/PIDE/markup.scala	Sun Mar 10 00:23:52 2019 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Sun Mar 10 14:19:30 2019 +0100
     2.3 @@ -89,6 +89,15 @@
     2.4    }
     2.5  
     2.6  
     2.7 +  /* meta data */
     2.8 +
     2.9 +  val META_TITLE = "meta_title"
    2.10 +  val META_CREATOR = "meta_creator"
    2.11 +  val META_CONTRIBUTOR = "meta_contributor"
    2.12 +  val META_DATE = "meta_date"
    2.13 +  val META_DESCRIPTION = "meta_description"
    2.14 +
    2.15 +
    2.16    /* formal entities */
    2.17  
    2.18    val BINDING = "binding"
     3.1 --- a/src/Pure/Thy/document_marker.ML	Sun Mar 10 00:23:52 2019 +0100
     3.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 14:19:30 2019 +0100
     3.3 @@ -8,6 +8,7 @@
     3.4  sig
     3.5    type marker = Proof.context -> Proof.context
     3.6    val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
     3.7 +  val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
     3.8    val evaluate: Input.source -> marker
     3.9  end;
    3.10  
    3.11 @@ -37,6 +38,8 @@
    3.12        in body x ctxt' end;
    3.13    in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
    3.14  
    3.15 +fun setup0 name scan = setup name (Scan.lift scan);
    3.16 +
    3.17  
    3.18  (* evaluate inner syntax *)
    3.19  
    3.20 @@ -57,8 +60,16 @@
    3.21  
    3.22  (* concrete markers *)
    3.23  
    3.24 +fun meta_data markup arg ctxt =
    3.25 +  (Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt);
    3.26 +
    3.27  val _ =
    3.28    Theory.setup
    3.29 -    (setup (Binding.make ("tag", \<^here>)) (Scan.lift Parse.name) Document_Source.update_tags);
    3.30 +    (setup0 (Binding.make ("tag", \<^here>)) Parse.name Document_Source.update_tags #>
    3.31 +     setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
    3.32 +     setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
    3.33 +     setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
    3.34 +     setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
    3.35 +     setup0 (Binding.make ("description", \<^here>)) Parse.embedded (meta_data Markup.meta_description));
    3.36  
    3.37  end;