# HG changeset patch
# User wenzelm
# Date 1457201644 -3600
# Node ID 2382876c238b219e8c9362f2467be4d85d51c924
# Parent  a564458f94db9654fec0290706d106f4f096f8ed
more PIDE markup;

diff -r a564458f94db -r 2382876c238b src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Mar 05 17:01:45 2016 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Mar 05 19:14:04 2016 +0100
@@ -40,6 +40,7 @@
   val language_document: bool -> T
   val language_antiquotation: T
   val language_text: bool -> T
+  val language_verbatim: bool -> T
   val language_rail: T
   val language_path: T
   val bindingN: string val binding: T
@@ -316,6 +317,7 @@
 val language_antiquotation =
   language {name = "antiquotation", symbols = true, antiquotes = false, delimited = true};
 val language_text = language' {name = "text", symbols = true, antiquotes = false};
+val language_verbatim = language' {name = "verbatim", symbols = true, antiquotes = false};
 val language_rail = language {name = "rail", symbols = true, antiquotes = true, delimited = true};
 val language_path = language {name = "path", symbols = false, antiquotes = false, delimited = true};
 
diff -r a564458f94db -r 2382876c238b src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Sat Mar 05 17:01:45 2016 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Sat Mar 05 19:14:04 2016 +0100
@@ -154,8 +154,11 @@
 
 val _ =
   Theory.setup
-    (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text)
-      (Thy_Output.verbatim_text o #context));
+    (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.text_input)
+      (fn {context = ctxt, ...} => fn source =>
+       (Context_Position.report ctxt (Input.pos_of source)
+          (Markup.language_verbatim (Input.is_delimited source));
+        Thy_Output.verbatim_text ctxt (Input.source_content source))));
 
 
 (* ML text *)