# HG changeset patch
# User immler@in.tum.de
# Date 1239812584 -7200
# Node ID 5be7a165a9b9795a895a24ca22ebcbede52c43e1
# Parent  ca43697902b9ecc802a07b04d2e658b7cf1ef3b5
use jEdits styles

diff -r ca43697902b9 -r 5be7a165a9b9 src/Tools/jEdit/build.xml
--- a/src/Tools/jEdit/build.xml	Wed Apr 15 14:25:42 2009 +0200
+++ b/src/Tools/jEdit/build.xml	Wed Apr 15 18:23:04 2009 +0200
@@ -75,7 +75,6 @@
       <copy file="plugin/dockables.xml" todir="${build.classes.dir}" />
       <copy file="plugin/actions.xml" todir="${build.classes.dir}" />
       <copy file="plugin/Isabelle.props" todir="${build.classes.dir}" />
-      <copy file="plugin/styles.props" todir="${build.classes.dir}" />
     </target>
     <target name="-post-jar">
       <!-- jars -->
diff -r ca43697902b9 -r 5be7a165a9b9 src/Tools/jEdit/plugin/styles.props
--- a/src/Tools/jEdit/plugin/styles.props	Wed Apr 15 14:25:42 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-#syntax styles
-options.isabelle.styles.command.foreground=#000080
-options.isabelle.styles.keyword.foreground=#008000
-options.isabelle.styles.fixed_decl.foreground=#080808
-options.isabelle.styles.local_fact_decl.foreground=#080808
-options.isabelle.styles.fact.foreground=#080808
-options.isabelle.styles.method.foreground=#101010
-options.isabelle.styles.literal.foreground=#808000
-options.isabelle.styles.ident.foreground=#C0C000
-options.isabelle.styles.doc_source.foreground=#C00000
-options.isabelle.styles.ML_source.foreground=#C00000
-options.isabelle.styles.malformed=#FF0000
-#ML
-options.isabelle.styles.ML_keyword.foreground=#000080
-options.isabelle.styles.ML_ident.foreground=#000080
-options.isabelle.styles.ML_tvar.foreground=#
-options.isabelle.styles.ML_numeral.foreground=#808000
-options.isabelle.styles.ML_char.foreground=#C0C000
-options.isabelle.styles.ML_string.foreground=#C0C000
-options.isabelle.styles.ML_comment.foreground=#808080
-options.isabelle.styles.ML_malformed.foreground=#FF0000
diff -r ca43697902b9 -r 5be7a165a9b9 src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Apr 15 14:25:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Apr 15 18:23:04 2009 +0200
@@ -19,54 +19,48 @@
 
 object DynamicTokenMarker {
 
-  var styles : Array[SyntaxStyle] = null
-  def reload_styles: Array[SyntaxStyle] = {
-    styles = new Array[SyntaxStyle](256)
-    //jEdit styles
-    for(i <- 0 to Token.ID_COUNT) styles(i) = new SyntaxStyle(Color.black, Color.white, Isabelle.plugin.font)
-    //isabelle styles
-    def from_property(kind : String, spec : String, default : Color) : Color = 
-      try {Color.decode(Isabelle.Property("styles." + kind + "." + spec))} catch {case _ => default}
-
-    for((kind, i) <- kinds) styles(i + FIRST_BYTE) = new SyntaxStyle(
-      from_property(kind, "foreground", Color.black),
-      from_property(kind, "background", Color.white),
-      Isabelle.plugin.font)
-    return styles
+  // Mapping to jEdits token types
+  def choose_byte(kind: String): Byte = {
+    // TODO: as properties
+    kind match {
+      // 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 => Token.DIGIT
+      // inner syntax
+      case Markup.TFREE | Markup.FREE => Token.LITERAL2
+      case Markup.TVAR | Markup.SKOLEM | Markup.BOUND | Markup.VAR => Token.LITERAL3
+      case Markup.NUM | Markup.FLOAT | Markup.XNUM | Markup.XSTR | Markup.LITERAL
+        | Markup.INNER_COMMENT => Token.LITERAL4
+      case Markup.SORT | Markup.TYP | Markup.TERM | Markup.PROP
+        | Markup.ATTRIBUTE | Markup.METHOD => Token.FUNCTION
+      // ML syntax
+      case Markup.ML_KEYWORD => Token.KEYWORD2
+      case Markup.ML_IDENT => Token.KEYWORD3
+      case Markup.ML_TVAR => Token.LITERAL3
+      case Markup.ML_NUMERAL => Token.LITERAL4
+      case Markup.ML_CHAR | Markup.ML_STRING => Token.LITERAL1
+      case Markup.ML_COMMENT => Token.COMMENT1
+      case Markup.ML_MALFORMED => Token.INVALID
+      // embedded source text
+      case Markup.ML_SOURCE | Markup.DOC_SOURCE | Markup.ANTIQ | Markup.ML_ANTIQ
+        | Markup.DOC_ANTIQ => Token.COMMENT4
+      // outer syntax
+      case Markup.IDENT => Token.KEYWORD3
+      case Markup.COMMAND => Token.KEYWORD1
+      case Markup.KEYWORD => Token.KEYWORD2
+      case Markup.VERBATIM => Token.COMMENT1
+      case Markup.COMMENT => Token.COMMENT2
+      case Markup.CONTROL => Token.COMMENT3
+      case Markup.MALFORMED => Token.INVALID
+      case Markup.STRING | Markup.ALTSTRING => Token.LITERAL1
+      // other
+      case _ => 0
+    }
   }
 
-  private final val FIRST_BYTE : Byte = 30
-  val kinds = List(// TODO Markups as Enumeration?
-     // default style
-    null,
-    // logical entities
-    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,
-    // inner syntax
-    Markup.TFREE, Markup.FREE,
-    Markup.TVAR, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
-    Markup.NUM, Markup.FLOAT, Markup.XNUM, Markup.XSTR, Markup.LITERAL,
-    Markup.INNER_COMMENT,
-    Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP,
-    Markup.ATTRIBUTE, Markup.METHOD,
-    // ML syntax
-    Markup.ML_KEYWORD, Markup.ML_IDENT, Markup.ML_TVAR, Markup.ML_NUMERAL,
-    Markup.ML_CHAR, Markup.ML_STRING, Markup.ML_COMMENT, Markup.ML_MALFORMED,
-    // embedded source text
-    Markup.ML_SOURCE, Markup.DOC_SOURCE, Markup.ANTIQ, Markup.ML_ANTIQ,
-    Markup.DOC_ANTIQ,
-    // outer syntax
-    Markup.IDENT, Markup.COMMAND, Markup.KEYWORD, Markup.VERBATIM, Markup.COMMENT,
-    Markup.CONTROL, Markup.MALFORMED, Markup.STRING, Markup.ALTSTRING
-  ).zipWithIndex
-
-  def choose_byte(kind : String) : Byte = (kinds.find (k => kind == k._1)) match {
-    case Some((kind, index)) => (index + FIRST_BYTE).asInstanceOf[Byte]
-    case _ => FIRST_BYTE
-  }
-
-  def choose_color(kind : String) : Color = styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
+  def choose_color(kind : String, styles: Array[SyntaxStyle]) : Color =
+    styles((choose_byte(kind).asInstanceOf[Byte])).getForegroundColor
 
 }
 
diff -r ca43697902b9 -r 5be7a165a9b9 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Apr 15 14:25:42 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Apr 15 18:23:04 2009 +0200
@@ -64,17 +64,6 @@
 
   /* activation */
 
-  Isabelle.plugin.font_changed += (_ => update_styles)
-
-  private def update_styles = {
-    if (text_area != null) {
-      if (Isabelle.plugin.font != null) {
-        text_area.getPainter.setStyles(DynamicTokenMarker.reload_styles)
-        repaint_all
-      }
-    }
-  }
-
   private val selected_state_controller = new CaretListener {
     override def caretUpdate(e: CaretEvent) = {
       val cmd = prover.document.find_command_at(e.getDot)
@@ -90,7 +79,6 @@
     text_area.addLeftOfScrollBar(phase_overview)
     text_area.getPainter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, this)
     buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover))
-    update_styles
     document_actor ! new Text.Change(id(), 0,buffer.getText(0, buffer.getLength),0)
   }
 
@@ -215,7 +203,7 @@
         val finish = to_current(node.stop + e.start)
         if (finish > start && begin < end) {
           encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
-            DynamicTokenMarker.choose_color(node.kind), true)
+            DynamicTokenMarker.choose_color(node.kind, text_area.getPainter.getStyles), true)
         }
       }
     }