# HG changeset patch
# User wenzelm
# Date 1537725593 -7200
# Node ID 6e9df530b44193c2c9f792d0668b80f2c46d65a8
# Parent  d57c460ba11276a26a27c2be889c13b12ded1add
discontinued old-style inner comments;

diff -r d57c460ba112 -r 6e9df530b441 NEWS
--- a/NEWS	Sun Sep 23 19:59:32 2018 +0200
+++ b/NEWS	Sun Sep 23 19:59:53 2018 +0200
@@ -7,6 +7,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Old-style inner comments (* ... *) within the term language are no
+longer supported (legacy feature in Isabelle2018).
+
+
 *** System ***
 
 * Isabelle server command "use_theories" supports "nodes_status_delay"
diff -r d57c460ba112 -r 6e9df530b441 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Sun Sep 23 19:59:32 2018 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Sun Sep 23 19:59:53 2018 +0200
@@ -22,7 +22,7 @@
   val is_tid: string -> bool
   datatype token_kind =
     Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
-    String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF
+    String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF
   eqtype token
   val kind_of_token: token -> token_kind
   val str_of_token: token -> string
@@ -120,13 +120,13 @@
 
 datatype token_kind =
   Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
-  String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF;
+  String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF;
 
 val token_kinds =
   Vector.fromList
    [Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str,
-    String, Cartouche, Space, Comment NONE, Comment (SOME Comment.Comment),
-    Comment (SOME Comment.Cancel), Comment (SOME Comment.Latex), Dummy, EOF];
+    String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
+    Comment Comment.Latex, Dummy, EOF];
 
 fun token_kind i = Vector.sub (token_kinds, i);
 fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
@@ -301,8 +301,7 @@
 
     val scan =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
-      Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
-      Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) ||
+      Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token String ||
       scan_str >> token Str ||
diff -r d57c460ba112 -r 6e9df530b441 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Sep 23 19:59:32 2018 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Sep 23 19:59:53 2018 +0200
@@ -341,12 +341,6 @@
 
     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 =>