old-style inner comments are legacy;
authorwenzelm
Thu Jan 25 16:01:02 2018 +0100 (16 months ago)
changeset 675075db077cfe1b2
parent 67506 30233285270a
child 67508 189ab2c3026b
old-style inner comments are legacy;
NEWS
src/Pure/Syntax/syntax_phases.ML
     1.1 --- a/NEWS	Thu Jan 25 15:21:05 2018 +0100
     1.2 +++ b/NEWS	Thu Jan 25 16:01:02 2018 +0100
     1.3 @@ -14,6 +14,10 @@
     1.4  supported. INCOMPATIBILITY, use the command-line tool "isabelle
     1.5  update_comments" to update existing theory files.
     1.6  
     1.7 +* Old-style inner comments (* ... *) within the term language are legacy
     1.8 +and will be discontinued soon: use formal comments "\<comment> \<open>...\<close>" or "\<^cancel>\<open>...\<close>"
     1.9 +instead.
    1.10 +
    1.11  * The "op <infix-op>" syntax for infix operators has been replaced by
    1.12  "(<infix-op>)". If <infix-op> begins or ends with a "*", there needs to
    1.13  be a space between the "*" and the corresponding parenthesis.
     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Thu Jan 25 15:21:05 2018 +0100
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Thu Jan 25 16:01:02 2018 +0100
     2.3 @@ -340,6 +340,12 @@
     2.4  
     2.5      val toks = Syntax.tokenize syn raw syms;
     2.6      val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
     2.7 +    val _ = toks |> List.app (fn tok =>
     2.8 +      (case Lexicon.kind_of_token tok of
     2.9 +        Lexicon.Comment NONE =>
    2.10 +          legacy_feature ("Old-style inner comment: use \"\<comment> \<open>...\<close>\" or \"\<^cancel>\<open>...\<close>\" instead" ^
    2.11 +            Position.here (Lexicon.pos_of_token tok))
    2.12 +      | _ => ()));
    2.13  
    2.14      val pts = Syntax.parse syn root (filter Lexicon.is_proper toks)
    2.15        handle ERROR msg =>