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