# HG changeset patch
# User wenzelm
# Date 1545854243 -3600
# Node ID 7d59af98af29c2fca1ba3c07bf6055c4984c89f9
# Parent  cc2d676d53952ca0c057ea165621af977922c181
{* verbatim *} is explicit legacy feature;

diff -r cc2d676d5395 -r 7d59af98af29 NEWS
--- a/NEWS	Wed Dec 26 16:25:20 2018 +0100
+++ b/NEWS	Wed Dec 26 20:57:23 2018 +0100
@@ -9,6 +9,10 @@
 
 *** General ***
 
+* Old-style {* verbatim *} tokens are explicitly marked as legacy
+feature and will be removed soon. Use \<open>cartouche\<close> syntax instead, e.g.
+via "isabelle update_cartouches -t" (available since Isabelle2015).
+
 * The font family "Isabelle DejaVu" is systematically derived from the
 existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif"
 and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique".
diff -r cc2d676d5395 -r 7d59af98af29 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Dec 26 16:25:20 2018 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Dec 26 20:57:23 2018 +0100
@@ -145,6 +145,14 @@
 
     val token_reports = map (reports_of_token keywords) span;
     val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span);
+
+    val verbatim =
+      span |> map_filter (fn tok =>
+        if Token.kind_of tok = Token.Verbatim then SOME (Token.pos_of tok) else NONE);
+    val _ =
+      if null verbatim then ()
+      else legacy_feature ("Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead" ^
+        Position.here_list verbatim);
   in
     if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax"
     else