discontinued old-style inner comments;
authorwenzelm
Sun Sep 23 19:59:53 2018 +0200 (13 months ago ago)
changeset 690426e9df530b441
parent 69041 d57c460ba112
child 69043 57a76e4728ed
discontinued old-style inner comments;
NEWS
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/NEWS	Sun Sep 23 19:59:32 2018 +0200
     1.2 +++ b/NEWS	Sun Sep 23 19:59:53 2018 +0200
     1.3 @@ -7,6 +7,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Old-style inner comments (* ... *) within the term language are no
    1.10 +longer supported (legacy feature in Isabelle2018).
    1.11 +
    1.12 +
    1.13  *** System ***
    1.14  
    1.15  * Isabelle server command "use_theories" supports "nodes_status_delay"
     2.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Sep 23 19:59:32 2018 +0200
     2.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Sep 23 19:59:53 2018 +0200
     2.3 @@ -22,7 +22,7 @@
     2.4    val is_tid: string -> bool
     2.5    datatype token_kind =
     2.6      Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
     2.7 -    String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF
     2.8 +    String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF
     2.9    eqtype token
    2.10    val kind_of_token: token -> token_kind
    2.11    val str_of_token: token -> string
    2.12 @@ -120,13 +120,13 @@
    2.13  
    2.14  datatype token_kind =
    2.15    Literal | Ident | Long_Ident | Var | Type_Ident | Type_Var | Num | Float | Str |
    2.16 -  String | Cartouche | Space | Comment of Comment.kind option | Dummy | EOF;
    2.17 +  String | Cartouche | Space | Comment of Comment.kind | Dummy | EOF;
    2.18  
    2.19  val token_kinds =
    2.20    Vector.fromList
    2.21     [Literal, Ident, Long_Ident, Var, Type_Ident, Type_Var, Num, Float, Str,
    2.22 -    String, Cartouche, Space, Comment NONE, Comment (SOME Comment.Comment),
    2.23 -    Comment (SOME Comment.Cancel), Comment (SOME Comment.Latex), Dummy, EOF];
    2.24 +    String, Cartouche, Space, Comment Comment.Comment, Comment Comment.Cancel,
    2.25 +    Comment Comment.Latex, Dummy, EOF];
    2.26  
    2.27  fun token_kind i = Vector.sub (token_kinds, i);
    2.28  fun token_kind_index k = #1 (the (Vector.findi (fn (_, k') => k = k') token_kinds));
    2.29 @@ -301,8 +301,7 @@
    2.30  
    2.31      val scan =
    2.32        Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
    2.33 -      Symbol_Pos.scan_comment err_prefix >> token (Comment NONE) ||
    2.34 -      Comment.scan >> (fn (kind, ss) => token (Comment (SOME kind)) ss) ||
    2.35 +      Comment.scan >> (fn (kind, ss) => token (Comment kind) ss) ||
    2.36        Scan.max token_leq scan_lit scan_val ||
    2.37        scan_string >> token String ||
    2.38        scan_str >> token Str ||
     3.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Sep 23 19:59:32 2018 +0200
     3.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Sep 23 19:59:53 2018 +0200
     3.3 @@ -341,12 +341,6 @@
     3.4  
     3.5      val toks = Syntax.tokenize syn raw syms;
     3.6      val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
     3.7 -    val _ = toks |> List.app (fn tok =>
     3.8 -      (case Lexicon.kind_of_token tok of
     3.9 -        Lexicon.Comment NONE =>
    3.10 -          legacy_feature ("Old-style inner comment: use \"\<comment> \<open>...\<close>\" or \"\<^cancel>\<open>...\<close>\" instead" ^
    3.11 -            Position.here (Lexicon.pos_of_token tok))
    3.12 -      | _ => ()));
    3.13  
    3.14      val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
    3.15        handle ERROR msg =>