src/Pure/Thy/document_marker.ML
changeset 70070 be04e9a053a7
parent 70068 b9985133805d
child 70071 cb643a1a5313
     1.1 --- a/src/Pure/Thy/document_marker.ML	Sun Mar 10 00:23:52 2019 +0100
     1.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 14:19:30 2019 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    type marker = Proof.context -> Proof.context
     1.6    val setup: binding -> 'a context_parser -> ('a -> marker) -> theory -> theory
     1.7 +  val setup0: binding -> 'a parser -> ('a -> marker) -> theory -> theory
     1.8    val evaluate: Input.source -> marker
     1.9  end;
    1.10  
    1.11 @@ -37,6 +38,8 @@
    1.12        in body x ctxt' end;
    1.13    in thy |> Markers.map (Name_Space.define (Context.Theory thy) true (name, marker) #> #2) end;
    1.14  
    1.15 +fun setup0 name scan = setup name (Scan.lift scan);
    1.16 +
    1.17  
    1.18  (* evaluate inner syntax *)
    1.19  
    1.20 @@ -57,8 +60,16 @@
    1.21  
    1.22  (* concrete markers *)
    1.23  
    1.24 +fun meta_data markup arg ctxt =
    1.25 +  (Context_Position.report_text ctxt (Position.thread_data ()) markup arg; ctxt);
    1.26 +
    1.27  val _ =
    1.28    Theory.setup
    1.29 -    (setup (Binding.make ("tag", \<^here>)) (Scan.lift Parse.name) Document_Source.update_tags);
    1.30 +    (setup0 (Binding.make ("tag", \<^here>)) Parse.name Document_Source.update_tags #>
    1.31 +     setup0 (Binding.make ("title", \<^here>)) Parse.embedded (meta_data Markup.meta_title) #>
    1.32 +     setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
    1.33 +     setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
    1.34 +     setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
    1.35 +     setup0 (Binding.make ("description", \<^here>)) Parse.embedded (meta_data Markup.meta_description));
    1.36  
    1.37  end;