src/Tools/jEdit/src/jedit/TheoryView.scala
changeset 34445 61ffe9a35f1d
parent 34440 561a6d19bd95
child 34446 5c79f97ec1d1
equal deleted inserted replaced
34444:a245f6cc3105 34445:61ffe9a35f1d
    36         case Phase.FAILED => new Color(255, 192, 192)
    36         case Phase.FAILED => new Color(255, 192, 192)
    37         case _ => Color.red
    37         case _ => Color.red
    38       }
    38       }
    39   }
    39   }
    40 
    40 
    41   def chooseColor(status : String) : Color = {
    41   def chooseColor(status : String): Color = {
    42     //TODO: as properties!
    42     //TODO: as properties!
    43     status match {
    43     status match {
    44       //outer
    44       // logical entities
    45       case "ident" | "command" | "keyword" => Color.blue
    45       case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL
    46       case "verbatim"=> Color.green
    46         | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT
    47       case "comment" => Color.gray
    47         | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255)
    48       case "control" => Color.white
    48       // inner syntax
    49       case "malformed" => Color.red
    49       case Markup.TFREE | Markup.FREE => Color.blue
    50       case "string" | "altstring" => Color.orange
    50       case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green
    51       //logical
    51       case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
    52       case "tclass" | "tycon" | "fixed_decl"  | "fixed"
    52         | Markup.INNER_COMMENT => new Color(255, 128, 128)
    53         | "const_decl" | "const" | "fact_decl" | "fact"
    53       case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
    54         |"dynamic_fact" |"local_fact_decl" | "local_fact"
    54         | Markup.ATTRIBUTE | Markup.METHOD  => Color.yellow
    55         => new Color(255, 0, 255)
    55       // embedded source text
    56       //inner syntax
    56       case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
    57       case "tfree" | "free" => Color.blue
    57         | Markup.DOC_ANTIQ => new Color(0, 192, 0)
    58       case "tvar" | "skolem" | "bound" | "var" => Color.green
    58       // outer syntax
    59       case "num" | "xnum" | "xstr" | "literal" | "inner_comment" => new Color(255, 128, 128)
    59       case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue
    60       case "sort" | "typ" | "term" | "prop" | "attribute" | "method"  => Color.yellow
    60       case Markup.VERBATIM => Color.green
    61         // embedded source
    61       case Markup.COMMENT => Color.gray
    62       case "doc_source"  | "ML_source" | "ML_antic" | "doc_antiq" | "antiq"
    62       case Markup.CONTROL => Color.white
    63         => new Color(0, 192, 0)
    63       case Markup.MALFORMED => Color.red
       
    64       case Markup.STRING | Markup.ALTSTRING => Color.orange
       
    65       // other
    64       case _ => Color.white
    66       case _ => Color.white
    65     }
    67     }
    66   }
    68   }
    67 }
    69 }
    68 
    70