# 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(