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