# 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 \cartouche\ 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 \cartouche\ instead" ^ + Position.here_list verbatim); in if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax" else