src/Tools/Graphview/src/parameters.scala
author wenzelm
Mon, 08 Oct 2012 21:17:20 +0200
changeset 49736 dfa100466d2e
parent 49729 f53a8f73b40f
child 50471 a5930c929b1e
permissions -rw-r--r--
clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     1
/*  Title:      Tools/Graphview/src/parameters.scala
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     2
    Author:     Markus Kaiser, TU Muenchen
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     3
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     4
Visual parameters with fallbacks for non-jEdit-environment.
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     5
*/
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     6
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     7
package isabelle.graphview
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
     8
49558
af7b652180d5 minimal component and build setup for graphview;
wenzelm
parents: 49557
diff changeset
     9
import isabelle._
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    10
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    11
import java.awt.Color
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    12
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    13
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    14
object Parameters
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    15
{
49558
af7b652180d5 minimal component and build setup for graphview;
wenzelm
parents: 49557
diff changeset
    16
  val font_family: String = "IsabelleText"
af7b652180d5 minimal component and build setup for graphview;
wenzelm
parents: 49557
diff changeset
    17
  val font_size: Int = 16
49729
f53a8f73b40f more basic tooltips;
wenzelm
parents: 49572
diff changeset
    18
  val tooltip_font_size: Int = 10
f53a8f73b40f more basic tooltips;
wenzelm
parents: 49572
diff changeset
    19
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    20
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    21
  object Colors {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    22
    val Filter_Colors = List(
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    23
      
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    24
      new Color(0xD9, 0xF2, 0xE2), //blue
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    25
      new Color(0xFF, 0xE7, 0xD8), //orange
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    26
      new Color(0xFF, 0xFF, 0xE5), //yellow
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    27
      new Color(0xDE, 0xCE, 0xFF), //lilac
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    28
      new Color(0xCC, 0xEB, 0xFF), //turquoise
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    29
      new Color(0xFF, 0xE5, 0xE5), //red
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    30
      new Color(0xE5, 0xE5, 0xD9)  //green
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    31
    )
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    32
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    33
    private var curr : Int = -1
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    34
    def next = {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    35
      this.synchronized {
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    36
        curr = (curr + 1) % Filter_Colors.length
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    37
        Filter_Colors(curr)
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    38
      }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    39
    }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    40
    
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    41
    val Default = Color.WHITE
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    42
    val No_Axioms = Color.LIGHT_GRAY
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    43
  }
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    44
  
49736
dfa100466d2e clarified long_names -- conform to usual Isabelle practice of not analysing internal names;
wenzelm
parents: 49729
diff changeset
    45
  var long_names = false
49557
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    46
  var arrow_heads = false
61988f9df94d added Graphview tool, based on Isabelle/Scala and Swing/Graphics2D;
Markus Kaiser <markus.kaiser@in.tum.de>
parents:
diff changeset
    47
}