# HG changeset patch
# User wenzelm
# Date 1552228284 -3600
# Node ID cb643a1a53134b812520819dee4cc7eefd9327d6
# Parent  be04e9a053a7cfb847e29e250554390051273c71
PIDE markup for spell-checking;

diff -r be04e9a053a7 -r cb643a1a5313 src/Pure/Thy/document_marker.ML
--- a/src/Pure/Thy/document_marker.ML	Sun Mar 10 14:19:30 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML	Sun Mar 10 15:31:24 2019 +0100
@@ -70,6 +70,11 @@
      setup0 (Binding.make ("creator", \<^here>)) Parse.embedded (meta_data Markup.meta_creator) #>
      setup0 (Binding.make ("contributor", \<^here>)) Parse.embedded (meta_data Markup.meta_contributor) #>
      setup0 (Binding.make ("date", \<^here>)) Parse.embedded (meta_data Markup.meta_date) #>
-     setup0 (Binding.make ("description", \<^here>)) Parse.embedded (meta_data Markup.meta_description));
+     setup0 (Binding.make ("description", \<^here>)) (Parse.input Parse.embedded)
+      (fn source => fn ctxt =>
+        let
+          val (arg, pos) = Input.source_content source;
+          val _ = Context_Position.report ctxt pos Markup.words;
+        in meta_data Markup.meta_description arg ctxt end));
 
 end;