more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
authorwenzelm
Wed Mar 05 16:13:24 2014 +0100 (2014-03-05 ago)
changeset 559192eb8c13339a5
parent 55918 41e06ec17604
child 55920 f376f18fd0b7
more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
src/Pure/Isar/token.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/Isar/token.ML	Wed Mar 05 16:06:11 2014 +0100
     1.2 +++ b/src/Pure/Isar/token.ML	Wed Mar 05 16:13:24 2014 +0100
     1.3 @@ -42,7 +42,6 @@
     1.4    val inner_syntax_of: T -> string
     1.5    val source_position_of: T -> Symbol_Pos.source
     1.6    val content_of: T -> string
     1.7 -  val keyword_markup: string -> Markup.T
     1.8    val value_markup: value -> Markup.T list
     1.9    val completion_report: T -> Position.report_text list
    1.10    val report: T -> Position.report_text
    1.11 @@ -254,14 +253,13 @@
    1.12    | Sync          => (Markup.control, "")
    1.13    | EOF           => (Markup.control, "");
    1.14  
    1.15 +fun keyword_markup keyword x =
    1.16 +  if Symbol.is_ascii_identifier x then keyword else Markup.operator;
    1.17 +
    1.18  in
    1.19  
    1.20 -fun keyword_markup x =
    1.21 -  if Symbol.is_ascii_identifier x
    1.22 -  then Markup.keyword2
    1.23 -  else Markup.operator;
    1.24 -
    1.25 -fun value_markup (Literal x) = keyword_markup x :: Completion.suppress_abbrevs x
    1.26 +fun value_markup (Literal x) =
    1.27 +      keyword_markup Markup.quasi_keyword x :: Completion.suppress_abbrevs x
    1.28    | value_markup _ = [];
    1.29  
    1.30  fun completion_report tok =
    1.31 @@ -271,7 +269,7 @@
    1.32  
    1.33  fun report tok =
    1.34    if is_kind Keyword tok then
    1.35 -    ((pos_of tok, keyword_markup (content_of tok)), "")
    1.36 +    ((pos_of tok, keyword_markup Markup.keyword2 (content_of tok)), "")
    1.37    else
    1.38      let val (m, text) = token_kind_markup (kind_of tok)
    1.39      in ((pos_of tok, m), text) end;
     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Mar 05 16:06:11 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Wed Mar 05 16:13:24 2014 +0100
     2.3 @@ -114,6 +114,7 @@
     2.4    val keyword1N: string val keyword1: T
     2.5    val keyword2N: string val keyword2: T
     2.6    val keyword3N: string val keyword3: T
     2.7 +  val quasi_keywordN: string val quasi_keyword: T
     2.8    val elapsedN: string
     2.9    val cpuN: string
    2.10    val gcN: string
    2.11 @@ -419,6 +420,7 @@
    2.12  val (keyword1N, keyword1) = markup_elem "keyword1";
    2.13  val (keyword2N, keyword2) = markup_elem "keyword2";
    2.14  val (keyword3N, keyword3) = markup_elem "keyword3";
    2.15 +val (quasi_keywordN, quasi_keyword) = markup_elem "quasi_keyword";
    2.16  val (operatorN, operator) = markup_elem "operator";
    2.17  val (stringN, string) = markup_elem "string";
    2.18  val (altstringN, altstring) = markup_elem "altstring";
     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Mar 05 16:06:11 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Wed Mar 05 16:13:24 2014 +0100
     3.3 @@ -215,6 +215,7 @@
     3.4    val KEYWORD1 = "keyword1"
     3.5    val KEYWORD2 = "keyword2"
     3.6    val KEYWORD3 = "keyword3"
     3.7 +  val QUASI_KEYWORD = "quasi_keyword"
     3.8    val OPERATOR = "operator"
     3.9    val STRING = "string"
    3.10    val ALTSTRING = "altstring"
     4.1 --- a/src/Tools/jEdit/etc/options	Wed Mar 05 16:06:11 2014 +0100
     4.2 +++ b/src/Tools/jEdit/etc/options	Wed Mar 05 16:13:24 2014 +0100
     4.3 @@ -84,6 +84,7 @@
     4.4  option keyword1_color : string = "006699FF"
     4.5  option keyword2_color : string = "009966FF"
     4.6  option keyword3_color : string = "0099FFFF"
     4.7 +option quasi_keyword_color : string = "66CCFFFF"
     4.8  option caret_invisible_color : string = "50000080"
     4.9  option completion_color : string = "0000FFFF"
    4.10  
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 05 16:06:11 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 05 16:13:24 2014 +0100
     5.3 @@ -239,6 +239,7 @@
     5.4    val keyword1_color = color_value("keyword1_color")
     5.5    val keyword2_color = color_value("keyword2_color")
     5.6    val keyword3_color = color_value("keyword3_color")
     5.7 +  val quasi_keyword_color = color_value("quasi_keyword_color")
     5.8    val caret_invisible_color = color_value("caret_invisible_color")
     5.9    val completion_color = color_value("completion_color")
    5.10  
    5.11 @@ -651,6 +652,7 @@
    5.12        Markup.KEYWORD1 -> keyword1_color,
    5.13        Markup.KEYWORD2 -> keyword2_color,
    5.14        Markup.KEYWORD3 -> keyword3_color,
    5.15 +      Markup.QUASI_KEYWORD -> quasi_keyword_color,
    5.16        Markup.STRING -> Color.BLACK,
    5.17        Markup.ALTSTRING -> Color.BLACK,
    5.18        Markup.VERBATIM -> Color.BLACK,