# HG changeset patch # User wenzelm # Date 1535390947 -7200 # Node ID 253f04c1e8146a684ec6fd1616facbef7cfc1162 # Parent 877534be1930d8937373b06b3eb88f4751d9f199 simplified markup; diff -r 877534be1930 -r 253f04c1e814 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Mon Aug 27 19:12:48 2018 +0200 +++ b/src/Pure/ML/ml_lex.ML Mon Aug 27 19:29:07 2018 +0200 @@ -148,23 +148,23 @@ local -fun token_kind_markup SML = +val token_kind_markup = fn Type_Var => (Markup.ML_tvar, "") | Word => (Markup.ML_numeral, "") | Int => (Markup.ML_numeral, "") | Real => (Markup.ML_numeral, "") | 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, "") + | String => (Markup.ML_string, "") + | Comment _ => (Markup.ML_comment, "") | Error msg => (Markup.bad (), msg) | _ => (Markup.empty, ""); in -fun token_report SML (tok as Token ((pos, _), (kind, x))) = +fun token_report (tok as Token ((pos, _), (kind, x))) = let val (markup, txt) = - if not (is_keyword tok) then token_kind_markup SML kind + if not (is_keyword tok) then token_kind_markup kind else if is_delimiter tok then (Markup.ML_delimiter, "") else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "") else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "") @@ -349,8 +349,7 @@ (fn msg => recover msg >> map Antiquote.Text)) |> Source.exhaust; val _ = Position.reports (Antiquote.antiq_reports input); - val _ = - Position.reports_text (maps (fn Antiquote.Text t => [token_report SML t] | _ => []) input); + val _ = Position.reports_text (maps (fn Antiquote.Text t => [token_report t] | _ => []) input); val _ = List.app check input; in input @ termination end; diff -r 877534be1930 -r 253f04c1e814 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Mon Aug 27 19:12:48 2018 +0200 +++ b/src/Pure/PIDE/markup.ML Mon Aug 27 19:29:07 2018 +0200 @@ -110,8 +110,6 @@ val ML_charN: string val ML_char: T val ML_stringN: string val ML_string: T val ML_commentN: string val ML_comment: T - val SML_stringN: string val SML_string: T - val SML_commentN: string val SML_comment: T val ML_defN: string val ML_openN: string val ML_structureN: string @@ -459,8 +457,6 @@ val (ML_charN, ML_char) = markup_elem "ML_char"; val (ML_stringN, ML_string) = markup_elem "ML_string"; val (ML_commentN, ML_comment) = markup_elem "ML_comment"; -val (SML_stringN, SML_string) = markup_elem "SML_string"; -val (SML_commentN, SML_comment) = markup_elem "SML_comment"; val ML_defN = "ML_def"; val ML_openN = "ML_open"; diff -r 877534be1930 -r 253f04c1e814 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Mon Aug 27 19:12:48 2018 +0200 +++ b/src/Pure/PIDE/markup.scala Mon Aug 27 19:29:07 2018 +0200 @@ -319,8 +319,6 @@ val ML_CHAR = "ML_char" val ML_STRING = "ML_string" val ML_COMMENT = "ML_comment" - val SML_STRING = "SML_string" - val SML_COMMENT = "SML_comment" val ML_DEF = "ML_def" val ML_OPEN = "ML_open" diff -r 877534be1930 -r 253f04c1e814 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Mon Aug 27 19:12:48 2018 +0200 +++ b/src/Pure/PIDE/rendering.scala Mon Aug 27 19:29:07 2018 +0200 @@ -136,9 +136,7 @@ Markup.ML_NUMERAL -> Color.inner_numeral, Markup.ML_CHAR -> Color.inner_quoted, Markup.ML_STRING -> Color.inner_quoted, - Markup.ML_COMMENT -> Color.inner_comment, - Markup.SML_STRING -> Color.inner_quoted, - Markup.SML_COMMENT -> Color.inner_comment) + Markup.ML_COMMENT -> Color.inner_comment) val foreground = Map(