# HG changeset patch # User wenzelm # Date 1516098472 -3600 # Node ID 1f4d167b6ac93f31a6df374d4472d8ba303f02d8 # Parent 4311845b04126e9a3b574f1cdddea2588b7e2946 discontinued old form of marginal comments; diff -r 4311845b0412 -r 1f4d167b6ac9 NEWS --- a/NEWS Tue Jan 16 09:58:17 2018 +0100 +++ b/NEWS Tue Jan 16 11:27:52 2018 +0100 @@ -9,6 +9,11 @@ *** General *** +* Marginal comments need to be written exclusively in the new-style form +"\ \text\", old ASCII variants like "-- {* ... *}" are no longer +supported. INCOMPATIBILITY, use the command-line tool "isabelle +update_comments" to update existing theory files. + * The "op " syntax for infix operators has been replaced by "()". If begins or ends with a "*", there needs to be a space between the "*" and the corresponding parenthesis. diff -r 4311845b0412 -r 1f4d167b6ac9 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Tue Jan 16 09:58:17 2018 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Tue Jan 16 11:27:52 2018 +0100 @@ -25,7 +25,6 @@ val parse: theory -> Position.T -> string -> Toplevel.transition list val parse_tokens: theory -> Token.T list -> Toplevel.transition list val parse_spans: Token.T list -> Command_Span.span list - val side_comments: Token.T list -> Token.T list val command_reports: theory -> Token.T -> Position.report_text list val check_command: Proof.context -> command_keyword -> string end; @@ -210,12 +209,8 @@ in msg ^ quote (Markup.markup Markup.keyword1 name) end)) end); -val parse_cmt = (Parse.$$$ "--" || Parse.$$$ Symbol.comment) -- Parse.!!! Parse.document_source; - fun commands_source thy = Token.source_proper #> - Source.source Token.stopper (Scan.bulk (parse_cmt >> K NONE || Parse.not_eof >> SOME)) #> - Source.map_filter I #> Source.source Token.stopper (Scan.bulk (fn xs => Parse.!!! (parse_command thy) xs)); in @@ -271,26 +266,6 @@ end; -(* side-comments *) - -local - -fun is_cmt tok = Token.kind_of tok = Token.Comment (SOME Comment.Comment); - -fun cmts (t1 :: t2 :: toks) = - if Token.keyword_with (fn s => s = "--" orelse s = Symbol.comment) t1 then t2 :: cmts toks - else if is_cmt t1 then t1 :: cmts (t2 :: toks) - else cmts (t2 :: toks) - | cmts _ = []; - -in - -val side_comments = - cmts o filter_out (fn tok => Token.is_informal_comment tok orelse Token.is_space tok); - -end; - - (* check commands *) fun command_reports thy tok = diff -r 4311845b0412 -r 1f4d167b6ac9 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Tue Jan 16 09:58:17 2018 +0100 +++ b/src/Pure/Isar/token.ML Tue Jan 16 11:27:52 2018 +0100 @@ -624,7 +624,7 @@ scan_verbatim >> token_range Verbatim || scan_cartouche >> token_range Cartouche || scan_comment >> token_range (Comment NONE) || - (Comment.scan_cancel || Comment.scan_latex) >> (fn (k, ss) => token (Comment (SOME k)) ss) || + Comment.scan >> (fn (k, ss) => token (Comment (SOME k)) ss) || scan_space >> token Space || (Scan.max token_leq (Scan.max token_leq diff -r 4311845b0412 -r 1f4d167b6ac9 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Tue Jan 16 09:58:17 2018 +0100 +++ b/src/Pure/Isar/token.scala Tue Jan 16 11:27:52 2018 +0100 @@ -48,9 +48,6 @@ trait Parsers extends Scan.Parsers with Comment.Parsers { - private def comment_marker: Parser[Token] = - one(Symbol.is_comment) ^^ (x => Token(Token.Kind.KEYWORD, x)) - private def delimited_token: Parser[Token] = { val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x)) @@ -111,7 +108,7 @@ } def token(keywords: Keyword.Keywords): Parser[Token] = - comment_marker | (delimited_token | other_token(keywords)) + delimited_token | other_token(keywords) def token_line(keywords: Keyword.Keywords, ctxt: Scan.Line_Context) : Parser[(Token, Scan.Line_Context)] = diff -r 4311845b0412 -r 1f4d167b6ac9 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Tue Jan 16 09:58:17 2018 +0100 +++ b/src/Pure/PIDE/command.ML Tue Jan 16 11:27:52 2018 +0100 @@ -205,8 +205,10 @@ (fn () => (span |> maps (fn tok => check_error (fn () => Thy_Output.check_token_comments ctxt tok))) @ - (Outer_Syntax.side_comments span |> maps (fn tok => - check_error (fn () => Thy_Output.output_text ctxt {markdown = false} (Token.input_of tok))))) + (span |> maps (fn tok => + if Token.kind_of tok = Token.Comment (SOME Comment.Comment) then + check_error (fn () => Thy_Output.output_text ctxt {markdown = false} (Token.input_of tok)) + else []))) (); fun report tr m = diff -r 4311845b0412 -r 1f4d167b6ac9 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Jan 16 09:58:17 2018 +0100 +++ b/src/Pure/PIDE/command.scala Tue Jan 16 11:27:52 2018 +0100 @@ -396,11 +396,10 @@ private def clean_tokens(tokens: List[Token]): List[(Token, Int)] = { - val markers = Set("%", "--", Symbol.comment, Symbol.comment_decoded) def clean(toks: List[(Token, Int)]): List[(Token, Int)] = toks match { case (t1, i1) :: (t2, i2) :: rest => - if (t1.is_keyword && markers(t1.source)) clean(rest) + if (t1.is_keyword && t1.source == "%" && t2.is_name) clean(rest) else (t1, i1) :: clean((t2, i2) :: rest) case _ => toks } diff -r 4311845b0412 -r 1f4d167b6ac9 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Tue Jan 16 09:58:17 2018 +0100 +++ b/src/Pure/Pure.thy Tue Jan 16 11:27:52 2018 +0100 @@ -6,7 +6,7 @@ theory Pure keywords - "!!" "!" "+" "--" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" + "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" "\" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command diff -r 4311845b0412 -r 1f4d167b6ac9 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Tue Jan 16 09:58:17 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Tue Jan 16 11:27:52 2018 +0100 @@ -355,11 +355,7 @@ (Basic_Token cmd, (markup_false, d)))])); val cmt = Scan.peek (fn d => - Scan.one is_black_comment >> - (fn tok => (NONE, (Basic_Token tok, ("", d)))) || - (Parse.$$$ "--" || Parse.$$$ Symbol.comment) |-- - Parse.!!!! (improper |-- Parse.document_source) >> - (fn source => (NONE, (Markup_Token ("cmt", source), ("", d))))); + Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); val other = Scan.peek (fn d => Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d)))));