more HTML rendering as in Isabelle/jEdit;
authorwenzelm
Thu Jun 08 23:04:07 2017 +0200 (2017-06-08)
changeset 66044bd7516709051
parent 66043 f704c063e95d
child 66045 f8c4442bb3a9
more HTML rendering as in Isabelle/jEdit;
tuned;
etc/isabelle.css
src/Pure/Isar/token.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/html.ML
src/Pure/Thy/present.scala
     1.1 --- a/etc/isabelle.css	Thu Jun 08 21:17:13 2017 +0200
     1.2 +++ b/etc/isabelle.css	Thu Jun 08 23:04:07 2017 +0200
     1.3 @@ -35,23 +35,30 @@
     1.4  .binding        { color: #336655; }
     1.5  .tfree          { color: #A020F0; }
     1.6  .tvar           { color: #A020F0; }
     1.7 -.free           { color: blue; }
     1.8 +.free           { color: #0000FF; }
     1.9  .skolem         { color: #D2691E; }
    1.10 -.bound          { color: green; }
    1.11 +.bound          { color: #008000; }
    1.12  .var            { color: #00009B; }
    1.13  .numeral        { }
    1.14  .literal        { font-weight: bold; }
    1.15  .delimiter      { }
    1.16 -.inner_string   { color: #FF00CC; }
    1.17 +.inner_numeral  { color: #FF0000; }
    1.18 +.inner_quoted   { color: #FF00CC; }
    1.19  .inner_cartouche { color: #CC6600; }
    1.20  .inner_comment  { color: #CC0000; }
    1.21 +.dynamic        { color: #7BA428; }
    1.22 +.class_parameter_color { color: #D2691E; }
    1.23  
    1.24  .bold           { font-weight: bold; }
    1.25  
    1.26 -.keyword1       { color: #006699; font-weight: bold; }
    1.27 -.keyword2       { color: #009966; font-weight: bold; }
    1.28 -.keyword3       { color: #0099FF; font-weight: bold; }
    1.29 -.operator       { }
    1.30 +.main           { color: #000000; }
    1.31 +.command        { font-weight: bold; }
    1.32 +.keyword        { font-weight: bold; }
    1.33 +.keyword1       { color: #006699; }
    1.34 +.keyword2       { color: #009966; }
    1.35 +.keyword3       { color: #0099FF; }
    1.36 +.quasi_keyword  { color: #9966FF; }
    1.37 +.operator       { color: #323232; }
    1.38  .string         { color: #FF00CC; }
    1.39  .alt_string     { color: #CC00CC; }
    1.40  .verbatim       { color: #6600CC; }
     2.1 --- a/src/Pure/Isar/token.ML	Thu Jun 08 21:17:13 2017 +0200
     2.2 +++ b/src/Pure/Isar/token.ML	Thu Jun 08 23:04:07 2017 +0200
     2.3 @@ -293,6 +293,8 @@
     2.4  fun keyword_markup (important, keyword) x =
     2.5    if important orelse Symbol.is_ascii_identifier x then keyword else Markup.delimiter;
     2.6  
     2.7 +val keyword_properties = Markup.properties [(Markup.kindN, Markup.keywordN)];
     2.8 +
     2.9  fun completion_report tok =
    2.10    if is_kind Keyword tok
    2.11    then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
    2.12 @@ -302,7 +304,8 @@
    2.13    if is_command tok then
    2.14      keyword_reports tok (command_markups keywords (content_of tok))
    2.15    else if is_kind Keyword tok then
    2.16 -    keyword_reports tok [keyword_markup (false, Markup.keyword2) (content_of tok)]
    2.17 +    keyword_reports tok
    2.18 +      [keyword_markup (false, keyword_properties Markup.keyword2) (content_of tok)]
    2.19    else
    2.20      let val (m, text) = token_kind_markup (kind_of tok)
    2.21      in [((pos_of tok, m), text)] end;
     3.1 --- a/src/Pure/PIDE/markup.ML	Thu Jun 08 21:17:13 2017 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Thu Jun 08 23:04:07 2017 +0200
     3.3 @@ -125,7 +125,8 @@
     3.4    val markdown_itemN: string val markdown_item: int -> T
     3.5    val inputN: string val input: bool -> Properties.T -> T
     3.6    val command_keywordN: string val command_keyword: T
     3.7 -  val commandN: string val command: T
     3.8 +  val commandN: string
     3.9 +  val keywordN: string
    3.10    val stringN: string val string: T
    3.11    val alt_stringN: string val alt_string: T
    3.12    val verbatimN: string val verbatim: T
    3.13 @@ -304,7 +305,7 @@
    3.14      (if name = "" then [] else [(nameN, name)]) @ (if kind = "" then [] else [(kindN, kind)]));
    3.15  
    3.16  fun get_entity_kind (name, props) =
    3.17 -  if name = entityN then AList.lookup (op =) props kindN
    3.18 +  if name = entityN then Properties.get props kindN
    3.19    else NONE;
    3.20  
    3.21  val defN = "def";
    3.22 @@ -480,7 +481,9 @@
    3.23  (* outer syntax *)
    3.24  
    3.25  val (command_keywordN, command_keyword) = markup_elem "command_keyword";
    3.26 -val (commandN, command) = markup_elem "command";
    3.27 +
    3.28 +val commandN = "command";
    3.29 +val keywordN = "keyword";
    3.30  val (keyword1N, keyword1) = markup_elem "keyword1";
    3.31  val (keyword2N, keyword2) = markup_elem "keyword2";
    3.32  val (keyword3N, keyword3) = markup_elem "keyword3";
     4.1 --- a/src/Pure/PIDE/markup.scala	Thu Jun 08 21:17:13 2017 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Thu Jun 08 23:04:07 2017 +0200
     4.3 @@ -325,6 +325,7 @@
     4.4    /* outer syntax */
     4.5  
     4.6    val COMMAND = "command"
     4.7 +  val KEYWORD = "keyword"
     4.8    val KEYWORD1 = "keyword1"
     4.9    val KEYWORD2 = "keyword2"
    4.10    val KEYWORD3 = "keyword3"
     5.1 --- a/src/Pure/Thy/html.ML	Thu Jun 08 21:17:13 2017 +0200
     5.2 +++ b/src/Pure/Thy/html.ML	Thu Jun 08 23:04:07 2017 +0200
     5.3 @@ -25,8 +25,9 @@
     5.4  (* common markup *)
     5.5  
     5.6  fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
     5.7 +val enclose_span = uncurry enclose o span;
     5.8  
     5.9 -val hidden = span Markup.hiddenN |-> enclose;
    5.10 +val hidden = enclose_span Markup.hiddenN;
    5.11  
    5.12  
    5.13  (* symbol output *)
    5.14 @@ -85,9 +86,14 @@
    5.15  
    5.16  fun present_span symbols keywords =
    5.17    let
    5.18 +    fun present_markup (name, props) =
    5.19 +      (case Properties.get props Markup.kindN of
    5.20 +        SOME kind =>
    5.21 +          if kind = Markup.commandN orelse kind = Markup.keywordN then enclose_span kind else I
    5.22 +      | NONE => I) #> enclose_span name;
    5.23      fun present_token tok =
    5.24 -      fold_rev (uncurry enclose o span o #1)
    5.25 -        (Token.markups keywords tok) (output symbols (Token.unparse tok));
    5.26 +      fold_rev present_markup (Token.markups keywords tok)
    5.27 +        (output symbols (Token.unparse tok));
    5.28    in implode o map present_token o Command_Span.content end;
    5.29  
    5.30  
     6.1 --- a/src/Pure/Thy/present.scala	Thu Jun 08 21:17:13 2017 +0200
     6.2 +++ b/src/Pure/Thy/present.scala	Thu Jun 08 23:04:07 2017 +0200
     6.3 @@ -104,19 +104,28 @@
     6.4    /* theory document */
     6.5  
     6.6    private val document_span_elements =
     6.7 -    Markup.Elements(Markup.TFREE, Markup.TVAR, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
     6.8 -      Markup.NUMERAL, Markup.LITERAL, Markup.DELIMITER, Markup.INNER_STRING, Markup.INNER_CARTOUCHE,
     6.9 -      Markup.INNER_COMMENT, Markup.COMMAND, Markup.KEYWORD1, Markup.KEYWORD2, Markup.KEYWORD3,
    6.10 -      Markup.QUASI_KEYWORD, Markup.IMPROPER, Markup.OPERATOR, Markup.STRING, Markup.ALT_STRING,
    6.11 -      Markup.VERBATIM, Markup.CARTOUCHE, Markup.COMMENT)
    6.12 +    Markup.Elements(Rendering.text_color.keySet + Markup.NUMERAL + Markup.COMMENT)
    6.13  
    6.14    def make_html(xml: XML.Body): XML.Body =
    6.15      xml map {
    6.16        case XML.Wrapped_Elem(markup, body1, body2) =>
    6.17          XML.Wrapped_Elem(markup, make_html(body1), make_html(body2))
    6.18        case XML.Elem(markup, body) =>
    6.19 -        if (document_span_elements(markup.name)) HTML.span(markup.name, make_html(body))
    6.20 -        else XML.Elem(markup, make_html(body))
    6.21 +        val name = markup.name
    6.22 +        val html =
    6.23 +          markup.properties match {
    6.24 +            case Markup.Kind(kind) if kind == Markup.COMMAND || kind == Markup.KEYWORD =>
    6.25 +              List(HTML.span(kind, make_html(body)))
    6.26 +            case _ =>
    6.27 +              make_html(body)
    6.28 +          }
    6.29 +        Rendering.text_color.get(name) match {
    6.30 +          case Some(c) =>
    6.31 +            HTML.span(c.toString, html)
    6.32 +          case None =>
    6.33 +            if (document_span_elements(name)) HTML.span(name, html)
    6.34 +            else XML.Elem(markup, html)
    6.35 +        }
    6.36        case XML.Text(text) =>
    6.37          XML.Text(Symbol.decode(text))
    6.38      }