# HG changeset patch
# User wenzelm
# Date 1516892462 -3600
# Node ID 5db077cfe1b2eb6bd3f20063a447834fb1da4698
# Parent  30233285270acbc71503d9aa50e9a2992561f38b
old-style inner comments are legacy;

diff -r 30233285270a -r 5db077cfe1b2 NEWS
--- 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.
diff -r 30233285270a -r 5db077cfe1b2 src/Pure/Syntax/syntax_phases.ML
--- 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 =>