#!/usr/local/bin/wish  -f
wm geometry . +0+10
wm minsize . 400 400
set w ""
set module "lite"
catch {destroy $w}
frame $w.frame
label $w.frame.label -text "ITL formula:" 
# entry $w.frame.entry -relief sunken -width 70
text $w.frame.entry -width 70
# bind $w.frame.entry <Return>  \
#     {prolog "event verify [$w.frame.entry get]" $module}

frame $w.frame2
button $w.frame2.ok -text "Quit" \
    -command "prolog {event quit 0} $module; destroy $w."
checkbutton $w.frame2.verbose -text "Verbose"   \
    -variable verbose -command \
    {prolog "event verbose $verbose" $module}
# button $w.frame2.verify -text "Verity"   -command \
#     {prolog "event verify [$w.frame.entry get]" $module}
button $w.frame2.verify -text "Verity"   -command \
    {prolog "event verify [$w.frame.entry get 0.0 end]" $module}
button $w.frame2.counter -state disabled \
    -text "Counter Example"   -command "prolog {event counter a} $module"
button $w.frame2.execute -state disabled \
    -text "Execute"   -command "prolog {event execute a} $module"
button $w.frame2.map -text "Map"  -state disabled  -command {
      regexp {([0-9]+)x([0-9]+)} [wm geometry .] dm width height
      set height [expr $height-150]
      prolog "event map $height" $module
      } 
label $w.frame2.state -text "State:" 

set c $w.c
canvas $c -scrollincrement 10  -confine false 
scrollbar $w.vscroll  -relief sunken -command "$c yview"
scrollbar $w.hscroll -orient horiz -relief sunken -command "$c xview"
pack append $w.frame \
	$w.frame.label {left} $w.frame.entry {padx 5 left fillx} 
pack append $w.frame2 \
        $w.frame2.ok {left} \
        $w.frame2.state {padx 5 left expand} \
        $w.frame2.verify {right} \
        $w.frame2.map {right} \
        $w.frame2.counter {right} \
        $w.frame2.execute {right} \
        $w.frame2.verbose {right} 
pack append $w. \
        $w.frame2 {bottom fill pady 5} \
        $w.frame {bottom fill pady 20} \
        $w.hscroll {bottom fillx} $w.vscroll {right filly } \
        $c {top expand fill}
# $c config -xscroll "$w.hscroll set" -yscroll "$w.vscroll set"

  set {symbolicName(entry)} $w.frame.entry
  set {symbolicName(diag)} $w.frame2.counter
  set {symbolicName(execute)} $w.frame2.execute
  set {symbolicName(map)} $w.frame2.map
  set {symbolicName(states)} $w.frame2.state
  set {symbolicName(verify)} $w.frame2.verify
  set {symbolicName(canvas)} $w.c

update

#

# $w.frame2.counter configure -state normal 
# $w.frame2.execute configure -state normal 
# $w.frame2.map configure -state normal 
# proc prolog {a {b user}} {
#    puts "prolog $a $b"
# }