# HG changeset patch # User wenzelm # Date 1230478829 -3600 # Node ID 61ffe9a35f1d4d2201712fd619eae1f09ef24a47 # Parent a245f6cc3105208899ff1484a8954681f49c55c7 use symbolic Markup elements instead of literal strings; diff -r a245f6cc3105 -r 61ffe9a35f1d src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Dec 28 12:59:27 2008 +0100 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Sun Dec 28 16:40:29 2008 +0100 @@ -38,29 +38,31 @@ } } - def chooseColor(status : String) : Color = { + def chooseColor(status : String): Color = { //TODO: as properties! status match { - //outer - case "ident" | "command" | "keyword" => Color.blue - case "verbatim"=> Color.green - case "comment" => Color.gray - case "control" => Color.white - case "malformed" => Color.red - case "string" | "altstring" => Color.orange - //logical - case "tclass" | "tycon" | "fixed_decl" | "fixed" - | "const_decl" | "const" | "fact_decl" | "fact" - |"dynamic_fact" |"local_fact_decl" | "local_fact" - => new Color(255, 0, 255) - //inner syntax - case "tfree" | "free" => Color.blue - case "tvar" | "skolem" | "bound" | "var" => Color.green - case "num" | "xnum" | "xstr" | "literal" | "inner_comment" => new Color(255, 128, 128) - case "sort" | "typ" | "term" | "prop" | "attribute" | "method" => Color.yellow - // embedded source - case "doc_source" | "ML_source" | "ML_antic" | "doc_antiq" | "antiq" - => new Color(0, 192, 0) + // logical entities + case Markup.TCLASS | Markup.TYCON | Markup.FIXED_DECL | Markup.FIXED | Markup.CONST_DECL + | Markup.CONST | Markup.FACT_DECL | Markup.FACT | Markup.DYNAMIC_FACT + | Markup.LOCAL_FACT_DECL | Markup.LOCAL_FACT => new Color(255, 0, 255) + // inner syntax + case Markup.TFREE | Markup.FREE => Color.blue + case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Color.green + case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL + | Markup.INNER_COMMENT => new Color(255, 128, 128) + case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP + | Markup.ATTRIBUTE | Markup.METHOD => Color.yellow + // embedded source text + case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ + | Markup.DOC_ANTIQ => new Color(0, 192, 0) + // outer syntax + case Markup.IDENT | Markup.COMMAND | Markup.KEYWORD => Color.blue + case Markup.VERBATIM => Color.green + case Markup.COMMENT => Color.gray + case Markup.CONTROL => Color.white + case Markup.MALFORMED => Color.red + case Markup.STRING | Markup.ALTSTRING => Color.orange + // other case _ => Color.white } }