simplified markup;
authorwenzelm
Mon Aug 27 19:29:07 2018 +0200 (9 months ago)
changeset 68822253f04c1e814
parent 68821 877534be1930
child 68823 5e7b1ae10eb8
simplified markup;
src/Pure/ML/ml_lex.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
     1.1 --- a/src/Pure/ML/ml_lex.ML	Mon Aug 27 19:12:48 2018 +0200
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Mon Aug 27 19:29:07 2018 +0200
     1.3 @@ -148,23 +148,23 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun token_kind_markup SML =
     1.8 +val token_kind_markup =
     1.9   fn Type_Var => (Markup.ML_tvar, "")
    1.10    | Word => (Markup.ML_numeral, "")
    1.11    | Int => (Markup.ML_numeral, "")
    1.12    | Real => (Markup.ML_numeral, "")
    1.13    | Char => (Markup.ML_char, "")
    1.14 -  | String => (if SML then Markup.SML_string else Markup.ML_string, "")
    1.15 -  | Comment _ => (if SML then Markup.SML_comment else Markup.ML_comment, "")
    1.16 +  | String => (Markup.ML_string, "")
    1.17 +  | Comment _ => (Markup.ML_comment, "")
    1.18    | Error msg => (Markup.bad (), msg)
    1.19    | _ => (Markup.empty, "");
    1.20  
    1.21  in
    1.22  
    1.23 -fun token_report SML (tok as Token ((pos, _), (kind, x))) =
    1.24 +fun token_report (tok as Token ((pos, _), (kind, x))) =
    1.25    let
    1.26      val (markup, txt) =
    1.27 -      if not (is_keyword tok) then token_kind_markup SML kind
    1.28 +      if not (is_keyword tok) then token_kind_markup kind
    1.29        else if is_delimiter tok then (Markup.ML_delimiter, "")
    1.30        else if member (op =) keywords2 x then (Markup.ML_keyword2 |> Markup.keyword_properties, "")
    1.31        else if member (op =) keywords3 x then (Markup.ML_keyword3 |> Markup.keyword_properties, "")
    1.32 @@ -349,8 +349,7 @@
    1.33            (fn msg => recover msg >> map Antiquote.Text))
    1.34        |> Source.exhaust;
    1.35      val _ = Position.reports (Antiquote.antiq_reports input);
    1.36 -    val _ =
    1.37 -      Position.reports_text (maps (fn Antiquote.Text t => [token_report SML t] | _ => []) input);
    1.38 +    val _ = Position.reports_text (maps (fn Antiquote.Text t => [token_report t] | _ => []) input);
    1.39      val _ = List.app check input;
    1.40    in input @ termination end;
    1.41  
     2.1 --- a/src/Pure/PIDE/markup.ML	Mon Aug 27 19:12:48 2018 +0200
     2.2 +++ b/src/Pure/PIDE/markup.ML	Mon Aug 27 19:29:07 2018 +0200
     2.3 @@ -110,8 +110,6 @@
     2.4    val ML_charN: string val ML_char: T
     2.5    val ML_stringN: string val ML_string: T
     2.6    val ML_commentN: string val ML_comment: T
     2.7 -  val SML_stringN: string val SML_string: T
     2.8 -  val SML_commentN: string val SML_comment: T
     2.9    val ML_defN: string
    2.10    val ML_openN: string
    2.11    val ML_structureN: string
    2.12 @@ -459,8 +457,6 @@
    2.13  val (ML_charN, ML_char) = markup_elem "ML_char";
    2.14  val (ML_stringN, ML_string) = markup_elem "ML_string";
    2.15  val (ML_commentN, ML_comment) = markup_elem "ML_comment";
    2.16 -val (SML_stringN, SML_string) = markup_elem "SML_string";
    2.17 -val (SML_commentN, SML_comment) = markup_elem "SML_comment";
    2.18  
    2.19  val ML_defN = "ML_def";
    2.20  val ML_openN = "ML_open";
     3.1 --- a/src/Pure/PIDE/markup.scala	Mon Aug 27 19:12:48 2018 +0200
     3.2 +++ b/src/Pure/PIDE/markup.scala	Mon Aug 27 19:29:07 2018 +0200
     3.3 @@ -319,8 +319,6 @@
     3.4    val ML_CHAR = "ML_char"
     3.5    val ML_STRING = "ML_string"
     3.6    val ML_COMMENT = "ML_comment"
     3.7 -  val SML_STRING = "SML_string"
     3.8 -  val SML_COMMENT = "SML_comment"
     3.9  
    3.10    val ML_DEF = "ML_def"
    3.11    val ML_OPEN = "ML_open"
     4.1 --- a/src/Pure/PIDE/rendering.scala	Mon Aug 27 19:12:48 2018 +0200
     4.2 +++ b/src/Pure/PIDE/rendering.scala	Mon Aug 27 19:29:07 2018 +0200
     4.3 @@ -136,9 +136,7 @@
     4.4      Markup.ML_NUMERAL -> Color.inner_numeral,
     4.5      Markup.ML_CHAR -> Color.inner_quoted,
     4.6      Markup.ML_STRING -> Color.inner_quoted,
     4.7 -    Markup.ML_COMMENT -> Color.inner_comment,
     4.8 -    Markup.SML_STRING -> Color.inner_quoted,
     4.9 -    Markup.SML_COMMENT -> Color.inner_comment)
    4.10 +    Markup.ML_COMMENT -> Color.inner_comment)
    4.11  
    4.12    val foreground =
    4.13      Map(