|  | 
 | 
  
    |  | #############################################
 | 
  
    |  | # Configuration file for editor application #
 | 
  
    |  | #############################################
 | 
  
    |  | 
 | 
  
    |  | 
 | 
  
    |  | #
 | 
  
    |  | # Set width and height of sprites
 | 
  
    |  | #
 | 
  
    |  | 
 | 
  
    |  | place_height=40
 | 
  
    |  | place_width=40
 | 
  
    |  | 
 | 
  
    |  | transition_height=40
 | 
  
    |  | transition_width=41
 | 
  
    |  | 
 | 
  
    |  | #
 | 
  
    |  | # Set width and height of page
 | 
  
    |  | #
 | 
  
    |  | 
 | 
  
    |  | page_height=600
 | 
  
    |  | page_width=600
 | 
  
    |  | 
 | 
  
    |  | #
 | 
  
    |  | # Set color of sprites
 | 
  
    |  | # assign a 24 bit hex value (red,green,blue).
 | 
  
    |  | #
 | 
  
    |  | # example (gives green places, and blue transitions)
 | 
  
    |  | #
 | 
  
    |  | #
 | 
  
    |  | #place_fill_color=0x00ff00 
 | 
  
    |  | #transition_fill_color=0xff0000
 | 
  
    |  | #arc_border_color=0x00ff00
 | 
  
    |  | #arc_fill_color=0x32cb41
 | 
  
    |  | #extension_color=0x130347
 |