less confusing markup;
authorwenzelm
Sat Nov 07 13:13:23 2015 +0100 (2015-11-07)
changeset 61598ed4dad8823a4
parent 61597 53e32a9b66b8
child 61599 2e52df0cd8ee
less confusing markup;
src/Pure/ML/ml_antiquotations.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/ML/ml_antiquotations.ML	Sat Nov 07 12:53:22 2015 +0100
     1.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Sat Nov 07 13:13:23 2015 +0100
     1.3 @@ -12,9 +12,8 @@
     1.4  val _ = Theory.setup
     1.5   (ML_Antiquotation.value @{binding cartouche}
     1.6      (Args.context -- Scan.lift (Parse.position Args.cartouche_input) >> (fn (ctxt, (source, pos)) =>
     1.7 -      (Context_Position.report ctxt pos Markup.ML_cartouche;
     1.8 -        "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
     1.9 -          ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))) #>
    1.10 +      "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
    1.11 +        ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
    1.12  
    1.13    ML_Antiquotation.inline @{binding undefined}
    1.14      (Scan.succeed "(raise General.Match)") #>
     2.1 --- a/src/Pure/PIDE/markup.ML	Sat Nov 07 12:53:22 2015 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Sat Nov 07 13:13:23 2015 +0100
     2.3 @@ -101,7 +101,6 @@
     2.4    val ML_numeralN: string val ML_numeral: T
     2.5    val ML_charN: string val ML_char: T
     2.6    val ML_stringN: string val ML_string: T
     2.7 -  val ML_cartoucheN: string val ML_cartouche: T
     2.8    val ML_commentN: string val ML_comment: T
     2.9    val SML_stringN: string val SML_string: T
    2.10    val SML_commentN: string val SML_comment: T
    2.11 @@ -440,7 +439,6 @@
    2.12  val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
    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_cartoucheN, ML_cartouche) = markup_elem "ML_cartouche";
    2.16  val (ML_commentN, ML_comment) = markup_elem "ML_comment";
    2.17  val (SML_stringN, SML_string) = markup_elem "SML_string";
    2.18  val (SML_commentN, SML_comment) = markup_elem "SML_comment";
     3.1 --- a/src/Pure/PIDE/markup.scala	Sat Nov 07 12:53:22 2015 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Sat Nov 07 13:13:23 2015 +0100
     3.3 @@ -260,7 +260,6 @@
     3.4    val ML_NUMERAL = "ML_numeral"
     3.5    val ML_CHAR = "ML_char"
     3.6    val ML_STRING = "ML_string"
     3.7 -  val ML_CARTOUCHE = "ML_cartouche"
     3.8    val ML_COMMENT = "ML_comment"
     3.9    val SML_STRING = "SML_string"
    3.10    val SML_COMMENT = "SML_comment"
     4.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Nov 07 12:53:22 2015 +0100
     4.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Nov 07 13:13:23 2015 +0100
     4.3 @@ -143,7 +143,7 @@
     4.4    private val language_context_elements =
     4.5      Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
     4.6        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
     4.7 -      Markup.ML_STRING, Markup.ML_CARTOUCHE, Markup.ML_COMMENT)
     4.8 +      Markup.ML_STRING, Markup.ML_COMMENT)
     4.9  
    4.10    private val language_elements = Markup.Elements(Markup.LANGUAGE)
    4.11  
    4.12 @@ -309,9 +309,7 @@
    4.13            if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
    4.14            else None
    4.15          case Text.Info(_, elem)
    4.16 -        if elem.name == Markup.ML_STRING ||
    4.17 -          elem.name == Markup.ML_CARTOUCHE ||
    4.18 -          elem.name == Markup.ML_COMMENT =>
    4.19 +        if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
    4.20            Some(Completion.Language_Context.ML_inner)
    4.21          case Text.Info(_, _) =>
    4.22            Some(Completion.Language_Context.inner)
    4.23 @@ -778,7 +776,6 @@
    4.24        Markup.ML_NUMERAL -> inner_numeral_color,
    4.25        Markup.ML_CHAR -> inner_quoted_color,
    4.26        Markup.ML_STRING -> inner_quoted_color,
    4.27 -      Markup.ML_CARTOUCHE -> inner_cartouche_color,
    4.28        Markup.ML_COMMENT -> inner_comment_color,
    4.29        Markup.SML_STRING -> inner_quoted_color,
    4.30        Markup.SML_COMMENT -> inner_comment_color)