--- a/NEWS Thu Jan 25 15:21:05 2018 +0100
+++ b/NEWS Thu Jan 25 16:01:02 2018 +0100
@@ -14,6 +14,10 @@
supported. INCOMPATIBILITY, use the command-line tool "isabelle
update_comments" to update existing theory files.
+* Old-style inner comments (* ... *) within the term language are legacy
+and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"
+instead.
+
* The "op <infix-op>" syntax for infix operators has been replaced by
"(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
be a space between the "*" and the corresponding parenthesis.
--- a/src/Pure/Syntax/syntax_phases.ML Thu Jan 25 15:21:05 2018 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Thu Jan 25 16:01:02 2018 +0100
@@ -340,6 +340,12 @@
val toks = Syntax.tokenize syn raw syms;
val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
+ val _ = toks |> List.app (fn tok =>
+ (case Lexicon.kind_of_token tok of
+ Lexicon.Comment NONE =>
+ legacy_feature ("Old-style inner comment: use \"\<comment> \<open>...\<close>\" or \"\<^cancel>\<open>...\<close>\" instead" ^
+ Position.here (Lexicon.pos_of_token tok))
+ | _ => ()));
val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
handle ERROR msg =>