PIDE markup for spell-checking;
authorwenzelm
Sun Mar 10 15:31:24 2019 +0100 (6 weeks ago ago)
changeset 70071cb643a1a5313
parent 70070 be04e9a053a7
child 70072 def3ec9cdb7e
PIDE markup for spell-checking;
src/Pure/Thy/document_marker.ML
     1.1 --- a/src/Pure/Thy/document_marker.ML	Sun Mar 10 14:19:30 2019 +0100
     1.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 15:31:24 2019 +0100
     1.3 @@ -70,6 +70,11 @@
     1.4       setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
     1.5       setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
     1.6       setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
     1.7 -     setup0 (Binding.make ("description", \<^here>)) Parse.embedded (meta_data Markup.meta_description));
     1.8 +     setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded)
     1.9 +      (fn source => fn ctxt =>
    1.10 +        let
    1.11 +          val (arg, pos) = Input.source_content source;
    1.12 +          val _ = Context_Position.report ctxt pos Markup.words;
    1.13 +        in meta_data Markup.meta_description arg ctxt end));
    1.14  
    1.15  end;