--- 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".
--- 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