# HG changeset patch # User wenzelm # Date 1515340545 -3600 # Node ID 221612c942de51e7334168a16f0b81872bf26cc3 # Parent f834d6f21c5525d7ade4403f2f7ca4b469933829 allow formal comments in ML; ML_Compiler.eval: always suppress comments; diff -r f834d6f21c55 -r 221612c942de src/Pure/ML/ml_compiler.ML --- a/src/Pure/ML/ml_compiler.ML Sun Jan 07 15:12:00 2018 +0100 +++ b/src/Pure/ML/ml_compiler.ML Sun Jan 07 16:55:45 2018 +0100 @@ -173,8 +173,12 @@ if #SML flags then String.explode else maps (String.explode o Symbol.esc) o Symbol.explode; + fun token_content tok = + if ML_Lex.is_comment tok then NONE + else SOME (input_explode (ML_Lex.check_content_of tok), tok); + val input_buffer = - Unsynchronized.ref (toks |> map (`(input_explode o ML_Lex.check_content_of))); + Unsynchronized.ref (map_filter token_content toks); fun get () = (case ! input_buffer of diff -r f834d6f21c55 -r 221612c942de src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Sun Jan 07 15:12:00 2018 +0100 +++ b/src/Pure/ML/ml_lex.ML Sun Jan 07 16:55:45 2018 +0100 @@ -9,11 +9,12 @@ val keywords: string list datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Error of string | EOF + Space | Comment | Comment_Cartouche | Error of string | EOF eqtype token val stopper: token Scan.stopper val is_regular: token -> bool val is_improper: token -> bool + val is_comment: token -> bool val set_range: Position.range -> token -> token val range_of: token -> Position.range val pos_of: token -> Position.T @@ -63,7 +64,7 @@ datatype token_kind = Keyword | Ident | Long_Ident | Type_Var | Word | Int | Real | Char | String | - Space | Comment | Error of string | EOF; + Space | Comment | Comment_Cartouche | Error of string | EOF; datatype token = Token of Position.range * (token_kind * string); @@ -108,8 +109,13 @@ fun is_improper (Token (_, (Space, _))) = true | is_improper (Token (_, (Comment, _))) = true + | is_improper (Token (_, (Comment_Cartouche, _))) = true | is_improper _ = false; +fun is_comment (Token (_, (Comment, _))) = true + | is_comment (Token (_, (Comment_Cartouche, _))) = true + | is_comment _ = false; + fun warn tok = (case tok of Token (_, (Keyword, ":>")) => @@ -147,6 +153,7 @@ | Char => (Markup.ML_char, "") | String => (if SML then Markup.SML_string else Markup.ML_string, "") | Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "") + | Comment_Cartouche => (if SML then Markup.SML_comment else Markup.ML_comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); @@ -292,6 +299,7 @@ scan_string >> token String || scan_blanks1 >> token Space || Symbol_Pos.scan_comment err_prefix >> token Comment || + Symbol_Pos.scan_comment_cartouche err_prefix >> token Comment_Cartouche || Scan.max token_leq (Scan.literal lexicon >> token Keyword) (scan_word >> token Word ||