src/Pure/Thy/document_marker.ML
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (2 months ago ago)
changeset 70070 be04e9a053a7
parent 70068 b9985133805d
child 70071 cb643a1a5313
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
wenzelm@70068
     1
(*  Title:      Pure/Thy/document_marker.ML
wenzelm@70068
     2
    Author:     Makarius
wenzelm@70068
     3
wenzelm@70068
     4
Document markers: declarations on the presentation context.
wenzelm@70068
     5
*)
wenzelm@70068
     6
wenzelm@70068
     7
signature DOCUMENT_MARKER =
wenzelm@70068
     8
sig
wenzelm@70068
     9
  type marker = Proof.context -> Proof.context
wenzelm@70068
    10
  val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
wenzelm@70070
    11
  val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
wenzelm@70068
    12
  val evaluate: Input.source -> marker
wenzelm@70068
    13
end;
wenzelm@70068
    14
wenzelm@70068
    15
structure Document_Marker: DOCUMENT_MARKER =
wenzelm@70068
    16
struct
wenzelm@70068
    17
wenzelm@70068
    18
(* theory data *)
wenzelm@70068
    19
wenzelm@70068
    20
type marker = Proof.context -> Proof.context;
wenzelm@70068
    21
wenzelm@70068
    22
structure Markers = Theory_Data
wenzelm@70068
    23
(
wenzelm@70068
    24
  type T = (Token.src -> Proof.context -> Proof.context) Name_Space.table;
wenzelm@70068
    25
  val empty : T = Name_Space.empty_table "document_marker";
wenzelm@70068
    26
  val extend = I;
wenzelm@70068
    27
  val merge = Name_Space.merge_tables;
wenzelm@70068
    28
);
wenzelm@70068
    29
wenzelm@70068
    30
val get_markers = Markers.get o Proof_Context.theory_of;
wenzelm@70068
    31
wenzelm@70068
    32
fun check ctxt = Name_Space.check (Context.Proof ctxt) (get_markers ctxt);
wenzelm@70068
    33
wenzelm@70068
    34
fun setup name scan body thy =
wenzelm@70068
    35
  let
wenzelm@70068
    36
    fun marker src ctxt =
wenzelm@70068
    37
      let val (x, ctxt') = Token.syntax scan src ctxt
wenzelm@70068
    38
      in body x ctxt' end;
wenzelm@70068
    39
  in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
wenzelm@70068
    40
wenzelm@70070
    41
fun setup0 name scan = setup name (Scan.lift scan);
wenzelm@70070
    42
wenzelm@70068
    43
wenzelm@70068
    44
(* evaluate inner syntax *)
wenzelm@70068
    45
wenzelm@70068
    46
val parse_marker = Parse.token Parse.liberal_name ::: Parse.!!! Parse.args;
wenzelm@70068
    47
wenzelm@70068
    48
fun evaluate input ctxt =
wenzelm@70068
    49
  let
wenzelm@70068
    50
    val pos = Input.pos_of input;
wenzelm@70068
    51
    val _ = Context_Position.report ctxt pos Markup.language_document_marker;
wenzelm@70068
    52
wenzelm@70068
    53
    val syms = Input.source_explode input;
wenzelm@70068
    54
    val markers =
wenzelm@70068
    55
      (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) syms of
wenzelm@70068
    56
        SOME res => res
wenzelm@70068
    57
      | NONE => error ("Bad input" ^ Position.here pos));
wenzelm@70068
    58
  in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
wenzelm@70068
    59
wenzelm@70068
    60
wenzelm@70068
    61
(* concrete markers *)
wenzelm@70068
    62
wenzelm@70070
    63
fun meta_data markup arg ctxt =
wenzelm@70070
    64
  (Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt);
wenzelm@70070
    65
wenzelm@70068
    66
val _ =
wenzelm@70068
    67
  Theory.setup
wenzelm@70070
    68
    (setup0 (Binding.make ("tag", \<^here>)) Parse.name Document_Source.update_tags #>
wenzelm@70070
    69
     setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
wenzelm@70070
    70
     setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
wenzelm@70070
    71
     setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
wenzelm@70070
    72
     setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
wenzelm@70070
    73
     setup0 (Binding.make ("description", \<^here>)) Parse.embedded (meta_data Markup.meta_description));
wenzelm@70068
    74
wenzelm@70068
    75
end;