PIDE markup for spell-checking;

--- 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;