#!/bin/sh
# the next line restarts using tclsh \
TCL_LIBRARY=$SMV_DIR/lib/smv/tcl_library TK_LIBRARY=$SMV_DIR/lib/smv/tk_library TIX_LIBRARY=$SMV_DIR/lib/smv/tix_library  exec $SMV_DIR/lib/smv/tixwish "$0" "$@"

load "$env(SMV_DIR)/lib/libsmv[info sharedlibextension]"
#package require Tix

proc sizeFonts {s} {
    global fontSize 
    global courier
    global helvetica

    set fontSize $s
    font configure $courier -size $s
    font configure $helvetica -size $s
}

if {[string compare $tcl_platform(platform) windows]} {
    if {[catch {set foo $env(VW_SMALL_FONTS)}]} {
	set fontSize 12
	tix configure -fontset 14Point
    } else {
	set fontSize 10
	tix configure -fontset 12Point
    }
} else {
    set fontSize 10
    tix configure -fontset 14Point
}
set courier [font create -family Courier -size $fontSize]
set helvetica [font create -family Helvetica -size $fontSize]

tix option set bold_font {helvetica 12 bold}
tix option set font $courier
tix option set fixed_font $courier



proc selectbox {name height width sb callback} {
    global courier
    frame $name
    if {[string match "" $sb]} {
	scrollbar $name.ysb -orient vertical -command "$name.text yview"
	set the_sb $name.ysb
    } else {
	set the_sb $sb
    }
    text $name.text -state disabled\
	-font $courier -relief raised -borderwidth 2 -height $height -width $width\
	-xscrollcommand "$name.xsb set"\
	-yscrollcommand "$the_sb set"\
	-wrap none -cursor hand2
    scrollbar $name.xsb -orient horizontal -command "$name.text xview"
    bind  $name.text <Button-1> "selectbox_press $name \{$callback\} %x %y"
    if {[string match "" $sb]} {
	pack $name.ysb -side right -fill y
    }
    pack $name.xsb -side bottom -fill x
    pack $name.text -side left -fill both -expand 1
}

proc selectbox_press {name cmd x y} {
    set lc [$name.text index @$x,$y]
    set l [expr [string range $lc 0 [expr [string first . $lc] - 1]] - 1]
    eval "$cmd $l"
}

proc selectbox_insert {name item where} {
    if {[string match end $where]} {
	set idx end
    } else {
	set idx "$where.0"
    }
    $name.text configure -state normal
    $name.text insert $idx "$item\n"
    $name.text configure -state disabled
}

proc selectbox_highlight {name action where} {
    set idx [expr $where + 1]
    $name.text configure -state normal
    $name.text tag $action highlight  $idx.0 $idx.end
    $name.text tag configure highlight -foreground red
    $name.text configure -state disabled
    $name.text see $idx.0
}

proc selectbox_clearhighlight {name} {
    $name.text configure -state normal
    $name.text tag remove highlight  1.0 end
    $name.text configure -state disabled
}

proc selectbox_delete {name from to} {
    if {[string match end $to]} {
	set to end
    } else {
	set to "[expr $to + 1].0"
    }
    $name.text configure -state normal
    $name.text delete [expr $from + 1].0 $to
    $name.text configure -state disabled
}

proc selectbox_get {name where} {
    set l [expr $where + 1]
    $name.text get $l.0 $l.end
}

proc selectbox_unselect {name} {
    $name.text configure -state normal
    $name.text tag remove highlight 1.0 [$name.text index end]
    $name.text configure -state disabled
}

proc selectbox_select {name item} {
    set l [expr $item + 1]
    $name.text configure -state normal
    $name.text tag remove highlight 1.0 [$name.text index end]
    $name.text tag add highlight ${l}.0 ${l}.end
    $name.text tag configure highlight -relief flat -underline 1
    $name.text see ${l}.0
    $name.text configure -state disabled
}


proc browsebox_extend {name callback} {
    global browsebox_
    set l $browsebox_($name)
    set n [llength $l]
    set b $name.s$n
    catch {destroy $b}
    set c [eval "$callback \{[browsebox_translate $name $l]\}"]
    if {[llength $c] > 0} {
	selectbox $b 20 20 "" "browsebox_click $name \{$callback\} $n"
	pack $b -side left -fill both -expand 1
	foreach x $c {
	    selectbox_insert $b $x end
	}
    }
}

proc browsebox_click {name callback which where} {
    global browsebox_
    set n 0
    set l ""
    selectbox_select $name.s$which $where
    foreach x $browsebox_($name) {
	if {$n == $which} {
	    lappend l $where
	} elseif {$n < $which} {
	    lappend l $x
	} else {
	    destroy $name.s$n
	}
	incr n
    }
    if {$n == $which} {lappend l $where} else {
	catch {destroy $name.s$n}
    }
    set browsebox_($name) $l
    browsebox_extend $name $callback
}

proc browsebox_translate {name idxs} {
    set n 0
    set l ""
    foreach x $idxs {
	lappend l [selectbox_get $name.s$n $x]
	incr n
    }
    return $l
}

proc browsebox_selection {name} {
    global browsebox_
    browsebox_translate $name $browsebox_($name)
}
	
proc browsebox {name callback} {
    global browsebox_
    set browsebox_($name) ""
    frame $name
    browsebox_extend $name $callback
}
    
proc get_dir {l} {
    set n [pwd]/
    foreach x $l {
	append n $x
    }
    if {[string match "*/" $n]} {
	if {[catch {set c [exec ls -aF $n]}]} {
	    return ""
	} else {
	    return $c
	}
    }
    return ""
}
#first line



# dialog.tcl --
#
# This file defines the procedure tk_dialog, which creates a dialog
# box containing a bitmap, a message, and one or more buttons.
#
# @(#) dialog.tcl 1.12 94/12/23 11:15:43
#
# Copyright (c) 1992-1993 The Regents of the University of California.
# Copyright (c) 1994 Sun Microsystems, Inc.
#
# See the file "license.terms" for information on usage and redistribution
# of this file, and for a DISCLAIMER OF ALL WARRANTIES.
#

#
# tk_dialog:
#
# This procedure displays a dialog box, waits for a button in the dialog
# to be invoked, then returns the index of the selected button.
#
# Arguments:
# w -		Window to use for dialog top-level.
# title -	Title to display in dialog's decorative frame.
# text -	Message to display in dialog.
# bitmap -	Bitmap to display in dialog (empty string means none).
# default -	Index of button that is to display the default ring
#		(-1 means none).
# args -	One or more strings to display in buttons across the
#		bottom of the dialog box.

proc tk_dialog {w title text bitmap default args} {
    global tkPriv

    set oldFocus [focus]

    # 1. Create the top-level window and divide it into top
    # and bottom parts.

    catch {destroy $w}
    toplevel $w -class Dialog
    wm title $w $title
    wm iconname $w Dialog
    wm protocol $w WM_DELETE_WINDOW { }
    wm transient $w [winfo toplevel [winfo parent $w]]
    frame $w.top -relief raised -bd 1
    pack $w.top -side top -fill both
    frame $w.bot -relief raised -bd 1
    pack $w.bot -side bottom -fill both

    # 2. Fill the top part with bitmap and message.

    label $w.msg -wraplength 3i -justify left -text $text \
	    -font -Adobe-Times-Medium-R-Normal--*-140-*-*-*-*-*-*
    pack $w.msg -in $w.top -side right -expand 1 -fill both -padx 3m -pady 3m
    if {$bitmap != ""} {
	label $w.bitmap -bitmap $bitmap
	pack $w.bitmap -in $w.top -side left -padx 3m -pady 3m
    }

    # 3. Create a row of buttons at the bottom of the dialog.

    set i 0
    foreach but $args {
	button $w.button$i -text $but -command "set tkPriv(button) $i"
	if {$i == $default} {
	    frame $w.default -relief sunken -bd 1
	    raise $w.button$i $w.default
	    pack $w.default -in $w.bot -side left -expand 1 -padx 3m -pady 2m
	    pack $w.button$i -in $w.default -padx 2m -pady 2m
	    bind $w <Return> "$w.button$i flash; set tkPriv(button) $i"
	} else {
	    pack $w.button$i -in $w.bot -side left -expand 1 \
		    -padx 3m -pady 2m
	}
	incr i
    }

    # 4. Withdraw the window, then update all the geometry information
    # so we know how big it wants to be, then center the window in the
    # display and de-iconify it.

    wm withdraw $w
    update idletasks
    set x [expr [winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
	    - [winfo vrootx [winfo parent $w]]]
    set y [expr [winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
	    - [winfo vrooty [winfo parent $w]]]
    wm geom $w +$x+$y
    wm deiconify $w

    # 5. Set a grab and claim the focus too.

    grab $w
    tkwait visibility $w
    if {$default >= 0} {
	focus $w.button$default
    } else {
	focus $w
    }

    # 6. Wait for the user to respond, then restore the focus and
    # return the index of the selected button.

    tkwait variable tkPriv(button)
    destroy $w
    focus $oldFocus
    return $tkPriv(button)
}

proc string_dialog {w title text bitmap init_value default args} {
    global tkPriv

    set oldFocus [focus]

    # 1. Create the top-level window and divide it into top
    # and bottom parts.

    catch {destroy $w}
    toplevel $w -class Dialog
    wm title $w $title
    wm iconname $w Dialog
    wm protocol $w WM_DELETE_WINDOW { }
    #wm transient $w [winfo toplevel [winfo parent $w]]
    frame $w.top -relief raised -bd 1
    pack $w.top -side top -fill both
    frame $w.ent -relief raised -bd 1
    pack $w.ent -side top -fill both
    frame $w.bot -relief raised -bd 1
    pack $w.bot -side bottom -fill both

    # 2. Fill the top part with bitmap and message.

    label $w.msg -wraplength 3i -justify left -text $text \
	    -font -Adobe-Times-Medium-R-Normal--*-140-*-*-*-*-*-*
    pack $w.msg -in $w.top -side right -expand 1 -fill both -padx 3m -pady 3m
    if {$bitmap != ""} {
	label $w.bitmap -bitmap $bitmap
	pack $w.bitmap -in $w.top -side left -padx 3m -pady 3m
    }

    entry $w.ent.entry -width 80
    pack  $w.ent.entry -side left -fill x
    $w.ent.entry selection from end
    $w.ent.entry insert end $init_value
    $w.ent.entry selection to end


    # 3. Create a row of buttons at the bottom of the dialog.

    set i 0
    foreach but $args {
	button $w.button$i -text $but -command "set tkPriv(button) $i"
	if {$i == $default} {
	    frame $w.default -relief sunken -bd 1
	    raise $w.button$i $w.default
	    pack $w.default -in $w.bot -side left -expand 1 -padx 3m -pady 2m
	    pack $w.button$i -in $w.default -padx 2m -pady 2m
	    bind $w <Return> "$w.button$i flash; set tkPriv(button) $i"
	} else {
	    pack $w.button$i -in $w.bot -side left -expand 1 \
		    -padx 3m -pady 2m
	}
	incr i
    }

    # 4. Withdraw the window, then update all the geometry information
    # so we know how big it wants to be, then center the window in the
    # display and de-iconify it.

    wm withdraw $w
    update idletasks
    set x [expr [winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
	    - [winfo vrootx [winfo parent $w]]]
    set y [expr [winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
	    - [winfo vrooty [winfo parent $w]]]
    wm geom $w +$x+$y
    wm deiconify $w

    # 5. Set a grab and claim the focus too.

    grab $w
    tkwait visibility $w
#    if {$default >= 0} {
#	focus $w.button$default
#    } else {
#	focus $w
#    }
    focus $w.ent.entry

    # 6. Wait for the user to respond, then restore the focus and
    # return the index of the selected button.

    tkwait variable tkPriv(button)
    set foo [$w.ent.entry get]
    destroy $w
    focus $oldFocus
    return [list $tkPriv(button) $foo]
}

proc noop {x} {
  return $x
}

proc options_dialog {w options} {
    global tkPriv
    global options_hash

    set oldFocus [focus]

    # 1. Create the top-level window

    catch {destroy $w}
    toplevel $w -class Dialog
    wm title $w "SMV options"
    wm iconname $w Dialog
    wm protocol $w WM_DELETE_WINDOW { }
    #wm transient $w [winfo toplevel [winfo parent $w]]
    frame $w.top -relief raised -bd 1
    pack $w.top -side top -fill both
    frame $w.bot -relief raised -bd 1
    pack $w.bot -side bottom -fill both

    # 2. Fill the top part with buttons and entries

    set i 0
    set cmds ""
    set nb $w.top.nb
    tixNoteBook $nb -ipadx 2 -ipady 2
    $nb add 1 -label General -underline 0
    $nb add 2 -label BDD -underline 2 -raisecmd {global propslist; focus [$propslist subwidget hlist]}
    $nb add 3 -label SAT -underline 2 -raisecmd {global propslist; focus [$propslist subwidget hlist]}
    pack $nb -expand yes -fill both -padx 2 -pady 2 -side top

    foreach option $options {
       set name [lindex $option 0]
       set class [lindex $option 5]
       set nf $nb.nbframe.$class
       if {[lindex $option 2] == 0} {
         global temp$name
	 set temp$name 0
         set temp$name [lindex $option 4]
	  frame $nf.frame$i
 	checkbutton $nf.frame$i.button -text [lindex $option 3]\
           -variable temp$name -onvalue 1 -offvalue 0  
	pack $nf.frame$i.button -side left
        pack $nf.frame$i -side top  -anchor w -fill x

	lappend cmds "set options_hash($name) \$temp$name"
	} else {	
        if {[lindex $option 2] == 1} {
	  frame $nf.frame$i
	  entry $nf.frame$i.entry -width 10
          label $nf.frame$i.label -text [lindex $option 3]
	  pack  $nf.frame$i.label -side left
	  pack  $nf.frame$i.entry -side left -fill x -expand 1
	  pack $nf.frame$i -side top  -anchor w -fill x
          $nf.frame$i.entry insert 0 [lindex $option 4]
          lappend cmds "set options_hash($name) \[$nf.frame$i.entry get\]"
        }
        }
        set i [expr $i + 1]
     }

    # 3. Create a row of buttons at the bottom of the dialog.

     button $w.bot.b1 -text "OK" -command "set tkPriv(button) 1"
	pack $w.bot.b1 -side left -padx 2 -pady 2
     button $w.bot.b2 -text "Cancel" -command "set tkPriv(button) 0"
	pack $w.bot.b2 -side left -padx 2 -pady 2

    # 4. Withdraw the window, then update all the geometry information
    # so we know how big it wants to be, then center the window in the
    # display and de-iconify it.

    wm withdraw $w
    update idletasks
    set x [expr [winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
	    - [winfo vrootx [winfo parent $w]]]
    set y [expr [winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
	    - [winfo vrooty [winfo parent $w]]]
    wm geom $w +$x+$y
    wm deiconify $w

    # 5. Set a grab and claim the focus too.

    grab $w
    tkwait visibility $w
    focus $w

    # 6. Wait for the user to respond, then restore the focus and
    # return the index of the selected button.

    tkwait variable tkPriv(button)
    if {$tkPriv(button)} {
	foreach cmd $cmds {
           eval "$cmd"
        }
	smv_setOptions [make_options_from_hash $options]
    }
    catch {destroy $w}
    focus $oldFocus
}







proc list_dialog {w title text bitmap choices} {
    global tkPriv

    set oldFocus [focus]

    # 1. Create the top-level window and divide it into top
    # and bottom parts.

    catch {destroy $w}
    toplevel $w -class Dialog
    wm title $w $title
    wm iconname $w Dialog
    wm protocol $w WM_DELETE_WINDOW { }
    wm transient $w [winfo toplevel [winfo parent $w]]
    frame $w.top -relief raised -bd 1
    pack $w.top -side top -fill both
    frame $w.mid -relief raised -bd 1
    pack $w.mid -side top -fill both -expand 1
    frame $w.bot -relief raised -bd 1
    pack $w.bot -side bottom -fill both

    # 2. Fill the top part with bitmap and message.

    label $w.msg -wraplength 3i -justify left -text $text \
	    -font -Adobe-Times-Medium-R-Normal--*-140-*-*-*-*-*-*
    pack $w.msg -in $w.top -side right -expand 1 -fill both -padx 3m -pady 3m
    if {$bitmap != ""} {
	label $w.bitmap -bitmap $bitmap
	pack $w.bitmap -in $w.top -side left -padx 3m -pady 3m
    }


#########################################################################

    set thelist $w.mid.lb

    set theopts {
	hlist.columns 1
	hlist.header  false
	hlist.separator "\n"
    }
    lappend theopts hlist.font
    global helvetica
    lappend theopts $helvetica
    
    tixScrolledHList $thelist -options $theopts

    pack $thelist -expand yes -fill both -padx 3 -pady 3 -side left
 
    set thehlist [$thelist subwidget hlist]

    foreach x $choices {
	$thehlist add $x -itemtype text -text $x
    }


#########################################################################



    if {0} {
	# make a listbox in the middle
	
	listbox $w.mid.lb -relief raised -borderwidth 2 \
	    -yscrollcommand "$w.mid.sb set" 
	scrollbar $w.mid.sb -command "$w.mid.lb yview"
	pack $w.mid.sb -side right -fill y
	pack $w.mid.lb -side left -fill both -expand 1
	
	
	foreach x $choices {
	    $w.mid.lb insert end $x
	}
	$w.mid.lb selection set 0 
    }

##########################


    # 3. Create a row of buttons at the bottom of the dialog.

    set i 0
    set default 0
    foreach but "Choose Cancel" {
	button $w.button$i -text $but -command "set tkPriv(button) $i"
	if {$i == $default} {
	    frame $w.default -relief sunken -bd 1
	    raise $w.button$i $w.default
	    pack $w.default -in $w.bot -side left -expand 1 -padx 3m -pady 2m
	    pack $w.button$i -in $w.default -padx 2m -pady 2m
	    bind $w <Return> "$w.button$i flash; set tkPriv(button) $i"
	} else {
	    pack $w.button$i -in $w.bot -side left -expand 1 \
		    -padx 3m -pady 2m
	}
	incr i
    }

    # 4. Withdraw the window, then update all the geometry information
    # so we know how big it wants to be, then center the window in the
    # display and de-iconify it.

    wm withdraw $w
    update idletasks
    set x [expr [winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
	    - [winfo vrootx [winfo parent $w]]]
    set y [expr [winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
	    - [winfo vrooty [winfo parent $w]]]
    wm geom $w +$x+$y
    wm deiconify $w

    # 5. Set a grab and claim the focus too.

    grab $w
    tkwait visibility $w
    if {$default >= 0} {
	focus $w.button$default
    } else {
	focus $w
    }

    # 6. Wait for the user to respond, then restore the focus and
    # return the index of the selected button.

    while {1} {
      tkwait variable tkPriv(button)
	if {0} {
	    set sel [$w.mid.lb curselection]
	    if {[string length $sel] == 0} {
		if {$tkPriv(button) != 0} {
		    destroy $w
		    focus $oldFocus
		    return ""
		}
	    } else {
		set res [$w.mid.lb get $sel]
		destroy $w
		focus $oldFocus
		return $res
	    }
	} else {
	    if {$tkPriv(button) != 0} {
		    destroy $w
		    focus $oldFocus
		    return ""
	    }
	    set sel [$thehlist info anchor]
	    if {[string length $sel] > 0} {
		destroy $w
		focus $oldFocus
		return $sel
	    }
	}
    }
}

proc error_dialog {msg} {
    tk_messageBox -icon error -message $msg -type ok -parent .
}

# This is the expl user interface

set signals_list ""
set cur_file ""
set moded 0



proc LoadFile {n} {
  global source_text
  $source_text configure -state normal
  $source_text delete 1.0 end

  set name $n
  if {[catch {set f [open $name]}]} {
    $source_text insert end "cannot open $name"
  } else {
    while {![eof $f]} {
      $source_text insert end [read $f 1000]
    }
    close $f
  }
  $source_text configure -state disabled
  global cur_file
  set cur_file $n
}


proc SetFile {f l} {
    global cur_file
    global cur_line
    if {[string compare $f $cur_file] != 0} {
	LoadFile $f
    }
    set cur_line $l
    global source_text
    $source_text tag remove highlight 1.0 [$source_text index end]
    $source_text tag add highlight ${l}.0 [expr $l + 1].0
    $source_text tag configure highlight -background cyan2
    $source_text see ${l}.0
    # this is for emacs. in case emacs is confused about the current working
    # directory, make an absolute pathname.
    if {[string compare [string index $f 0] /]} {
	set f [pwd]/$f
    }
    global env
    if {![catch {set foo $env(VW_EMACS)}]} {
	puts "\032\032${f}:${l}:"
    }
}

proc get_results {} {
    global results
    global result_index
    global the_traces
    if {[catch {
	if {[file mtime [smv_extension out]] > [smv_modTime]} {
	    smv_restoreResults
	    set results [smv_summarize]
	    catch {unset result_index}
	    set count 0
	    foreach x $results {
		set result_index([lindex $x 0]) $count
		incr count
	    }
	} else {
	    set results ""
	}
    }]} {
	set results ""
    }
}  

proc my_write_using {} {
  global moded
  set moded 0
  smv_save
}

proc RunSmvBatch {all} {
    global smv_file_name
    global batch_log
    global the_props
    global courier
    
    if {[catch {check_mod_time}]} {return}
    my_write_using
    set w $batch_log(frame)
    
    $w.text delete 1.0 end
    eval $batch_log(raise)
    update

    if {$all == 2} {
	if {[string length $the_props] != 0} {
	    set batch_log(file) [smv_exec smv -r -force -only -check [lindex $the_props 0]\
				  $smv_file_name]
	} else {
	    set batch_log(file) [smv_exec smv -trav -r -force $smv_file_name]
	}
    } elseif {!$all && [string length $the_props] != 0} {
	set batch_log(file) [smv_exec smv -all -only -check [lindex $the_props 0]\
				  $smv_file_name]
    } else {
	set batch_log(file) [smv_exec smv $smv_file_name]
    }
    
    fconfigure $batch_log(file) -blocking 0
    fileevent $batch_log(file) readable {bg_input}
}

proc bg_input {} {
    global batch_log
    set w $batch_log(frame)
    $w.text insert end [read $batch_log(file) 1000]
    $w.text see end
    update idletasks
    if {[eof $batch_log(file)]} {
	close $batch_log(file)
	if {[catch {smv_wait} msg]} {
	    if {[scan $msg { "%[^\"]", line %d:} f l] == 2} {
		show_error $msg
	    } else {
		tk_messageBox -icon error -type ok \
		    -title "Error" -parent .\
		    -message $msg
	    }
	} else {
#	    after idle {
#		set OldFocus [focus]
#		puts "old focus: $OldFocus"
		tk_messageBox -icon info -type ok \
		    -title Confirm -parent .\
		    -message "Verification finished"
#		focus $OldFocus
#		wm withdraw .
#		wm deiconify .
#	    }
	    eval $batch_log(raise)
	    get_results
	}
	set batch_log(file) ""
    }
}


proc RunSmvProcess {} {
    global smv_file_name
    if {[catch {check_mod_time}]} {return}
  my_write_using
  if {[catch {eval "exec smv $smv_file_name >@stdout"} msg]} {
    tk_dialog .d "SMV Error" \
       $msg \
       warning 0 "OK"
    if {[scan $msg { "%[^"]", line %d:} f l] == 2} { 
      SetFile $f $l
    }
    return
  }
  get_results
}  

proc RunSmv {} {
  global results

    if {[catch {check_mod_time}]} {return}
  my_write_using
  smv_verify
  smv_saveResults
  set results [smv_summarize]
}  

proc SetClosedSignals {} {
    global have_model
    if {$have_model} {
	sigtree_flash
    }
}

proc revert_using {} {
    global moded
    smv_restore
    set moded 0
    global the_props
    set the_props $the_props
}

proc my_save {} {
  global moded

  if {$moded} {
    set ans [tk_dialog .d "File Modified" \
       "Save changes to abstraction?" \
       warning 0 "Save" "Don't save" "Cancel"]
    if {$ans == 0} {
       my_write_using
       return 1
    }
    if {$ans == 1} {
	return 1
    }
    return 0
  }
  return 1
}

proc my_quit {} {
    global moded
    global have_model
    global tracegrid
    
    if {!$have_model} {exit}
    if {[check_background]} {return}
    if {[my_save]} {
	catch {
	    if {$tracegrid(show_all)} {
		file delete [smv_extension traces]
	    } else {
		tracegrid_save_view [smv_extension traces]
	    }
	}
	smv_quit
	exit
    }
}


set trace_scale 6
set tracesShowAll 1

proc set_scale {s} {
  global trace_scale
  global trace_index
  global the_traces
  global result_count
    global tracesShowAll
  set trace_scale $s
  set where [lindex [.p.p2.nb.nbframe.traces.names.l yview] 0]
    if {!$tracesShowAll} {
	set l [.p.p2.nb.nbframe.traces.names.l get 1.0 end]
    }
    .p.p2.nb.nbframe.traces.names.l configure -state normal
    .p.p2.nb.nbframe.traces.values.l configure -state normal
  .p.p2.nb.nbframe.traces.names.l delete 1.0 end
  .p.p2.nb.nbframe.traces.values.l delete 1.0 end
    .p.p2.nb.nbframe.traces.names.l configure -state disabled
    .p.p2.nb.nbframe.traces.values.l configure -state disabled
    if {$tracesShowAll} {
	catch {foreach x [smv_trace $the_traces .] {make_trace $x}}
    } else {
	foreach x  $l {
	    if {$result_count} {
		set traces [smv_trace $the_traces $x]
		if {[llength $traces] > 0 && \
			[string compare [lindex [lindex $traces 0] 0] $x] == 0} {
		    make_trace [lindex $traces 0]
		} else {make_trace [list $x {}]}
	    } else {make_trace [list $x {}]}
	}
    }
    .p.p2.nb.nbframe.traces.names.l yview moveto $where
    .p.p2.nb.nbframe.traces.values.l yview moveto $where
    highlight_current_state
}

proc save_traces {filename} {
    if {[catch {set file [open $filename w]} msg]} {
	tk_dialog .d "Error" \
	    $msg \
	    warning 0 "OK"
	return
    }
    set l [.p.p2.nb.nbframe.traces.names.l get 1.0 end]
    foreach x  $l {
	puts $file $x
    }
    close $file
}

proc tracegrid_see {r} {
    global tracegrid
    set fracs [$tracegrid(g) yview]
    set topfrac [lindex $fracs 0]
    set botfrac [lindex $fracs 1]
    set rtopfrac [expr (($r - 2) * 1.0) / $tracegrid(size)]
    set rbotfrac [expr (($r + 2) * 1.0) / $tracegrid(size)]
    if {$rtopfrac < $topfrac} {
	$tracegrid(g) yview moveto $rtopfrac
    } elseif {$rbotfrac > $botfrac} {
	$tracegrid(g) yview moveto [expr $rbotfrac - ($botfrac - $topfrac)]
    }
}

proc tracegrid_see_one {x view i} {
    global tracegrid
    set fracs [$tracegrid(g) $view]
    set topfrac [lindex $fracs 0]
    set botfrac [lindex $fracs 1]
    set max [lindex [$tracegrid(g) index max max] $i]
    set rtopfrac [expr (($x - 2) * 1.0) / $max]
    set rbotfrac [expr (($x + 2) * 1.0) / $max]
    if {$rtopfrac < $topfrac} {
	$tracegrid(g) $view moveto $rtopfrac
    } elseif {$rbotfrac > $botfrac} {
	$tracegrid(g) $view moveto [expr $rbotfrac - ($botfrac - $topfrac)]
    }
}

proc tracegrid_see_both {x y} {
    tracegrid_see_one $x xview 0
    tracegrid_see_one $y yview 1
}

proc tracegrid_get_signals {} {
    global tracegrid
    set res {}
    set i 1
    while {$i <= $tracegrid(size)} {
	lappend res [$tracegrid(g) entrycget 0 $i -text]
	incr i
    }
    return $res
}

proc tracegrid_save_view {filename} {
    if {[catch {set file [open $filename w]} msg]} {
	tk_dialog .d "Error" \
	    $msg \
	    warning 0 "OK"
	return
    }
    set l [tracegrid_get_signals]
    foreach x  $l {
	puts $file $x
    }
    close $file
}

proc restore_traces {filename complain} {
    global tracesShowAll
    if {!$tracesShowAll} {
	if {[catch {set file [open $filename r]} msg]} {
	    if {$complain} {
		tk_dialog .d "Error" \
		    $msg \
		    warning 0 "OK"
	    }
	    return
	}
	.p.p2.nb.nbframe.traces.names.l configure -state normal
	.p.p2.nb.nbframe.traces.values.l configure -state normal
	.p.p2.nb.nbframe.traces.names.l delete 1.0 end
	.p.p2.nb.nbframe.traces.values.l delete 1.0 end

	while {![eof $file]} {
	    set n [string trim [gets $file]]
	    if {[string length $n] > 0} {
		.p.p2.nb.nbframe.traces.names.l insert end "$n\n"
	    }
	}
	.p.p2.nb.nbframe.traces.names.l configure -state disabled
	.p.p2.nb.nbframe.traces.values.l configure -state disabled
	close $file
    }
    global trace_scale
    set_scale $trace_scale
}

proc tracegrid_restore_view {filename complain} {
    if {[catch {set file [open $filename r]} msg]} {
	if {$complain} {
	    tk_dialog .d "Error" \
		$msg \
		warning 0 "OK"
	}
	return
    }
    set sigs {}
    while {![eof $file]} {
	set n [string trim [gets $file]]
	if {[string length $n] > 0} {
	    lappend sigs $n
	}
    }
    close $file
    tracegrid_refresh $sigs
}


proc lastn {s n} {
  set f  [expr [string length $s] - $n]
  set l [expr $f + $n - 1]
  return [string range $s $f $l ]
}

set result_count 0
set trace_count 0
set current_result 0
set loop_back 0

proc add_trace_value {t} {
  global trace_scale
  global loop_back
  set i 1
  set s ""	
  foreach x [lrange $t 0 [expr [llength $t] - 1]] {
    if {$i == $loop_back} {
      append s "|: "
    }
    append s [lastn [format "%${trace_scale}s " $x] ${trace_scale}]
    incr i
  }
    if {$loop_back} {
	append s ":|"
    }
    .p.p2.nb.nbframe.traces.values.l insert end "$s\n"
}


proc make_trace {t} {
  global trace_count
  global trace_scale
  set trace_count [expr $trace_count+1]
  set myname  [lindex $t 0]
    .p.p2.nb.nbframe.traces.names.l configure -state normal
    .p.p2.nb.nbframe.traces.values.l configure -state normal
  .p.p2.nb.nbframe.traces.names.l insert end "$myname\n"
  add_trace_value [lindex $t 1]
    .p.p2.nb.nbframe.traces.names.l configure -state disabled
    .p.p2.nb.nbframe.traces.values.l configure -state disabled
}
  
set the_traces ""
set current_state 0
set trace_selection 0
set trace_selection_name ""


proc highlight_current_state {} {
    global trace_scale
    global current_state
    global trace_selection
    .p.p2.nb.nbframe.traces.names.l configure -state normal
    .p.p2.nb.nbframe.traces.values.top configure -state normal
    .p.p2.nb.nbframe.traces.names.l configure -state normal

    .p.p2.nb.nbframe.traces.values.top tag remove highlight 1.0 [.p.p2.nb.nbframe.traces.values.top index end]
    .p.p2.nb.nbframe.traces.values.top tag add highlight 1.[expr $current_state * $trace_scale] \
	1.[expr $current_state * $trace_scale + $trace_scale]
    .p.p2.nb.nbframe.traces.values.top tag configure highlight -foreground white -background black
    .p.p2.nb.nbframe.traces.values.l tag remove highlight 1.0 [.p.p2.nb.nbframe.traces.values.l index end]
    .p.p2.nb.nbframe.traces.values.l tag remove lowlight 1.0 [.p.p2.nb.nbframe.traces.names.l index end]
    .p.p2.nb.nbframe.traces.values.l tag add highlight [expr $trace_selection+1].0\
	[expr $trace_selection+2].0
    .p.p2.nb.nbframe.traces.values.l tag configure highlight -foreground black -background white
    .p.p2.nb.nbframe.traces.names.l tag remove highlight 1.0 [.p.p2.nb.nbframe.traces.names.l index end]
    .p.p2.nb.nbframe.traces.names.l tag add highlight [expr $trace_selection+1].0\
	[expr $trace_selection+2].0
    .p.p2.nb.nbframe.traces.names.l tag configure highlight -foreground black -background white
    .p.p2.nb.nbframe.traces.values.l tag remove highlight\
	[expr $trace_selection+1].[expr $current_state * $trace_scale]\
	[expr $trace_selection+1].[expr $current_state * $trace_scale + $trace_scale]
    .p.p2.nb.nbframe.traces.values.l tag add lowlight\
	[expr $trace_selection+1].[expr $current_state * $trace_scale]\
	[expr $trace_selection+1].[expr $current_state * $trace_scale + $trace_scale]
    .p.p2.nb.nbframe.traces.values.l tag configure lowlight -foreground white -background black


    .p.p2.nb.nbframe.traces.names.l configure -state disabled
    .p.p2.nb.nbframe.traces.values.top configure -state disabled
    .p.p2.nb.nbframe.traces.names.l configure -state disabled
}

proc make_traces1 {index } {
    global the_traces
    global loop_back
    global results
    global trace_scale
    if {$index >= 0} {
	set loop_back [lindex [lindex $results $index] 3]
	set name [lindex [lindex $results $index] 0]
	choose_prop [list $name]
    } else {set loop_back "0"}
    if {[string compare $the_traces ""]} {
	set the_traces $index
    } else {
	set the_traces $index
	global tracegrid
	if {!$tracegrid(show_all)} {
	    tracegrid_restore_view [smv_extension traces] 0
	}
    }
    return
}

proc make_traces {index} {
    global current_state
    set current_state 0
    make_traces1 $index
}

set results ""

trace variable the_props w prop_update_result

proc prop_update_result {name1 name2 op} {
    after idle {
	global results
	global result_index
	global the_props
	
	
	if {[string compare $results ""]} {
	    if {[catch {
		set i $result_index([lindex $the_props 0])
	    }]} {set i -2}
	    if {$i != $the_traces} {
		make_traces $i
	    }
	}
    }
}


proc make_result {t} {
    global result_count
    set prop [lindex $t 0]
    if {[string compare $prop "."] == 0} {
	set prop [lindex $t 1]
    }
    global resultslist
    [$resultslist subwidget hlist] add $result_count -itemtype text -text $prop
    if {[lindex $t 2] == 1} {set val true} else {set val false}
    [$resultslist subwidget hlist] item create $result_count 1 -itemtype text -text $val
    set rtime [lindex $t 5]
    if {$rtime != 0} {
        [$resultslist subwidget hlist] item create $result_count 2 -itemtype text -text [clock format $rtime]
    }
}

set exists_results 0

proc trace_yview args {
  eval ".p.p2.nb.nbframe.traces.names.l yview $args"
  eval ".p.p2.nb.nbframe.traces.values.l yview $args"
}

proc results_yview args {
  eval ".p.p1.nb.nbframe.results.names.l yview $args"
  eval ".p.p1.nb.nbframe.results.values.l yview $args"
}

proc view_depend {s} {
    global the_traces
    global trace_index
    set dl [get_depend $s]
    foreach x  "$dl" {
      set foo ""
      catch {set foo $trace_index(${x})}
      if {[string compare $foo ""] != 0} {
         make_trace [lindex $the_traces $foo]
      }
    }
  .p.p2.nb.nbframe.traces.names.l see end
  .p.p2.nb.nbframe.traces.values.l see end
}

proc resultslist_no_filter {t} {
  return 1
}

proc resultslist_current_filter {t} {
    return [expr [lindex $t 5] >= [smv_modTime]]
}
				 
proc resultslist_property_filter {t} {
    global the_props
    return [expr ![string compare [lindex $the_props 0] [lindex $t 0]]]
}


proc make_results {l} {
    global exists_results
    global result_count
    global trace_scale
    global resultslist
    global resultslist_filter
    [$resultslist subwidget hlist] delete all
    set result_count 0
    foreach t "$l" {
	if {[$resultslist_filter $t]} {
	    make_result $t
	}
        set result_count [expr $result_count+1]
    }
}


trace variable results w results_update

proc results_update {name1 name2 op} {
    after idle {
	global results
        global exists_results
        global result_count
        global trace_scale
        global resultslist
	make_results $results
        if {$result_count} {
   	    set lastres [expr $result_count - 1]
	    [$resultslist subwidget hlist] selection set $lastres
	    make_traces $lastres
        } else {
	    global the_traces
	    set the_traces ""
        }
        #  set_scale $trace_scale
        set exists_results 1
	if {[llength $results] > 0} {
	  .p.p1.nb raise results
	}
    }
}

proc my_abs_mode {} {
  if {[string compare [get_abs_mode] "Abstraction"] == 0} {
    set state normal
  } else {
    set state disabled
  }
  set_abs_mode [get_abs_mode]
  SetClosedSignals
  .mbar.absb.menu configure -state $state
}


if {[llength $argv] > 1} {
    puts "syntax: vw \[filename\]\n"
    exit 1
}
set smv_file_name [lindex $argv 0]


if {![string compare $smv_file_name ""]} {
    catch {cd $env(SMVHOME)}
} else {
    set d [file dirname $smv_file_name]
    if {[string compare $d ""]} {
	cd $d
	set smv_file_name [file tail $smv_file_name]
    }
}
    
set smv_init_time 0

foreach x "[pack slaves .]" {destroy $x}

# build the top level window

# menu .mbar
frame .mbar
pack .mbar -side top -fill x -expand 0

# a paned winow to hold two notebooks

tixPanedWindow .p -paneborderwidth 0 -separatorbg gray50
pack .p -side top -expand yes -fill both -padx 2 -pady 2

.p add p1 -size 250
.p add p2

#two notebooks



tixNoteBook .p.p1.nb -ipadx 2 -ipady 2
.p.p1.nb add sf -label Browser -underline 0 -raisecmd {global sigtree; focus [$sigtree subwidget hlist]}
.p.p1.nb add props -label Properties -underline 2 -raisecmd {global propslist; focus [$propslist subwidget hlist]}
.p.p1.nb add results -label Results -underline 0 -raisecmd {global resultslist; focus [$resultslist subwidget hlist]}
.p.p1.nb add cone -label Cone -underline 0 -raisecmd {global conelist; focus [$conelist subwidget hlist]}
.p.p1.nb add using -label Using -underline 3 -raisecmd {global usinglist; focus [$usinglist subwidget hlist]}
.p.p1.nb add groups -label Groups -underline 0 -raisecmd {focus .p.p1.nb.nbframe}
pack .p.p1.nb -expand yes -fill both -padx 2 -pady 2 -side top

tixNoteBook .p.p2.nb -ipadx 2 -ipady 2
.p.p2.nb add textframe -label Source -underline 0 \
  -raisecmd {focus .p.p2.nb.nbframe; textframe_raise; ntrace_lower; log_lower; global source_text; focus $source_text}
.p.p2.nb add ntrace -label Trace -underline 0 \
  -raisecmd {focus .p.p2.nb.nbframe; textframe_lower; ntrace_raise; log_lower}
.p.p2.nb add log -label Log -underline 0 \
  -raisecmd {focus .p.p2.nb.nbframe; textframe_lower; ntrace_lower; log_raise}
pack .p.p2.nb -expand yes -fill both -padx 2 -pady 2 -side top

bind all <Alt-b> {focus .p.p1.nb.nbframe; .p.p1.nb raise sf; global sigtree; focus [$sigtree subwidget hlist]}
bind all <Alt-o> {focus .p.p1.nb.nbframe; .p.p1.nb raise props; global propslist; focus [$propslist subwidget hlist]}
bind all <Alt-r> {focus .p.p1.nb.nbframe; .p.p1.nb raise results; global resultslist; focus [$resultslist subwidget hlist]}
bind all <Alt-c> {focus .p.p1.nb.nbframe; .p.p1.nb raise cone; global conelist; focus [$conelist subwidget hlist]}
bind all <Alt-n> {focus .p.p1.nb.nbframe; .p.p1.nb raise using; global usinglist; focus [$usinglist subwidget hlist]}
bind all <Alt-g> {focus .p.p1.nb.nbframe; .p.p1.nb raise groups}
bind all <Alt-s> {focus .p.p2.nb.nbframe; .p.p2.nb raise textframe; global source_text; focus $source_text}
bind all <Alt-t> {focus .p.p2.nb.nbframe; .p.p2.nb raise ntrace}
bind all <Alt-l> {focus .p.p2.nb.nbframe; .p.p2.nb raise log}

# if focus is in browser window, 
#bind .p.p1.nb.nbframe <Control-s> +{case [.p.p1.nb raised] {sf {start_isearch  .p.p1.nb.nbframe.sf.   next hlist}}}
#bind TixHList <Control-r> {start_isearch %W next hlist}


tixScrolledText .p.p2.nb.nbframe.textframe.text -scrollbar y -options "text.font $courier text.height 10 text.state disabled"
# -font $courier -borderwidth 2 -height 10 -state disabled
set source_text [.p.p2.nb.nbframe.textframe.text subwidget text]
frame .p.p2.nb.nbframe.textframe.mbar  -relief raised -bd 2
menubutton .p.p2.nb.nbframe.textframe.mbar.file -text File -menu .p.p2.nb.nbframe.textframe.mbar.file.menu
menu .p.p2.nb.nbframe.textframe.mbar.file.menu -postcommand {

    .p.p2.nb.nbframe.textframe.mbar.file.menu delete 0 last
    
    global cur_file
    global cur_line
    
    set state disabled
    if {![catch {set file $cur_file}] && [string compare "" $file]} {
	set state normal
    }
    
    .p.p2.nb.nbframe.textframe.mbar.file.menu add command\
	-state $state\
	-label "Open in emacs" -underline 0 -command {

	    global cur_file
	    global cur_line
	    
	    if {![catch {set file $cur_file}] && [string compare "" $file]} {
		after idle {
		    run_editor_on_file $cur_line $cur_file
		    #	    set foo $cur_file
		    #	    set cur_file ""
		    #	    SetFile $foo $cur_line
		    #	    catch {
		    #		check_mod_time
		    #	    }
		}
	    }
	}

    set fnum 0

    if {![catch {set srcfiles [smv_getFiles]}]} {
	foreach x $srcfiles {
	    if {$fnum == 0} {
		.p.p2.nb.nbframe.textframe.mbar.file.menu add separator
	    }
	    
	    if {$fnum < 10} {
		.p.p2.nb.nbframe.textframe.mbar.file.menu add command\
		    -label "$fnum $x"\
		    -underline 0\
		    -command "SetFile $x 1"
	    } else {
		.p.p2.nb.nbframe.textframe.mbar.file.menu add command\
		    -label "$x"\
		    -command "SetFile $x 1"
	    }
	    incr fnum;
	}
    }
}

menubutton .p.p2.nb.nbframe.textframe.mbar.show -text Show -menu .p.p2.nb.nbframe.textframe.mbar.show.menu
menu .p.p2.nb.nbframe.textframe.mbar.show.menu
.p.p2.nb.nbframe.textframe.mbar.show.menu add radiobutton -underline 6 -label "Where Declared" -variable show_signal_mode -value declare -command {see_signal}
.p.p2.nb.nbframe.textframe.mbar.show.menu add radiobutton -underline 6 -label "Where Initialized" -variable show_signal_mode -value init -command {see_signal}
.p.p2.nb.nbframe.textframe.mbar.show.menu add radiobutton -underline 6 -label "Where Assigned" -variable show_signal_mode -value assign -command {see_signal}
.p.p2.nb.nbframe.textframe.mbar.show.menu add radiobutton -underline 18  -label "Where Assigned in Trace" -variable show_signal_mode -value intrace -command {see_signal}

bind Text <Tab> {after idle {focus [tk_focusNext %W]}}
bind Text <Shift-Tab> {after idle {focus [tk_focusPrev %W]}}


proc textframe_raise {} {
    .p.p2.nb.nbframe.textframe.mbar.show configure -underline 3
    .p.p2.nb.nbframe.textframe.mbar.file configure -underline 3
}


proc textframe_lower {} {
    .p.p2.nb.nbframe.textframe.mbar.show configure -underline -1
    .p.p2.nb.nbframe.textframe.mbar.file configure -underline -1
}

proc ntrace_raise {} {
    .p.p2.nb.nbframe.ntrace.mbar.file configure -underline 3
    .p.p2.nb.nbframe.ntrace.mbar.edit configure -underline 1
    .p.p2.nb.nbframe.ntrace.mbar.run configure -underline 1
    .p.p2.nb.nbframe.ntrace.mbar.view configure -underline 3
}
proc ntrace_lower {} {
    .p.p2.nb.nbframe.ntrace.mbar.file configure -underline -1
    .p.p2.nb.nbframe.ntrace.mbar.edit configure -underline -1
    .p.p2.nb.nbframe.ntrace.mbar.run configure -underline -1
    .p.p2.nb.nbframe.ntrace.mbar.view configure -underline -1
}

proc log_raise {} {
    .p.p2.nb.nbframe.log.mbar.file configure -underline 3
}


proc log_lower {} {
    .p.p2.nb.nbframe.log.mbar.file configure -underline -1
}

# listbox .p.p1.nb.nbframe.sf.closed_signals -font $courier -relief raised -borderwidth 2 -height 15\
#  -yscrollcommand ".p.p1.nb.nbframe.sf.cs_scroll set" 


set sigtree .p.p1.nb.nbframe.sf.closed_signals
tixTree $sigtree -options "separator . hlist.columns 3 hlist.header true hlist.font $helvetica"\
	-browsecmd sigtree_browse \
	-opencmd sigtree_open -closecmd sigtree_close
# -font $courier -relief raised -borderwidth 2 -height 15


set hlist [$sigtree subwidget hlist]


# we don't want selection to move when mouse moves
bind TixHList <B1-Motion> ""
bind all <ButtonRelease-1> {
  global dragname
  . configure -cursor ""
  grab release .
    after idle {
      set dragname ""
    }
}

proc start_isearch {w dir type} {
    global isearch_window isearch_oldfocus isearch_anchor isearch_dir isearch_type
    if {[string compare [focus] .showprop.search]} {
	.showprop.search configure -state normal
	.showprop.search delete 0 end
	.showprop.search configure -state disabled
	set isearch_window $w
	set isearch_oldfocus [focus]
	set isearch_dir $dir
	set isearch_type $type
	focus .showprop.search
	if {[string match $type hlist]} {
	    set isearch_anchor [$w info anchor]
	    if {![string compare $isearch_anchor ""]} {
		set foo [$w info children]
		if {[llength $foo] == 0} {
		    set isearch_anchor ""
		} else {
		    set isearch_anchor [lindex $foo 0]
		    $w anchor set $isearch_anchor
		    $w see $isearch_anchor
		}
	    }
	} elseif {[string match $type grid]} {
	    set isearch_anchor [$w anchor get]
	    if {![string compare $isearch_anchor ""]} {
		set isearch_anchor 1
		$w anchor set 0 $isearch_anchor
		tracegrid_see $isearch_anchor
	    } else {
		set isearch_anchor [lindex $isearch_anchor 1]
		global tracegrid
		if {$isearch_anchor < 1} {set isearch_anchor 1}
		if {$isearch_anchor > $tracegrid(size)} {set isearch_anchor $tracegrid(size)}
		if {$tracegrid(size) > 0} {
		    $w anchor set 0 $isearch_anchor
		} else {set isearch_anchor ""}
	    }
	}
    }
}

#bind TixHList <Control-s> {start_isearch %W next hlist}
#bind TixHList <Control-r> {start_isearch %W next hlist}
#bind TixGrid <Control-s> {start_isearch %W next grid}
#bind TixGrid <Control-r> {start_isearch %W next grid}

set dragname ""

# [$sigtree subwidget hlist] configure -selectmode single
bindtags $hlist [concat [bindtags $hlist] drag_tag]
bind drag_tag <Button1-Motion> {drag_it %W}

# we can isearch in here
bindtags $hlist [concat [bindtags $hlist] isearch_tag]
bind isearch_tag <Control-s> {start_isearch %W next hlist}
bind isearch_tag  <Control-r> {start_isearch %W prev hlist}



proc drag_it {hlist} {
  global dragname
  if {[string match $dragname ""]} {
      set addr [$hlist info anchor]
      $hlist selection clear
      $hlist selection set $addr
#      set data [$hlist info data $addr]
      set data $addr
      set dragname $data
      if {[string compare $data ""]} {
	  . configure -cursor target
	  grab set -global .
      }
  }
}

proc sigtree_drag {} {
    global sigtree
    drag_it [$sigtree subwidget hlist]
}

set style(header) [tixDisplayStyle text  -refwindow $hlist \
	-fg black -anchor c \
        -padx 8 -pady 2\
	-font [tix option get bold_font ]]

$hlist header create 0 -itemtype text -text Name \
	-style $style(header)
$hlist header create 1 -itemtype text -text Layer \
	-style $style(header)

$hlist column width 2 0

proc sigtree_data {addr} {
    global sigtree
    return [[$sigtree subwidget hlist] info data $addr]
}

proc sigtree_close {addr} {
    global sigtree
    [$sigtree subwidget hlist] delete offsprings $addr
}

proc sigtree_open {addr} {
    global sigtree
    set n [sigtree_data $addr]
    foreach x [smv_children $n] {
	sigtree_add $sigtree $x
    }
}

proc sigtree_browse {addr} {
    global current_signal
    set n [sigtree_data $addr]
    set current_signal $n
}

proc sig_to_addr {n} {
    if {[string compare "." $n]} {
	regsub -all {\[} $n {.[} addr
	set addr .$addr
    } else {
	set addr $n
    }
    return $addr
}

proc sig_to_text {n} {
    if {[string compare "." $n]} {
	set text [lindex [split $n .] end]
    } else {
	set text ". (top level)"
    }
    return $text
}    

proc my_smv_layer {n} {
    global viewRequestedLayer
    if {$viewRequestedLayer} {
	return [smv_layer $n req]
    } else {
	return [smv_layer $n]
    }
}

proc sigtree_add {s n} {
    set addr [sig_to_addr $n]
    set text [sig_to_text $n]
    [$s subwidget hlist] add $addr -itemtype text -text $text -data $n
    [$s subwidget hlist] item create $addr 1 -itemtype text\
	    -text [my_smv_layer $n]
    if {[llength [smv_children $n]] > 0} {
	$s setmode $addr open
    } else {
	$s setmode $addr none
    }
}

set have_model 0

trace variable have_model w sigtree_update

proc sigtree_update {name1 name2 op} {
    after idle {
	global sigtree
	[$sigtree subwidget hlist] delete all
	global have_model
	if {$have_model} {sigtree_add $sigtree .}
    }
}
	
trace variable moded w sigtree_refresh
trace variable the_props w sigtree_refresh

proc sigtree_refresh1 {s n} {
    $s item configure $n 1 -text \
	    [my_smv_layer [$s info data $n]]
    foreach x [$s info children $n] {
	sigtree_refresh1 $s $x
    }
}


proc sigtree_flash {} {
    global sigtree
    set hlist [$sigtree subwidget hlist]
    foreach x [$hlist info children] {
	sigtree_refresh1 $hlist $x
    }
}

proc sigtree_refresh {name1 name2 op} {
    global moded
    global have_model
    if {$have_model && ($moded || ![string compare $name1 the_props])} {
	after idle {
	    sigtree_flash
	}
    }
}

trace variable current_signal w sigtree_goto

proc sigtree_goto1 {s n} {
    if {[string compare "." $n]} {
	set n [smv_parent $n]
	sigtree_goto1 $s $n
	$s open [sig_to_addr $n]
    }
}

proc sigtree_goto {name1 name2 op} {
    after idle {
	global current_signal
	catch {
	    if {[string compare $current_signal ""]} {
		global sigtree
		sigtree_goto1 $sigtree $current_signal
		[$sigtree subwidget hlist] selection clear
		[$sigtree subwidget hlist] selection set \
		    [sig_to_addr $current_signal]
		[$sigtree subwidget hlist] anchor set \
		    [sig_to_addr $current_signal]
		[$sigtree subwidget hlist] see \
		    [sig_to_addr $current_signal]
	    }
	}
    }
}

proc sigtree_get {} {
    global sigtree
    set addr [[$sigtree subwidget hlist] info anchor]
    if {[string compare "" $addr]} {
	return [sigtree_data $addr]
    } else {
	return ""
    }
}

proc propslist_unverified_filter {name status} {
    return [expr [string compare $status unverified] == 0]
}

proc propslist_verified_filter {name status} {
    return [expr [string compare $status verified] == 0]
}

proc propslist_assumed_filter {name status} {
    return [expr [string compare $status assumed] == 0]
}

proc propslist_no_filter {name status} {
    return 1
}



set propstop .p.p1.nb.nbframe.props.sl
set propssum $propstop.sum
set propslist_filter propslist_no_filter
set propslist_filter_choice "All properties"

frame $propstop
tixComboBox $propstop.a -dropdown true \
    -editable false -variable propslist_filter_choice -command props_choose\
    -options {
	listbox.height 4
    }

proc props_choose {foo} {
    global propslist_filter
    switch $foo {
	"All properties" {set propslist_filter propslist_no_filter}
	"Unverified properties" {set propslist_filter propslist_unverified_filter}
	"Verified properties" {set propslist_filter propslist_verified_filter}
	"Assumed properties" {set propslist_filter propslist_assumed_filter}
    }
    propslist_update1 0
}

$propstop.a insert end "All properties"
$propstop.a insert end "Unverified properties"
$propstop.a insert end "Verified properties"
$propstop.a insert end "Assumed properties"

set propslist .p.p1.nb.nbframe.props.pl

set propsopts {
    hlist.columns 3
    hlist.header  true
    hlist.separator "\n"
}
lappend propsopts hlist.font
lappend propsopts $helvetica

tixScrolledHList $propslist -options $propsopts

pack $propstop -fill x -side top
pack $propstop.a -side left
pack $propslist -expand yes -fill both -padx 3 -pady 3 -side left
 
set propshlist [$propslist subwidget hlist]

$propshlist configure -browsecmd propslist_browse
bindtags $propshlist [concat [bindtags $propshlist] isearch_tag]


# Create the title for the HList widget
#	>> Notice that we have set the hlist.header subwidget option to true
#      so that the header is displayed
#

# First some styles for the headers
set style(header) [tixDisplayStyle text  -refwindow $hlist \
	-fg black -anchor c \
        -padx 8 -pady 2\
	-font [tix option get bold_font ]]

$propshlist header create 0 -itemtype text -text Property \
	-style $style(header)
$propshlist header create 1 -itemtype text -text Status \
	-style $style(header)

# Notice that we use 3 columns in the hlist widget. This way when the user
# expands the windows wide, the right side of the header doesn't look
# chopped off. The following line ensures that the 3 column header is
# not shown unless the hlist window is wider than its contents.
#

$propshlist column width 2 0

# when we click on a property, make it the current property

proc propslist_browse {n} {
    choose_prop [list $n]
}

# whenever we have new results, update the properties window

trace variable results w propslist_update

proc propslist_update {name1 name2 op} {
    after idle {
	propslist_update1 1
    }
}


proc propslist_update1 {chk} {
    global propslist
    global propslist_filter
    [$propslist subwidget hlist] delete all
    set asscnt 0
    set verifcnt 0
    set unverifcnt 0
    foreach x [smv_update all] {
	set pstat($x) assumed
	incr asscnt
    }
    foreach x [smv_update props] {
	set pstat($x) verified
	incr verifcnt
    }
    foreach x [smv_update] {
	set pstat($x) unverified
	incr unverifcnt
    }
    set asscnt [expr $asscnt - $verifcnt]
    set verifcnt [expr $verifcnt - $unverifcnt]
    if {$chk && $unverifcnt == 0 && $verifcnt != 0} {
	if {$asscnt != 0} {
	    set ans  [tk_messageBox -icon question -type yesno \
		    -title "All verified" -parent .\
		    -message "All properties are verified. However, there are assumptions. Would you like to view these assumptions?"]
	    case $ans {
		yes {
		    global propstop
		    $propstop.a pick 3
		    .p.p1.nb raise props
		    return
		}
	    }
	} else {
	    tk_messageBox -icon info -type ok \
		    -title "All verified" -parent .\
		    -message "All properties are verified."
	}
    }
    foreach x [lsort [smv_update all]] {
	if {![string compare "" $propslist_filter] || \
		[$propslist_filter $x $pstat($x)]} {
	    [$propslist subwidget hlist] add $x -itemtype text\
		    -text $x
	    [$propslist subwidget hlist] item create $x 1 -itemtype text\
		    -text $pstat($x)
	}
    }
}

set usingtop .p.p1.nb.nbframe.using.sl
set usingsum $usingtop.sum
frame $usingtop
set usinglist .p.p1.nb.nbframe.using.pl

set usingopts {
    hlist.columns 3
    hlist.header  true
    hlist.separator "\n"
}
lappend usingopts hlist.font
lappend usingopts $helvetica

tixScrolledHList $usinglist -options $usingopts

pack $usingtop -fill x -side top
pack $usinglist -expand yes -fill both -padx 3 -pady 3 -side left
 
set usinghlist [$usinglist subwidget hlist]

$usinghlist configure -browsecmd usinglist_browse
bindtags $usinghlist [concat [bindtags $usinghlist] isearch_tag]


# Create the title for the HList widget
#	>> Notice that we have set the hlist.header subwidget option to true
#      so that the header is displayed
#

# First some styles for the headers
set style(header) [tixDisplayStyle text  -refwindow $hlist \
	-fg black -anchor c \
        -padx 8 -pady 2\
	-font [tix option get bold_font ]]

$usinghlist header create 0 -itemtype text -text Property \
	-style $style(header)
$usinghlist header create 1 -itemtype text -text Used... \
	-style $style(header)

# Notice that we use 3 columns in the hlist widget. This way when the user
# expands the windows wide, the right side of the header doesn't look
# chopped off. The following line ensures that the 3 column header is
# not shown unless the hlist window is wider than its contents.
#

$usinghlist column width 2 0

# when we click on a property, make it the current property

proc usinglist_browse {n} {
# do nothing for now
}

# whenever we have new results, update the properties window

trace variable the_props w usinglist_update

proc usinglist_update {name1 name2 op} {
    after idle {
	usinglist_update1
    }
}

proc usinglist_update1 {} {
    global usinglist
    global the_props
    [$usinglist subwidget hlist] delete all
    if {[string compare $the_props ""]} {
	if {![catch {set foo [smv_using]}]} {
	    foreach y [lsort $foo] {
		set x [lindex $y 0]
		catch {
		    [$usinglist subwidget hlist] add $x -itemtype text\
			-text $x
		    [$usinglist subwidget hlist] item create $x 1 -itemtype text\
			-text [lindex $y 1]
		}
	    }
	}
    }
}

proc conelist_allvars_filter {layer var next} {
    return $var
}

proc conelist_statevars_filter {layer var next} {
    return [expr $var && $next]
}

proc conelist_freevars_filter {layer var next} {
    return [expr ![string compare free $layer]]
}

proc conelist_no_filter {layer var next} {
    return 1
}

set conetop .p.p1.nb.nbframe.cone.sl
set conesum $conetop.sum
set conelist .p.p1.nb.nbframe.cone.pl
set conelist_filter conelist_no_filter
set conelist_filter_choice "Entire cone"

frame $conetop
tixComboBox $conetop.a -dropdown true \
    -editable false -variable conelist_filter_choice -command cone_choose\
    -options {
	listbox.height 4
    }

proc cone_choose {foo} {
    global conelist_filter
    switch $foo {
	"Entire cone" {set conelist_filter conelist_no_filter}
	"All variables" {set conelist_filter conelist_allvars_filter}
	"State variables" {set conelist_filter conelist_statevars_filter}
	"Free variables" {set conelist_filter conelist_freevars_filter}
    }
    conelist_update {} {} {}
}

$conetop.a insert end "Entire cone"
$conetop.a insert end "All variables"
$conetop.a insert end "State variables"
$conetop.a insert end "Free variables"

label $conesum -anchor w

set coneopts {
    hlist.columns 5
    hlist.header  true
    hlist.separator "\n"
}
lappend coneopts hlist.font
lappend coneopts $helvetica

tixScrolledHList $conelist -options $coneopts

pack $conetop -fill x -side top
pack $conetop.a -side left
pack $conesum -fill x -side left
pack $conelist -expand yes -fill both -padx 2 -pady 2 -side top
 
set conehlist [$conelist subwidget hlist]

#we can drag signals out of here
bindtags $conehlist [concat [bindtags $conehlist] drag_tag]

#we can isearch in here
bindtags $conehlist [concat [bindtags $conehlist] isearch_tag]


$conehlist configure -browsecmd conelist_browse


# Create the title for the HList widget
#	>> Notice that we have set the hlist.header subwidget option to true
#      so that the header is displayed
#

# First some styles for the headers
set style(header) [tixDisplayStyle text  -refwindow $hlist \
	-fg black -anchor c \
        -padx 8 -pady 2\
	-font [tix option get bold_font ]]

$conehlist header create 0 -itemtype text -text Signal \
	-style $style(header)
$conehlist header create 1 -itemtype text -text Layer \
	-style $style(header)
$conehlist header create 2 -itemtype text -text Vars \
	-style $style(header)
$conehlist header create 3 -itemtype text -text Type \
	-style $style(header)

# Notice that we use 3 columns in the hlist widget. This way when the user
# expands the windows wide, the right side of the header doesn't look
# chopped off. The following line ensures that the 3 column header is
# not shown unless the hlist window is wider than its contents.
#

$conehlist column width 4 0

# when we click on a property, make it the current property

proc conelist_browse {n} {
    global current_signal
    set current_signal $n
}

# when we have a new signal. show it 
trace variable current_signal w conelist_goto

proc conelist_goto {name1 name2 op} {
    after idle {
	global current_signal
	if {[string compare $current_signal ""]} {
	    global conehlist
	    catch {
		$conehlist selection clear
		$conehlist selection set $current_signal
		$conehlist anchor set $current_signal
		$conehlist see $current_signal
	    }
	}
    }
}

# whenever we have new results, update the properties window

trace variable moded w conelist_update
trace variable the_props w conelist_update

proc conelist_update {name1 name2 op} {
    after idle {
	global conesum
	$conesum config -text ""
	global conelist
	global conelist_filter
	[$conelist subwidget hlist] delete all
	global have_model
	if {$have_model} {
	    set total_comb 0
	    set total_state 0
	    foreach x [lsort [smv_cone]] {
		if {[catch {set layer [smv_layer $x]}]} {set layer ???}
		if {[catch {set vars [smv_layer $x vars]}]} {set vars 0}
		if {[catch {set next [expr $vars && [smv_layer $x next]]}]} {set next 0}
		if {![string compare "" $conelist_filter] || \
			[$conelist_filter $layer $vars $next]} {
		    [$conelist subwidget hlist] add $x -itemtype text\
			-text $x
		    [$conelist subwidget hlist] item create $x 1 -itemtype text\
			-text $layer
		    if {$vars} {
			[$conelist subwidget hlist] item create $x 2 -itemtype text\
			    -text $vars
			if {$next} {
			    set type state
			    incr total_state $vars
			} else {
			    set type comb
			    incr total_comb $vars
			}
			[$conelist subwidget hlist] item create $x 3 -itemtype text\
			    -text $type 
		    }
		}
	    }
	    $conesum config -text "State vars: $total_state,  Comb. vars: $total_comb"
	}
    }
}


proc post_tracegrid_file {w} {
    global the_traces
    global have_model
    
    $w.mbar.file.menu delete 0 last
    
    set state disabled
    if {$have_model} {set state normal}
    
    $w.mbar.file.menu add command -state $state -underline 0 -label "New trace"\
	-command {
	    global the_traces
	    global trace_scale
	    smv_newTrace
	    set the_traces -1
	}
    
    $w.mbar.file.menu add command -state $state\
	-underline 0 -label "Load from file..." -command {
	    after idle {
		set foo [tk_getOpenFile -filetypes {{"Trace files" {.tra}}\
							{"All files" *}} -parent .]
		if {[string compare $foo ""]} {
		    smv_loadTrace $foo
		    global the_traces
		    set the_traces -1
		}
	    }
	}
    
    set state disabled
    if {$have_model && [string compare $the_traces ""] != 0} {
	set state normal
    }
    
    
    $w.mbar.file.menu add command -state $state\
	-underline 0 -label "Save to file..." -command {
	    global the_traces
	    set foo [tk_getSaveFile -filetypes {{"Trace files" {.tra}}\
						    {"All files" *}} -parent .]
	    if {[string compare $foo ""]} {
		smv_saveTrace $the_traces $foo
	    }
	}
}

proc tracegrid_edit_cell {ov} {
    global tracegrid
    set tracegrid(override) $ov
    Tracegrid_edit
}

proc tracegrid_insert_row {} {
    global tracegrid
    set grid $tracegrid(g)
    set ent [$grid anchor get]
    if {[string comp $ent ""]} {
	set col [lindex $ent 0]
	set row [lindex $ent 1]
	if {$row > 0} {
	    tracegrid_insert_rows_before $row 1
	    $grid set 0 $row -text [sigtree_get]\
		-style $tracegrid(col0style)
	    $grid anchor set 0 $row
	    $grid selection set 0 $row
	    Tracegrid_editDone 0 $row
	}
    }
}


proc post_tracegrid_edit {w} {
    global the_traces
    global have_model
    global tracegrid
    set grid $tracegrid(g)
    set ent [$grid anchor get]
    
    $w.mbar.edit.menu delete 0 last
    
    set state disabled
    if {$have_model} {set state normal}
    
    set state disabled
    if {[string comp $ent ""] && [lindex $ent 0] > 0 && \
	    [lindex $ent 1] > 0 } {set state normal}
    
    $w.mbar.edit.menu add command -state $state -underline 0 -label "Suggest value"\
	-command "tracegrid_edit_cell 0"
    
    $w.mbar.edit.menu add command -state $state -underline 0 -label "Override value"\
	-command "tracegrid_edit_cell 1"
    
    set state disabled
    if {[string comp $ent ""] && [lindex $ent 0] == 0 && \
	    [lindex $ent 1] > 0 && [lindex $ent 1] <= $tracegrid(size) + 1} {set state normal}
    
    $w.mbar.edit.menu add command -state $state -underline 0 -label "Insert row"\
	-command {
	    global tracegrid
	    set grid $tracegrid(g)
	    set ent [$grid anchor get]
	    if {[string comp $ent ""]} {
		set col [lindex $ent 0]
		set row [lindex $ent 1]
		if {$row > 0} {
		    tracegrid_insert_rows_before $row 1
		    $grid set 0 $row -text [sigtree_get]\
			-style $tracegrid(col0style)
		    $grid anchor set 0 $row
		    $grid selection set 0 $row
		    Tracegrid_edit
		}
	    }
 	}
    

    set state disabled
    if {[string comp $ent ""] && [lindex $ent 0] == 0 && \
	    [lindex $ent 1] > 0 && [lindex $ent 1] <= $tracegrid(size)} {set state normal}

    $w.mbar.edit.menu add command -state $state -underline 0 -label "Delete row"\
	-command {
	    global tracegrid
	    set grid $tracegrid(g)
	    set ent [$grid anchor get]
	    if {[string comp $ent ""]} {
		set col [lindex $ent 0]
		set row [lindex $ent 1]
		if {$row > 0} {
		    tracegrid_remove_rows $row 1
		}
	    }
	}

    $w.mbar.edit.menu add command -underline 7 -label "Delete all" -command {
	global the_traces
	global tracegrid
	
	tracegrid_remove_rows 1 $tracegrid(size)
    }
    


}
    

proc post_tracegrid_run {w}  {
    global the_traces
    global have_model
    
    $w.mbar.run.menu delete 0 last
    
    set state disabled
    if {$have_model && [string compare $the_traces ""] != 0} {
	set state normal
    }
    
    $w.mbar.run.menu add command  -underline 0 -state $state\
	-label "Recalculate trace" -command {
	    global the_traces
	    global trace_scale
	    smv_runTrace $the_traces
	    tracegrid_refresh [tracegrid_get_signals]
	}
    
    $w.mbar.run.menu add command -underline 0 -state $state\
	-label "Extend trace" -command {
	    global the_traces
	    global trace_scale
	    
	    set ans\
		[string_dialog .d "Trace extension"\
		     "Extend trace by how many steps?" "" "" 0 "OK" "Cancel"]
	    if {[lindex $ans 0] == 0} {
		smv_extendTrace $the_traces [lindex $ans 1]
		tracegrid_refresh [tracegrid_get_signals]
	    }
	}
}

proc tracegrid_zoom {d} {
    global tracegrid
    set tracegrid(scale) [expr $tracegrid(scale) + $d * ($tracegrid(scale)/4+1)]
    $tracegrid(g) size column default\
	-size [expr $tracegrid(scale) * [font measure [$tracegrid(g) cget -font] 0]]
}

proc post_tracegrid_view {w} {
    global the_traces
    global have_model
    global tracegrid
    
    $w.mbar.view.menu delete 0 last
    
    set state disabled
    if {$tracegrid(scale) > 2} {set state normal}
    $w.mbar.view.menu add command -underline 5 -state $state -label "Zoom out" -command {
	tracegrid_zoom -1
    }
    $w.mbar.view.menu add command -underline 5 -label "Zoom in" -command {
	tracegrid_zoom +1
    }

    $w.mbar.view.menu add separator

    $w.mbar.view.menu add command -underline 0 -label "Save trace view" -command {
	set foo [tk_getSaveFile -filetypes {{"Trace view files" {.tvw}}\
						{"All files" *}} -parent .]
	if {[string compare $foo ""]} {
	    tracegrid_save_view $foo
	}
    }
    
    $w.mbar.view.menu add command -underline 0 -label "Restore trace view" -command {
	set foo [tk_getOpenFile -filetypes {{"Trace view files" {.tvw}}\
						{"All files" *}} -parent .]
	if {[string compare $foo ""]} {
	    tracegrid_restore_view $foo 1
	}
	
    }
    
    $w.mbar.view.menu add separator
    
    $w.mbar.view.menu add radiobutton -underline 5 -label "Show all traces"\
	-variable tracegrid(show_all) -value 1 -command {
	    global the_traces
	    set the_traces $the_traces
	}
    $w.mbar.view.menu add radiobutton -underline 7 -label "Show requested traces"\
	-variable tracegrid(show_all) -value 0
}

proc CreateTracegridMenu {w} {
	
    frame $w.mbar -relief raised -bd 2
    pack $w.mbar -side top -fill y -expand 0

    menubutton $w.mbar.file -text File -menu $w.mbar.file.menu
    menu $w.mbar.file.menu -postcommand "post_tracegrid_file $w"

    menubutton $w.mbar.edit -text Edit -menu $w.mbar.edit.menu
    menu $w.mbar.edit.menu -postcommand "post_tracegrid_edit $w"

    menubutton $w.mbar.run -text Run -menu $w.mbar.run.menu
    menu $w.mbar.run.menu -postcommand "post_tracegrid_run $w"
    
    menubutton $w.mbar.view -text View -menu $w.mbar.view.menu
    menu $w.mbar.view.menu -postcommand "post_tracegrid_view $w"

    pack $w.mbar -side top -fill x
    pack $w.mbar.file -side left
    pack $w.mbar.edit -side left
    pack $w.mbar.run -side left
    pack $w.mbar.view -side left
}

proc CreateTracegrid {nb page} {
    global tracegrid
    global courier
    global helvetica

    set w $nb.nbframe.$page
    set tracegrid(raise) "$nb raise $page"

    # make the menu bar

    CreateTracegridMenu $w

    # Create the grid and set options to make it editable.
    #
    tixScrolledGrid $w.g -bd 0
    pack $w.g -expand yes -fill both -padx 3 -pady 3

    set grid [$w.g subwidget grid]
    $grid config \
	-formatcmd "Tracegrid_format $grid" \
	-editnotifycmd "Tracegrid_editNotify" \
	-editdonecmd "Tracegrid_editDone" \
	-selectunit cell \
	-selectmode browse \
	-font $courier

    $grid size column 0 -size auto

    # when clicked in the grid, set the current signal and
    # current state appropriately 

    bindtags $grid [concat [bindtags $grid] tracegrid_tag]
    bind tracegrid_tag <Button-1> {
	global tracegrid
	global current_signal
	global current_state
	set grid $tracegrid(g)
	set ent [$grid anchor get]
	set col [lindex $ent 0]
	set row [lindex $ent 1]
	
	if {[string comp $ent ""] && $col >= 0 && $col <= $tracegrid(length) \
		&& $row > 0 && $row <= $tracegrid(size)} {
	    set sig [$grid entrycget 0 $row -text]
	    if {[string compare $sig ""] && ![string match =* $sig]} {
		set current_signal $sig
		set current_state [expr ($col == 0) ? 0 : ($col - 1)]
	    }
	}
    }
      
    bind tracegrid_tag <ButtonRelease-1> {
	global dragname
	if {[string compare $dragname ""]} {
	    _tixRecordFlags <ButtonRelease-1>  %% %# %b %c %d %f %h %k %m %o %p %s %t %w %x %y %A %B %E %K %N %R %T %W %X %Y
	    tixGrid:ButtonRelease-1 %W %x %y
	    _tixDeleteFlags
	    tracegrid_insert_row
	}
    }

    bind tracegrid_tag <Button1-Enter> {
	global dragname
	if {[string compare $dragname ""]} {
	    _tixRecordFlags <ButtonPress-1>  %% %# %b %c %d %f %h %k %m %o %p %s %t %w %x %y %A %B %E %K %N %R %T %W %X %Y
	    tixGrid:Button-1 %W %x %y
	    _tixDeleteFlags
	}
    }

    bind tracegrid_tag <Button1-Leave> {
	global dragname
	if {[string compare $dragname ""]} {
	    _tixRecordFlags <ButtonRelease-1>  %% %# %b %c %d %f %h %k %m %o %p %s %t %w %x %y %A %B %E %K %N %R %T %W %X %Y
	    tixGrid:ButtonRelease-1 %W %x %y
	    _tixDeleteFlags
	}
    }


    # Global data used by other Tracegrid_ procedures.
    #
    set tracegrid(g)   $grid
    set tracegrid(size) 0
    set tracegrid(edit) 0
    set tracegrid(col0style) [tixDisplayStyle text -anchor e -font $helvetica]
    set tracegrid(show_all) 1
    set tracegrid(scale) 8
    tracegrid_zoom 0

    # set us up to search this window

    bindtags $grid [concat [bindtags $grid] grid_isearch_tag]
    bind grid_isearch_tag <Control-s> {start_isearch %W next grid}
    bind grid_isearch_tag  <Control-r> {start_isearch %W prev grid}

    # set up to move around with arrow keys

    bind $tracegrid(g) <Up> {tracegrid_bump up}
    bind $tracegrid(g) <Down> {tracegrid_bump down}
    bind $tracegrid(g) <Left> {tracegrid_bump left}
    bind $tracegrid(g) <Right> {tracegrid_bump right}

    # put the anchor somewhere meaningful

    $tracegrid(g) anchor set 0 1
}

trace variable the_traces w Tracegrid_refresh

proc tracegrid_insert_rows_before {i n} {
    global tracegrid
    if {$i <= $tracegrid(size)} {
	$tracegrid(g) move row $i $tracegrid(size) $n
    }
    set tracegrid(size) [expr $tracegrid(size) + $n]
}
	
proc tracegrid_remove_rows {i n} {
    global tracegrid
    if {$i > $tracegrid(size)} {return}
    if {$i + $n - 1 > $tracegrid(size)} {
	set n [expr $tracegrid(size) - $n + 1]
    }
    $tracegrid(g) delete row $i [expr $i + $n - 1]
    if {$i + $n <= $tracegrid(size)} {
	$tracegrid(g) move row [expr $i+$n] $tracegrid(size) [expr -$n]
    }
    set tracegrid(size) [expr $tracegrid(size) - $n]
}
	


proc tracegrid_insert_traces {row trace sig} {
    global tracegrid
    set traces [smv_trace $trace $sig]
    set grid $tracegrid(g)
    if {[llength $traces] == 0} {error "No traces for $sig"}
    tracegrid_insert_rows_before $row [llength $traces]
    foreach x $traces {
	$grid set 0 $row -text [lindex $x 0]\
	    -style $tracegrid(col0style)
	set col 1
	foreach y [lindex $x 1] {
	    if {[string compare "*unknown*" $y] == 0} {set y -}
	    $grid set $col $row -text $y
	    incr col
	}
	incr row
    }
}


proc Tracegrid_refresh {name1 name2 foo} {
    global have_model
    global the_traces
    if {$have_model && [string compare $the_traces ""]} {
	after idle {
	    global tracegrid
	    if {$tracegrid(show_all)} {
		set sigs .
	    } else {
		set sigs [tracegrid_get_signals]
	    }
	    tracegrid_refresh $sigs
	    global the_traces
	    if {$the_traces >= 0 && [lindex [lindex $results $the_traces] 2] == 0} {
		eval $tracegrid(raise)
	    }
	}
    }
}

proc tracegrid_refresh {sigs} {
    global tracegrid
    global the_traces
    global results
    set grid $tracegrid(g)
#    $grid selection clear
    $grid delete row 0 $tracegrid(size)
    set tracegrid(size) 0
    set tracegrid(length) 0
    if {$the_traces < -1} return
    if {![catch {
	set tracegrid(length) [smv_traceLength $the_traces]
    }]} {
	set col 1
	while {$col <= $tracegrid(length)} {
	    set loop 0
	    if {$the_traces >= 0} {
		set loop [lindex [lindex $results $the_traces] 3]
	    }
	    set lab ""	   
	    if {$loop && $col == $loop} {append lab "|: "}
	    append lab $col
	    if {$loop && $col == $tracegrid(length)} {append lab " :|"}
	    
	    $grid set $col 0 -text $lab
	    incr col
	}
	foreach x $sigs {
	    catch {tracegrid_insert_traces [expr $tracegrid(size) + 1] $the_traces $x}
	}
    }
}


# Tracegrid_edit --
#
#	Prompts the user to edit a cell.
#
proc Tracegrid_edit {} {
    global tracegrid
    set grid $tracegrid(g)

    set ent [$grid anchor get]
    if {!$tracegrid(edit) && [string comp $ent ""]} {
	set tracegrid(edit) 1
	$grid edit set [lindex $ent 0]  [lindex $ent 1]
    }
}


# Tracegrid_editNotify --
#
#	Returns true if an entry can be edited.
#
proc Tracegrid_editNotify {x y} {
    global tracegrid
    set grid $tracegrid(g)

    if {$y > 0 &&\
	    $x <= $tracegrid(length) && $y <= $tracegrid(size)\
	    && $tracegrid(edit)} {
	set tracegrid(oldValue) [$grid entrycget $x $y -text]
	return 1
    }	
    return 0
}

# Tracegrid_editDone --
#
#	Gets called when the user is done editing an entry.
#
proc Tracegrid_editDone {x y} {
    global tracegrid
    global the_traces
    set grid $tracegrid(g)

    set tracegrid(edit) 0
    set pop [$grid entrycget $x $y -text]

    if {$x == 0} {
	tracegrid_remove_rows $y 1
	if {[catch {
	    tracegrid_insert_traces $y $the_traces $pop
	} msg]} {
	    error_dialog $msg
	}
    } else {
	set signal [$grid entrycget 0 $y -text]
	if {[string compare $signal ""]} {
	    if {$tracegrid(override)} {
		set bar :=
	    } else {
		set bar =
	    }
	    smv_modTrace $the_traces [expr $x - 1]\
		$signal $bar [string trim $pop]
	}
    }
}

# Tracegrid_format --
#
#	This command is called whenever the background of the grid
#	needs to be reformatted. The x1, y1, x2, y2 sprcifies the four
#	corners of the area that needs to be reformatted.
#
proc Tracegrid_format {w area x1 y1 x2 y2} {
    global tracegrid

    set bg(s-margin) gray65
    set bg(x-margin) gray65
    set bg(y-margin) gray65
    set bg(main)     gray20

    case $area {
	main {
	    $w format grid $x1 $y1 $x2 $y2 \
		    -relief raised -bd 1 -bordercolor $bg($area)\
		    -filled 0 -bg red\
		    -xon 1 -yon 1 -xoff 0 -yoff 0 -anchor se
	}
	y-margin {
	    $w format border $x1 $y1 $x2 $y2 \
		-fill 1 -relief raised -bd 1 -bg $bg($area) \
		-selectbackground gray80
	}
	default {
	    $w format border $x1 $y1 $x2 $y2 \
		-filled 1 \
		-relief raised -bd 1 -bg $bg($area) \
		-selectbackground gray80
	}
    }
}

proc tracegrid_bump {dir} {
    global tracegrid
    set a [$tracegrid(g) anchor get]
    if {[string compare $a ""]} {
	set ax [lindex $a 0]
	set ay [lindex $a 1]
	if {[string match $dir up]}    {incr ay -1}
	if {[string match $dir down]}  {incr ay 1}
	if {[string match $dir left]}  {incr ax -1}
	if {[string match $dir right]} {incr ax 1}
	if {[$tracegrid(g) info exists $ax $ay]} {
	    $tracegrid(g) selection clear 0 0 max max
	    $tracegrid(g) anchor set $ax $ay
	    $tracegrid(g) selection set $ax $ay
	    tracegrid_see_both $ax $ay
	}
    }
}

CreateTracegrid .p.p2.nb ntrace

# scrollbar .p.p1.nb.nbframe.sf.cs_scroll -command ".p.p1.nb.nbframe.sf.closed_signals yview"

proc CreateBatchLog {nb page} {
    global batch_log
    global courier

    set w $nb.nbframe.$page
    set batch_log(frame) $w
    set batch_log(raise) "$nb raise $page"
    set batch_log(file) ""
    frame $w.mbar -relief raised -bd 2
    pack $w.mbar -side top -fill x -expand 0
    menubutton $w.mbar.file -text File -menu $w.mbar.file.menu
    pack $w.mbar.file -side left
    menu $w.mbar.file.menu
    $w.mbar.file.menu add command -label Close -underline 0\
	-command {}
    text $w.text -font $courier -yscrollcommand "$w.sb set"
    pack $w.text -side left -expand 1 -fill both
    scrollbar $w.sb -orient vertical -command "$w.text yview"
    pack $w.sb -side right -expand 1 -fill y
}

CreateBatchLog .p.p2.nb log

proc check_background {} {
    global batch_log
    if {[string length $batch_log(file)] > 0} {
	set ans [tk_dialog .d "Warning" \
		     "A background verification task is running." \
		     warning 1 "Kill it" "Cancel"]
	if {$ans == 0} {
#	    catch {eval "exec kill -9 [pid $batch_log(file)]"}
	    smv_kill
	    catch {close $batch_log(file)}
	    set batch_log(file) ""
	    $batch_log(frame).text insert end "\n(Killed)"
	}
	return $ans
    }
    return 0
}


menubutton .mbar.fileb -menu .mbar.fileb.menu -text File -underline 0
menubutton .mbar.propb -menu .mbar.propb.menu -text Prop -underline 0
menubutton .mbar.viewb -menu .mbar.viewb.menu -text View -underline 0
menubutton .mbar.gotob -menu .mbar.gotob.menu -text Goto -underline 0
menubutton .mbar.histb -menu .mbar.histb.menu -text History -underline 1
menubutton .mbar.absb -menu .mbar.absb.menu -text Abstraction -underline 0
menubutton .mbar.helpb -menu .mbar.helpb.menu -text Help -underline 0

menu .mbar.helpb.menu
.mbar.helpb.menu add command -label "About SMV..." -underline 0 -command {
toplevel .h
wm title .h "About SMV..."
label .h.msg -wraplength 6i -justify center -text "This is SMV, experimental release test, written by Ken McMillan at Cadence Berkeley Labs. It is \
based on the original SMV from Carnegie Mellon University, by the same author.\n\
\n\
\"It does what it does, no more, no less.\"\n\
\n\
Copyright 1998 Cadence Design Systems\n\
Copyright 1992 Carnegie Mellon University"\
    -font $helvetica
pack .h.msg -side right -expand 1 -fill both -padx 3m -pady 3m

}
.mbar.helpb.menu add separator
.mbar.helpb.menu add command -label "Contents..." -underline 0\
    -command "opendoc smv"
.mbar.helpb.menu add command -label "Getting started with SMV..." -underline 0\
    -command "opendoc tutorial/tutorial"
.mbar.helpb.menu add command -label "Language reference..." -underline 0\
    -command "opendoc language/language"

if {![string compare $tcl_platform(platform) windows]} {
.mbar.helpb.menu add separator
.mbar.helpb.menu add command -label "Get Linux..." -underline 1\
    -command "opendoc linux/linux"
}

proc opendoc {d} {
    after idle "opendoc1 $d"
}

proc opendoc2 {file} {
    puts "got here ${file}..."
    puts -nonewline [read $file 1000]
    if {[eof $file]} {
	if {[catch {close $file} msg]} {
	    tk_messageBox -icon error -message $msg -type ok
	}
    }
}

proc opendoc1 {d} {
    global tcl_library
    global tcl_platform

    if {[catch {
	if {[string compare $tcl_platform(platform) windows]} {
	    if {[string compare "tutorial/tutorial" $d] == 0} {
		exec smv_tutorial
#	      set file [open |false r]
#              fconfigure $file -blocking 0
#              fileevent $file readable "opendoc2 $file"
	    } else {
		set smvdir ""
		global env
		foreach x [split $env(PATH) :] {
		    if {[file exists [file join $x smv]]} {
			set smvdir $x
			break
		    }
		}
		if {[string compare "" $smvdir] == 0} {error "can't find smv documentation"}
		# puts "using smv in $smvdir..."
		set smvdocdir [file join [file dirname $smvdir] doc/smv]

#		set f [file join [file dirname [file dirname $tcl_library]] doc/smv/$d.html]
		set f [file join $smvdocdir $d.html]
		if {[string compare $tcl_platform(os) Darwin] == 0} {
		    exec osascript -e "open location \"file:$f\""
		} else {
		    if {[catch {exec htmlview $f}]} {
			exec xdg-open $f &
		    }
		}
	    }
	} else {
	    set f [file nativename [file join [file dirname [file dirname $tcl_library]]\
					doc/$d.html]]
	    exec cmd << "\"$f\"\n" &
	}
    } msg]} {tk_messageBox -icon error -message $msg -type ok}
}
	   

menu .mbar.fileb.menu -postcommand {
    global the_props
    global smv_file_name
    .mbar.fileb.menu delete 0 last
    


    set state disabled
    if {[llength $the_props] > 0} {set state normal}

    
    .mbar.fileb.menu add command -label "New..." -underline 0 -command {
	global smv_file_name
	
	if {[check_background]} {return}
	
	set foo [tk_getSaveFile -filetypes {{"SMV files" {.smv .v}}} -parent . -title "Save new file as..."]
	if [string compare $foo ""] {
	    shut_it_down
	    set smv_file_name $foo
	    set d [file dirname $smv_file_name]
	    if {[string compare $d ""]} {
		cd $d
		set smv_file_name [file tail $smv_file_name]
	    }
	    if {[catch {set f [open $smv_file_name w]} msg]} {
		show_error $msg
	    } else {
		if {[string match "*.smv" $smv_file_name]} {
		    puts $f "module main(){\n\n}\n"
		} elseif {[string match "*.v" $smv_file_name]} {
		    puts $f "module main();\n\nendmodule\n"
		}
		close $f
		fire_it_up
		run_editor_on_file 2 $smv_file_name
	    }
	}
    }
  
    .mbar.fileb.menu add command -label "Open..." -underline 0 -command {
	global smv_file_name
	
	if {[check_background]} {return}
	
	set foo [tk_getOpenFile -filetypes {{"SMV files" {.smv .v}} {"All files" *}} -parent .]
	if [string compare $foo ""] {
	    shut_it_down
	    set smv_file_name $foo
	    set d [file dirname $smv_file_name]
	    if {[string compare $d ""]} {
		cd $d
		set smv_file_name [file tail $smv_file_name]
	    }
	    fire_it_up
	}
    }

  set reopen_state disabled
    if {[string compare $smv_file_name ""]} {set reopen_state normal}
    .mbar.fileb.menu add command -state $reopen_state -label "Reopen" -underline 0 -command {
        global the_props
	set foo $the_props
	shut_it_down
	set the_props $foo
	global cur_file
	save_editor_files
	fire_it_up
    }
    
  .mbar.fileb.menu add command -label "Save changes" -state $state -underline 0 -command {
	global moded
	smv_save
	set moded 0
      }
  .mbar.fileb.menu add command -label "Undo changes" -state $state \
       -underline 1 -command "revert_using"
  .mbar.fileb.menu add command -label "Save abstraction as..." -state $state -underline 17 -command {
	set foo [tk_getSaveFile -filetypes {{"Abstraction files" {.abs}}\
         {"All files" *}} -parent .]
      if {[string compare $foo ""]} {
	  smv_save $foo
      }
  }
  .mbar.fileb.menu add command -label "Quit" -underline 0 -command "my_quit"
}
# .mbar add cascade -label File -menu .mbar.fileb.menu -underline 0



proc choose_prop {choice} {
    global the_props
    global moded
    if {[string compare $the_props $choice]} {
	set the_props $choice
	if {[catch {eval "smv_props $the_props"} msg]} {
	    show_error $msg
	    set the_props ""
	    return
	} 
#	set moded 0
#    .mbar.absb.menu configure -state normal
	if {[string compare [lindex $choice 0] "."] != 0} {
	    .showprop.t configure -text "Property: [lindex $choice 0]"
	} else {
	    .showprop.t configure -text ""
	}
    }
}


menu .mbar.propb.menu -postcommand {
  global the_props
  .mbar.propb.menu delete 0 last


    
    set state disabled
    if {[llength $the_props] > 0} {set state normal}
    .mbar.propb.menu add command -underline 0 -label "Options..." -state $state\
      -command {
	  options_dialog .d [smv_options]
      }
    
    .mbar.propb.menu add command -underline 3 -label "Copy options..." -state $state\
      -command {
	  set choices [smv_getPropsWithOptions]
	  set choice \
	      [list_dialog .d "Choose a source property"\
		   "Copy options from..." "" $choices]
	  if {[string length $choice] > 0} {
	      set new_options [smv_options $choice]
	      smv_setOptions $new_options
	      global moded
	      set moded 0
	  }
      }
	      
    .mbar.propb.menu add command -underline 0 -label "Group siblings" -state $state\
      -command {
	  global the_props

	  choose_prop [eval "smv_groupSiblings $the_props"]
	  teardown_groups
	  setup_groups
      }

#    .mbar.propb.menu add command -underline 0 -label "Verify"  -command "RunSmv"
    set batch_state normal
    global batch_log
    if {[string length $batch_log(file)] > 0} {
	.mbar.propb.menu add command -underline 0 -label "Kill verification" -command {
	    global batch_log
#	    catch {eval "exec kill -9 [pid $batch_log(file)]"}
	    smv_kill
	    catch {close $batch_log(file)}
	    set batch_log(file) ""
	    $batch_log(frame).text insert end "\n(Killed)"
	}
    } else {
	if {[string compare $the_props ""]} {
	.mbar.propb.menu add command -label "Verify $the_props" -command "RunSmvBatch 0" -underline 0
	}
	.mbar.propb.menu add command -label "Verify all" -underline 7 -command "RunSmvBatch 1"
	.mbar.propb.menu add command -label "State count" -underline 6 -command "RunSmvBatch 2"
    }
}
# .mbar add cascade -label Prop -menu .mbar.propb.menu -underline 0





menu .mbar.viewb.menu
menu .mbar.viewb.menu.font

.mbar.viewb.menu add radiobutton -label "Requested layer" -variable viewRequestedLayer -value 1 -command {
  SetClosedSignals
}
.mbar.viewb.menu add radiobutton -label "Actual layer" -variable viewRequestedLayer -value 0 -command {
  SetClosedSignals
}
.mbar.viewb.menu add separator
.mbar.viewb.menu add cascade -menu .mbar.viewb.menu.font -label Fonts
.mbar.viewb.menu.font add radiobutton -label Large -variable fontSize -value 14\
    -command {sizeFonts 14}
.mbar.viewb.menu.font add radiobutton -label Medium -variable fontSize -value 12\
    -command {sizeFonts 12}
.mbar.viewb.menu.font add radiobutton -label Small -variable fontSize -value 10\
    -command {sizeFonts 10}

# .mbar add cascade -label View -menu .mbar.viewb.menu -underline 0

menu .mbar.foo -postcommand {
}
# .mbar add cascade -label Foo -menu .mbar.foo -underline 1


proc goto_dialog {s l} {
  set choice [list_dialog .d "Goto signal" $s "" $l]
  if {[string length $choice] > 0} {
    goto_by_name $choice
  }
}


menu .mbar.gotob.menu -postcommand {
    global current_signal
    .mbar.gotob.menu delete 0 last
    
    
    set state disabled
    if {$have_model && ![string match $current_signal ""]} {set state normal}
    
    .mbar.gotob.menu add command -state $state -underline 0 -label "Backward..."\
	-command {
	    global current_signal
	    goto_dialog "Signal $current_signal depends on..." [smv_depend $current_signal]
	}
    
    set state disabled
    if {$have_model && [llength $the_props] > 0  && ![string match $current_signal ""]} {set state normal}
    
    .mbar.gotob.menu add command -state $state -underline 0 -label "Forward..."\
	-command {
	    global current_signal
	    goto_dialog "These signals depend on $current_signal..." [smv_depend $current_signal fwd]
	}
    
}



# .mbar add cascade -label Goto -menu .mbar.gotob.menu -underline 0

set hist_list ""

proc add_to_hist {x} {
  global hist_list
  set foo [lsearch $hist_list $x]
  if {$foo >= 0} {
    set hist_list [lreplace $hist_list $foo $foo]
  }
  if {[llength $hist_list] >= 10} {
    set hist_list [lreplace $hist_list 0 0]
  }
  lappend hist_list $x
}

set show_signal_mode declare

proc see_signal {} {
    global show_signal_mode
    global signal_index
    global signals_list
    global current_signal
    catch {
	set e ""
	set e $current_signal
	global the_traces
	global current_state
	if {[catch {
	    set foo [smv_whereAssigned $show_signal_mode \
			 $e $the_traces $current_state]
	    SetFile [lindex $foo 0] [lindex $foo 1]
	} msg]} {
	    global cur_file
	    set cur_file ""
	    global source_text
	    $source_text configure -state normal
	    $source_text delete 1.0 end
	    $source_text insert end "$e $msg"
	    $source_text configure -state disabled
	}
    }
}
    
trace variable current_signal w source_update

proc source_update {name1 name2 op} {
    after idle {
	see_signal
    }
}

trace variable current_signal w hist_update

proc hist_update {name1 name2 op} {
    after idle {
	global current_signal
	add_to_hist $current_signal
    }
}


proc goto_by_name {x} {
    global current_signal
    set current_signal $x
}

proc my_abs_cmd {x y} {
  global signals_list
  global moded
  global the_props

    if {[catch {smv_abstraction $x $y} msg]} {
	tk_dialog .d "Error" $msg error 0 "Dismiss"
	return
    }
    set moded 1
}

proc other_abs_cmd {x} {
    set ans\
	[string_dialog .d "Enter layer name"\
	     "Enter a layer name for $x" "" "" 0 "OK" "Cancel"]
    if {[lindex $ans 0] == 0} {
	my_abs_cmd $x [lindex $ans 1]
    }
}
	

proc text_dialog {title s} {
    global tkPriv

    set oldFocus [focus]

    set w .td
    catch {destroy $w}
    toplevel $w -class Dialog
    wm title $w $title
    wm iconname $w Dialog
    wm protocol $w WM_DELETE_WINDOW { }
    wm transient $w [winfo toplevel [winfo parent $w]]
    frame $w.top -relief raised -bd 1
    pack $w.top -side top -fill both
    frame $w.bot -relief raised -bd 1
    pack $w.bot -side bottom -fill both

    # 2. Fill the top part with the text

    tixScrolledText $w.top.st
    [$w.top.st subwidget text] insert 1.0 $s
    pack $w.top.st -side top -fill both

    # 3. Create a row of buttons at the bottom of the dialog.

    set default 0
    set i 0
    foreach but "Dismiss" {
	button $w.button$i -text $but -command "set tkPriv(button) $i"
	if {$i == $default} {
	    frame $w.default -relief sunken -bd 1
	    raise $w.button$i $w.default
	    pack $w.default -in $w.bot -side left -expand 1 -padx 3m -pady 2m
	    pack $w.button$i -in $w.default -padx 2m -pady 2m
	    bind $w <Return> "$w.button$i flash; set tkPriv(button) $i"
	} else {
	    pack $w.button$i -in $w.bot -side left -expand 1 \
		-padx 3m -pady 2m
	}
	incr i
    }
    
    # 4. Withdraw the window, then update all the geometry information
    # so we know how big it wants to be, then center the window in the
    # display and de-iconify it.

    wm withdraw $w
    update idletasks
    set x [expr [winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
	    - [winfo vrootx [winfo parent $w]]]
    set y [expr [winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
	    - [winfo vrooty [winfo parent $w]]]
    wm geom $w +$x+$y
    wm deiconify $w

    # 5. Set a grab and claim the focus too.

    grab $w
    tkwait visibility $w
    if {$default >= 0} {
	focus $w.button$default
    } else {
	focus $w
    }

    # 6. Wait for the user to respond, then restore the focus and
    # return the index of the selected button.

    tkwait variable tkPriv(button)
    destroy $w
    focus $oldFocus
    return $tkPriv(button)
}

menu .mbar.histb.menu -postcommand {
  global hist_list
  global signal_index
  .mbar.histb.menu delete 0 last
  foreach x $hist_list {
      .mbar.histb.menu add command -label $x -command [list goto_by_name $x]
  }
}
# .mbar add cascade -label History -menu .mbar.histb.menu -underline 0



menu .mbar.absb.menu -postcommand {
    .mbar.absb.menu delete 0 last

    global current_signal
    global the_props
    set state disabled
    if {$have_model && [string compare "" $the_props] &&\
	    [string compare "" $current_signal]} {
	set state normal
    }

    .mbar.absb.menu add command -label "Explain layer" -state $state\
	-command {
	    global current_signal
	    text_dialog Explanation [smv_layer $current_signal why]
	}
    
    global have_model
    if {$have_model} {
	global current_signal
	set state disabled
	if {![catch {set e $current_signal}] && [string compare $e ""]} {
	    set state normal
	} else {set e ""}
	.mbar.absb.menu add command -label "(none)" -state $state\
		-command [list my_abs_cmd $e {}]
	.mbar.absb.menu add command -label "free" -state $state\
		-command [list my_abs_cmd $e free]
	.mbar.absb.menu add command -label "other..." -state $state\
		-command "other_abs_cmd $e"
	foreach x [smv_layers] {
	    .mbar.absb.menu add command -label $x -state $state\
		    -command [list my_abs_cmd $e $x]
	}
    }
}
# .mbar add cascade -label Abstraction -menu .mbar.absb.menu -underline 0

    
# . configure -menu .mbar


pack .mbar.fileb -side left
pack .mbar.propb -side left
pack .mbar.viewb -side left
pack .mbar.gotob -side left
pack .mbar.histb -side left
pack .mbar.absb -side left
pack .mbar.helpb -side right

#pack .p.p1.nb.nbframe.sf.cs_scroll -side right -fill y
pack .p.p1.nb.nbframe.sf.closed_signals -side left -fill both -expand 1
# pack .p.p2.nb.nbframe.textframe -side top -fill both -expand 1
pack .p.p2.nb.nbframe.textframe.mbar -side top -fill x
pack .p.p2.nb.nbframe.textframe.mbar.file -side left
pack .p.p2.nb.nbframe.textframe.mbar.show -side left
pack .p.p2.nb.nbframe.textframe.text -side left -fill both -expand 1

frame .showprop
pack .showprop -side top -fill both -expand 0
label .showprop.t -text ""
pack .showprop.t -side left
entry .showprop.search -state disabled -width 10
label .showprop.stag -text "i-search:"

pack .showprop.search -side right
pack .showprop.stag -side right

bind .showprop.search <Key> {
    isearch_key %A
}

proc isearch_point {} {
    global isearch_type isearch_window
    return [switch $isearch_type {
	hlist {$isearch_window info anchor}
	grid  {lindex [$isearch_window anchor get] 1}
    }]
}

proc isearch_select {foo} {
    global isearch_type isearch_window
    if {[string match $isearch_type hlist]} {
	$isearch_window selection clear
	$isearch_window selection set $foo $foo
    } else {
	$isearch_window selection set 0 $foo
    }
}

proc isearch_next {pt} {
    global isearch_type isearch_window isearch_dir tracegrid
    if {[string match $isearch_type hlist]} {
	return [$isearch_window info $isearch_dir $pt]
    } else {
	if {[string match $isearch_dir next]} {
	    if {$pt < $tracegrid(size)} {
		incr pt
		return $pt
	    } else {
		return ""
	    }
	} else {
	    if {$pt > 1} {
		set pt [expr $pt - 1]
		return $pt
	    } else {
		return ""
	    }
	}
    }
}

proc isearch_item {pt} {
    global isearch_type isearch_window isearch_dir tracegrid
    if {[string match $isearch_type hlist]} {
	return [$isearch_window item cget $pt 0 -text]
    } else {
	return [$isearch_window entrycget 0 $pt -text]
    }
}

proc isearch_set_point {pt} {
    global isearch_type isearch_window isearch_dir tracegrid
    if {[string match $isearch_type hlist]} {
	$isearch_window anchor set $pt
	$isearch_window see $pt
    } else {
	$isearch_window anchor set 0 $pt
	tracegrid_see $pt
    }
}


proc isearch_key {key} {
    if {![string compare $key "\r"]} {
	global isearch_window
	set foo [isearch_point]
	if {[string compare $foo ""]} {
	    isearch_select $foo
	    global sigtree isearch_type
	    if {[string match $isearch_type hlist]} {
		if {[string compare $isearch_window [$sigtree subwidget hlist]]} {
		    catch {[$isearch_window cget -browsecmd] $foo}
		} else {
		    sigtree_browse $foo
		}
	    }
	}
	global isearch_oldfocus
	if {[string compare $isearch_oldfocus ""]} {
	    focus $isearch_oldfocus
	} else {focus .}
	global isearch_oldsearch
	set isearch_oldsearch [.showprop.search get]
	.showprop.search configure -state normal
	.showprop.search delete 0 end
	.showprop.search configure -state disabled
	return
    }
    if {[string compare $key " "] >= 0 && [string compare $key "~"] <= 0} {
	
	.showprop.search configure -state normal
	.showprop.search insert end $key
	.showprop.search configure -state disabled
	isearch_do forw
    }
}



proc isearch_do {cmd} {
    set pat [.showprop.search get]
    if {[string compare $pat ""]} {
	set pt [isearch_point]
	regsub -all {\[|\]} $pat {\\&} pat
	switch $cmd {
	    next {set pt [isearch_next $pt]}
	}
	while {[string compare $pt ""]} {
	    set foo [isearch_item $pt]
	    if {[string match *${pat}* $foo]} {
		isearch_set_point $pt
		return
	    }
	    set pt [isearch_next $pt]
	}
	bell
    }
}

bind .showprop.search <KeyPress-Delete> {isearch_delete}

proc isearch_delete {} {
    .showprop.search configure -state normal
    .showprop.search delete [expr [.showprop.search index end] - 1]
    .showprop.search configure -state disabled
    global isearch_anchor
    isearch_set_point $isearch_anchor
    isearch_do forw
}

bind .showprop.search <Control-s> {
    global isearch_dir
    set isearch_dir next
    isearch_do next
}

bind .showprop.search <Control-r> {
    global isearch_dir
    set isearch_dir prev
    isearch_do next
}


bind .showprop.search <Control-g> {
    bell
    global $isearch_anchor $isearch_window $isearch_oldfocus
    if {[string compare $isearch_anchor ""]} {
	isearch_set_point $isearch_anchor
    } else {
	$isearch_window anchor clear
    }
    if {[string compare $isearch_oldfocus ""]} {
	focus $isearch_oldfocus
    } else {focus .}
    .showprop.search configure -state normal
    .showprop.search delete 0 end
    .showprop.search configure -state disabled
}
    
    

set resultstop .p.p1.nb.nbframe.results.sl
set resultssum $resultstop.sum
set resultslist_filter resultslist_no_filter
set resultslist_filter_choice "All results"

frame $resultstop
tixComboBox $resultstop.a -dropdown true \
    -editable false -variable resultslist_filter_choice -command results_choose\
    -options {
	listbox.height 4
    }

proc results_choose {foo} {
    global resultslist_filter
    switch $foo {
	"All results" {set resultslist_filter resultslist_no_filter}
	"Current results" {set resultslist_filter resultslist_current_filter}
	"Current property" {set resultslist_filter resultslist_property_filter}
    }
    global results
    make_results $results
    global the_traces
    global resultslist
    if {$the_traces >= 0} {
	catch {
	    [$resultslist subwidget hlist] selection set $the_traces
	}
    }
}

$resultstop.a insert end "All results"
$resultstop.a insert end "Current results"
$resultstop.a insert end "Current property"

set resultslist .p.p1.nb.nbframe.results.pl

set resultsopts {
    hlist.columns 4
    hlist.header  true
    hlist.separator "\n"
}
lappend resultsopts hlist.font
lappend resultsopts $helvetica

tixScrolledHList $resultslist -options $resultsopts

pack $resultstop -fill x -side top
pack $resultstop.a -side left
pack $resultslist -expand yes -fill both -padx 3 -pady 3 -side left
 
set resultshlist [$resultslist subwidget hlist]

$resultshlist configure -browsecmd resultslist_browse
bindtags $resultshlist [concat [bindtags $resultshlist] isearch_tag]


# Create the title for the HList widget
#	>> Notice that we have set the hlist.header subwidget option to true
#      so that the header is displayed
#

# First some styles for the headers
set style(header) [tixDisplayStyle text  -refwindow $hlist \
	-fg black -anchor c \
        -padx 8 -pady 2\
	-font [tix option get bold_font ]]

$resultshlist header create 0 -itemtype text -text Property \
	-style $style(header)
$resultshlist header create 1 -itemtype text -text Result \
	-style $style(header)
$resultshlist header create 2 -itemtype text -text Time \
	-style $style(header)

# Notice that we use 3 columns in the hlist widget. This way when the user
# expands the windows wide, the right side of the header doesn't look
# chopped off. The following line ensures that the 3 column header is
# not shown unless the hlist window is wider than its contents.
#

$resultshlist column width 3 0

# when we click on a property, make it the current property

proc resultslist_browse {n} {
    set s $n
    make_traces $s
    global results
    set name [lindex [lindex $results $s] 0]
    if {[string compare $name "."] && ![string match *//* $name]} {
	goto_by_name $name
    }
}



if {0} {
  frame .p.p1.nb.nbframe.results.names
  frame .p.p1.nb.nbframe.results.values
  listbox .p.p1.nb.nbframe.results.names.l -font $courier -relief raised -borderwidth 2 -height 3\
	-yscrollcommand ".p.p1.nb.nbframe.results.sb set"
  bindtags .p.p1.nb.nbframe.results.names.l [concat [bindtags .p.p1.nb.nbframe.results.names.l] results_names_tag]
  bind results_names_tag <Button-1> {
      set s [.p.p1.nb.nbframe.results.names.l curselection]
      if {[string compare $s ""]} {
	  make_traces $s
	  global results
	  set name [lindex [lindex $results $s] 0]
	  if {[string compare $name "."] && ![string match *//* $name]} {
	      goto_by_name $name
	  }
      }
  }
  listbox .p.p1.nb.nbframe.results.values.l -font $courier -relief raised -borderwidth 2 -height 3 -width 6\
	-yscrollcommand ".p.p1.nb.nbframe.results.sb set"
  scrollbar .p.p1.nb.nbframe.results.sb -command "results_yview"
  pack .p.p1.nb.nbframe.results.sb -side right -fill y
  pack .p.p1.nb.nbframe.results.names -side left -fill both -expand 1
  pack .p.p1.nb.nbframe.results.names.l -side top -fill both -expand 1
  pack .p.p1.nb.nbframe.results.values -side left -fill both 
  pack .p.p1.nb.nbframe.results.values.l -side top -fill both -expand 1
}

proc CreateOldTraces {} {
    frame .p.p2.nb.nbframe.traces.mbar -relief raised -bd 2
    menubutton .p.p2.nb.nbframe.traces.mbar.file -text File -menu .p.p2.nb.nbframe.traces.mbar.file.menu
    menu .p.p2.nb.nbframe.traces.mbar.file.menu -postcommand {
	global the_traces
	global have_model
	
	.p.p2.nb.nbframe.traces.mbar.file.menu delete 0 last
	
	set state disabled
	if {$have_model} {set state normal}
	
	.p.p2.nb.nbframe.traces.mbar.file.menu add command -state $state -label "New trace" -command {
	    global the_traces
	    global trace_scale
	    smv_newTrace
	    set the_traces -1
	    make_traces $the_traces
	}
	
	.p.p2.nb.nbframe.traces.mbar.file.menu add command -state $state -label "Load from file..." -command {
	    set foo [tk_getOpenFile -filetypes {{"Trace files" {.tra}}\
						    {"All files" *}} -parent .]
	    if {[string compare $foo ""]} {
		smv_loadTrace $foo
		make_traces -1
	    }
	}
	
	set state disabled
	if {$have_model && [string compare $the_traces ""] != 0} {set state normal}
	
	
	.p.p2.nb.nbframe.traces.mbar.file.menu add command -state $state -label "Save to file..." -command {
	    global the_traces
	    set foo [tk_getSaveFile -filetypes {{"Trace files" {.tra}}\
						    {"All files" *}} -parent .]
	    if {[string compare $foo ""]} {
		smv_saveTrace $the_traces $foo
	    }
	}
    }
    
    menubutton .p.p2.nb.nbframe.traces.mbar.run -text Run -menu .p.p2.nb.nbframe.traces.mbar.run.menu
    menu .p.p2.nb.nbframe.traces.mbar.run.menu -postcommand {
	global the_traces
	global have_model
	
	.p.p2.nb.nbframe.traces.mbar.run.menu delete 0 last
	
	set state disabled
	if {$have_model && [string compare $the_traces ""] != 0} {set state normal}
	
	.p.p2.nb.nbframe.traces.mbar.run.menu add command -state $state -label "Execute trace" -command {
	    global the_traces
	    global trace_scale
	    smv_runTrace $the_traces
	    set_scale $trace_scale
	}
	
	.p.p2.nb.nbframe.traces.mbar.run.menu add command -state $state -label "Extend trace" -command {
	    global the_traces
	    global trace_scale
	    
	    set ans\
		[string_dialog .d "Trace extension"\
		     "Extend trace by how many steps?" "" "" 0 "OK" "Cancel"]
	    if {[lindex $ans 0] == 0} {
		smv_extendTrace $the_traces [lindex $ans 1]
		make_traces $the_traces
	    }
	}
    }
    
    proc clear_traces {}  {
	.p.p2.nb.nbframe.traces.names.l configure -state normal
	.p.p2.nb.nbframe.traces.values.l configure -state normal
	.p.p2.nb.nbframe.traces.names.l delete 1.0 end
	.p.p2.nb.nbframe.traces.values.l delete 1.0 end
	.p.p2.nb.nbframe.traces.names.l configure -state disabled
	.p.p2.nb.nbframe.traces.values.l configure -state disabled
    }
    
    menubutton .p.p2.nb.nbframe.traces.mbar.view -text View -menu .p.p2.nb.nbframe.traces.mbar.view.menu
    menu .p.p2.nb.nbframe.traces.mbar.view.menu -postcommand {
	global the_traces
	global have_model
	
	.p.p2.nb.nbframe.traces.mbar.view.menu delete 0 last
	
	.p.p2.nb.nbframe.traces.mbar.view.menu add command -label "Clear traces" -command clear_traces
	
	
	
	.p.p2.nb.nbframe.traces.mbar.view.menu add command -label "Add trace(s)" -command {
	    global the_traces
	    global trace_index
	    global signals_list
	    global current_signal
	    if {$exists_results && [!catch {set name $current_signal}] &&\
		    [string compare "" $name]} {
		set traces [smv_trace $the_traces $name]
		if {[llength $traces] == 0} {
		    tk_dialog .d "No Signal Trace" \
			"There is no signal trace for $name" \
			warning 0 "OK"
		} else {
		    foreach y $traces {
			make_trace $y
		    }
		}
		.p.p2.nb.nbframe.traces.names.l see end
		.p.p2.nb.nbframe.traces.values.l see end
	    }
	}
	
	.p.p2.nb.nbframe.traces.mbar.view.menu add command -label "Delete trace" -command {
	    global the_traces
	    global trace_selection
	    if {$exists_results} {
		.p.p2.nb.nbframe.traces.names.l delete [expr $trace_selection+1].0\
		    [expr $trace_selection+1].end
		.p.p2.nb.nbframe.traces.values.l delete [expr $trace_selection+1].0\
		    [expr $trace_selection+1].end
	    }
	}
	
	.p.p2.nb.nbframe.traces.mbar.view.menu add command -label "Save trace view" -command {
	    set foo [tk_getSaveFile -filetypes {{"Trace view files" {.tvw}}\
						    {"All files" *}} -parent .]
	    if {[string compare $foo ""]} {
		save_traces $foo
	    }
	}
	
	.p.p2.nb.nbframe.traces.mbar.view.menu add command -label "Restore trace view" -command {
	    set foo [tk_getOpenFile -filetypes {{"Trace view files" {.tvw}}\
						    {"All files" *}} -parent .]
	    if {[string compare $foo ""]} {
		restore_traces $foo 1
	    }
	    
	}
	
	.p.p2.nb.nbframe.traces.mbar.view.menu add separator
	
	.p.p2.nb.nbframe.traces.mbar.view.menu add radiobutton -label "Show all traces" -variable tracesShowAll -value 1 -command {
	    global trace_scale
	    set_scale $trace_scale
	}
	.p.p2.nb.nbframe.traces.mbar.view.menu add radiobutton -label "Show requested traces" -variable tracesShowAll -value 0 -command {
	    clear_traces
	}
	
	
    }
    
    
    pack .p.p2.nb.nbframe.traces.mbar -side top -fill x
    pack .p.p2.nb.nbframe.traces.mbar.file -side left
    pack .p.p2.nb.nbframe.traces.mbar.run -side left
    pack .p.p2.nb.nbframe.traces.mbar.view -side left
    
    
    
    frame .p.p2.nb.nbframe.traces.names
    frame .p.p2.nb.nbframe.traces.values
    scrollbar .p.p2.nb.nbframe.traces.sb -command "trace_yview"
    scrollbar .p.p2.nb.nbframe.traces.names.sb -orient horizontal -command ".p.p2.nb.nbframe.traces.names.l xview"
    scrollbar .p.p2.nb.nbframe.traces.values.sb -orient horizontal -command ".p.p2.nb.nbframe.traces.values.l xview"
    text .p.p2.nb.nbframe.traces.names.top -state disabled\
	-font $courier -relief raised -borderwidth 2 -height 1 -width 20\
	-wrap none -cursor hand2
    text .p.p2.nb.nbframe.traces.names.l -state disabled\
	-font $courier -relief raised -borderwidth 2 -height 15 -width 20\
	-yscrollcommand ".p.p2.nb.nbframe.traces.sb set"\
	-xscrollcommand ".p.p2.nb.nbframe.traces.names.sb set"\
	-wrap none -cursor hand2
    #  bindtags .p.p2.nb.nbframe.traces.names.l [concat [bindtags .p.p2.nb.nbframe.traces.names.l] trace_names_tag]
    bind .p.p2.nb.nbframe.traces.names.l <Button-1> "trace_list_click %x %y"
    
    proc trace_list_click {x y} {
	global have_model
	if {$have_model} {
	    set lc [.p.p2.nb.nbframe.traces.names.l index @$x,$y]
	    set l [expr [string range $lc 0 [expr [string first . $lc] - 1]]]
	    global trace_selection
	    set trace_selection [expr $l - 1]
	    global trace_selection_name
	    set trace_selection_name [.p.p2.nb.nbframe.traces.names.l get $l.0 $l.end]
	    highlight_current_state
	    goto_by_name $trace_selection_name
&&&
	}
    }
    
    
    text .p.p2.nb.nbframe.traces.values.top -state disabled\
	-font $courier -relief raised -borderwidth 2 -height 1\
	-wrap none -cursor hand2
    
    proc select_state_press {x y} {
	global have_model
	if {$have_model} {
	    set lc [.p.p2.nb.nbframe.traces.values.top index @$x,$y]
	    set c [string range $lc [expr [string first . $lc] + 1] end]
	    global current_state
	    global trace_scale
	    set current_state [expr $c / $trace_scale]
	    highlight_current_state
	    see_signal
	}
    }
    
    bind  .p.p2.nb.nbframe.traces.values.top <Button-1> "select_state_press %x %y"
    text .p.p2.nb.nbframe.traces.values.l  -state disabled\
	-font $courier -relief raised -borderwidth 2 -height 15 -width 80\
	-yscrollcommand ".p.p2.nb.nbframe.traces.sb set"\
	-xscrollcommand ".p.p2.nb.nbframe.traces.values.sb set"\
	-wrap none -cursor hand2
    bind .p.p2.nb.nbframe.traces.values.l <Button-1> "trace_value_click %x %y"
    bind .p.p2.nb.nbframe.traces.values.l <Double-Button-1> "trace_value_double %x %y"
    
    proc trace_value_click {x y} {
	global have_model
	if {$have_model} {
	    set lc [.p.p2.nb.nbframe.traces.values.l index @$x,$y]
	    set l [expr [string range $lc 0 [expr [string first . $lc] - 1]]]
	    set c [string range $lc [expr [string first . $lc] + 1] end]
	    global current_state
	    global trace_scale
	    set current_state [expr $c / $trace_scale]
	    global trace_selection
	    set trace_selection [expr $l - 1]
	    global trace_selection_name
	    set trace_selection_name [.p.p2.nb.nbframe.traces.names.l get $l.0 $l.end]
	    highlight_current_state
	    goto_by_name $trace_selection_name
	}
    }
    
    proc trace_value_double {x y} {
	global have_model
	global trace_selection_name
	global current_state
	global the_traces
	if {$have_model && [string length $trace_selection_name] != 0 && [string length $the_traces] != 0} {
	    set foo [string_dialog .d\
			 "Value entry"\
			 "Enter a value for $trace_selection_name at state $current_state"\
			 "" "" 0 "Override" "Suggest" "Cancel"]
	    if {[lindex $foo 0] < 2} {
		if {[lindex $foo 0]==1} {
		    set bar =
		} else {
		    set bar :=
		}
		smv_modTrace $the_traces $current_state $trace_selection_name\
		    $bar [string trim [lindex $foo 1]]
	    }
	    global trace_scale
	    set_scale $trace_scale
	}
    }
    
    
    # pack .p.p2.nb.nbframe.traces -side top -fill x
    pack .p.p2.nb.nbframe.traces.sb -side right -fill y
    pack .p.p2.nb.nbframe.traces.names -side left -fill both
    pack .p.p2.nb.nbframe.traces.names.sb -side bottom -fill x
    pack .p.p2.nb.nbframe.traces.names.top -side top -fill x
    pack .p.p2.nb.nbframe.traces.names.l -side top -fill both -expand 1
    pack .p.p2.nb.nbframe.traces.values -side left -fill both -expand 1
    pack .p.p2.nb.nbframe.traces.values.sb -side bottom -fill x
    pack .p.p2.nb.nbframe.traces.values.top -side top -fill x
    pack .p.p2.nb.nbframe.traces.values.l -side top -fill both -expand 1
}
# the groups view

frame .p.p1.nb.nbframe.groups.t
frame .p.p1.nb.nbframe.groups.t.names
frame .p.p1.nb.nbframe.groups.t.values
label .p.p1.nb.nbframe.groups.t.names.lab -justify left -text "Groups:"
listbox .p.p1.nb.nbframe.groups.t.names.l -font $courier -relief raised -borderwidth 2 -height 15\
    -yscrollcommand ".p.p1.nb.nbframe.groups.t.names.vsb set"\
    -xscrollcommand ".p.p1.nb.nbframe.groups.t.names.sb set"
bindtags .p.p1.nb.nbframe.groups.t.names.l [concat [bindtags .p.p1.nb.nbframe.groups.t.names.l] groups_names_tag]
bind groups_names_tag <Button-1> {
    choose_group [selection get]
}
bind .p.p1.nb.nbframe.groups.t.names.l <Double-Button-1> {}
label .p.p1.nb.nbframe.groups.t.values.lab -justify left -text ""
listbox .p.p1.nb.nbframe.groups.t.values.l -font $courier -relief raised -borderwidth 2 -height 15 -width 40\
    -yscrollcommand ".p.p1.nb.nbframe.groups.t.values.vsb set"\
    -xscrollcommand ".p.p1.nb.nbframe.groups.t.values.sb set"
scrollbar .p.p1.nb.nbframe.groups.t.names.vsb -orient vertical -command ".p.p1.nb.nbframe.groups.t.values.l yview"
scrollbar .p.p1.nb.nbframe.groups.t.values.vsb -orient vertical -command ".p.p1.nb.nbframe.groups.t.values.l yview"
scrollbar .p.p1.nb.nbframe.groups.t.names.sb -orient horizontal -command ".p.p1.nb.nbframe.groups.t.names.l xview"
scrollbar .p.p1.nb.nbframe.groups.t.values.sb -orient horizontal -command ".p.p1.nb.nbframe.groups.t.values.l xview"
frame .p.p1.nb.nbframe.groups.b

set current_group ""
proc choose_group {n} {
    .p.p1.nb.nbframe.groups.t.values.l delete 0 end
    foreach x [smv_getGroup $n] {
	.p.p1.nb.nbframe.groups.t.values.l insert end $x
    }
    .p.p1.nb.nbframe.groups.t.values.lab configure -text "Contents of $n:"
    global current_group
    set current_group $n
}

button .p.p1.nb.nbframe.groups.b.new -text "New group" -command {
    set ans [string_dialog .d "Enter group name" "Enter a name for a new property group:" "" "" 0 "OK" "Cancel"]
    if {[lindex $ans 0] == 0} {
	set n [lindex $ans 1]
	eval [concat smv_setGroup $n [smv_getGroup $n]]
	teardown_groups
	setup_groups
    }
}
button .p.p1.nb.nbframe.groups.b.add -text "Add" -command {
    global current_signal
    if {[string length $current_group] > 0} {
	if {[!catch {set sig $current_signal}] &&\
		[string compare "" $sig]} {
	    .p.p1.nb.nbframe.groups.t.values.l insert end $sig
	    eval [concat smv_setGroup $current_group [.p.p1.nb.nbframe.groups.t.values.l get 0 end]]
	}
    }
}

button .p.p1.nb.nbframe.groups.b.del -text "Delete" -command {
    if {[string length $current_group] > 0} {
	foreach x [.p.p1.nb.nbframe.groups.t.values.l curselection] {
	    .p.p1.nb.nbframe.groups.t.values.l delete $x
	}
	eval [concat smv_setGroup $current_group [.p.p1.nb.nbframe.groups.t.values.l get 0 end]]
    }
}

pack .p.p1.nb.nbframe.groups.t -side top -fill x
pack .p.p1.nb.nbframe.groups.t.names -side left -fill both
pack .p.p1.nb.nbframe.groups.t.names.lab -side top -fill x -expand 1
pack .p.p1.nb.nbframe.groups.t.names.vsb -side right -fill y
pack .p.p1.nb.nbframe.groups.t.names.sb -side bottom -fill x
pack .p.p1.nb.nbframe.groups.t.names.l -side top -fill both -expand 1
pack .p.p1.nb.nbframe.groups.t.values -side left -fill both -expand 1
pack .p.p1.nb.nbframe.groups.t.values.lab -side top -fill x -expand 1
pack .p.p1.nb.nbframe.groups.t.values.vsb -side right -fill y
pack .p.p1.nb.nbframe.groups.t.values.sb -side bottom -fill x
pack .p.p1.nb.nbframe.groups.t.values.l -side top -fill both -expand 1
pack .p.p1.nb.nbframe.groups.b -side top -fill x
pack .p.p1.nb.nbframe.groups.b.new -side left -expand 1 -padx 3m -pady 2m
pack .p.p1.nb.nbframe.groups.b.add -side left -expand 1 -padx 3m -pady 2m
pack .p.p1.nb.nbframe.groups.b.del -side left -expand 1 -padx 3m -pady 2m


proc teardown_groups {} {
    .p.p1.nb.nbframe.groups.t.names.l delete 0 end
    .p.p1.nb.nbframe.groups.t.values.l delete 0 end
    .p.p1.nb.nbframe.groups.t.values.lab configure -text ""
}

proc setup_groups {} {
    teardown_groups
    set grps [smv_getGroups]
    foreach x $grps {
	.p.p1.nb.nbframe.groups.t.names.l insert end $x
    }
}



# bind .p.p1.nb.nbframe.sf.closed_signals <Double-Button-1> {
#  DoubleClickSignal
# }

# bindtags .p.p1.nb.nbframe.sf.closed_signals [concat [bindtags .p.p1.nb.nbframe.sf.closed_signals] closed_signals_tag]
# bind closed_signals_tag <ButtonRelease-1> {
#    catch {
#	set e [lindex $signals_list [.p.p1.nb.nbframe.sf.closed_signals curselection]]
#	set x [string trim [lindex $e 0]]
#	add_to_hist $x
#	see_signal
#    }
#}

proc bsr_fun {l} {
    set n ""
    foreach x $l {
	set i [string first \[ $x]
	if {$i >= 0 } {
	    append n [string range $x $i end]
	} else {
	    if {![string match "" $n]} {append n .}
	    append n $x
	}
    }
    if {[string match "" $n]} {set n .}
    goto_by_name $n
    set r [smv_children $n]
    set s ""
    foreach x $r {
	lappend s [string range $x [string last . $x] end ]
    }
    return $s
}






set smv_filterSelected 1
set viewRequestedLayer 0
set the_props ""
set have_model 0


proc show_error {msg} {
    if {[scan $msg { "%[^\"]", line %d:} f l] == 2} {
	set foo [list $f $l]
    } else {
    set foo [smv_where]
    }
    SetFile [lindex $foo 0] [lindex $foo 1]
    global source_text
    $source_text configure -state normal
    $source_text insert [expr [lindex $foo 1] + 1].0 "$msg" msg
    $source_text tag configure msg -foreground red
    $source_text configure -state disabled
    $source_text see [expr [lindex $foo 1] + 1].0
    .p.p2.nb raise textframe
    tk_dialog .d "Error" \
	"A source file error occurred\n(see the source view window)" \
	error 0 "Dismiss"
}


proc run_editor_on_file {line file} {
    if {[catch {
#	exec gnuclient -q +$line $file
	exec gnuclient -batch -eval "(let ((last-command-event (make-event 'button-press '(button 1)))) (raise-frame) (find-file \"[file join [pwd] $file]\") (goto-line $line) (focus-frame (selected-frame)))"
    } msg]} {
	set ans [tk_dialog .d "Question" \
		     "Cannot connect to XEmacs \n to edit file $file. \n Perhaps no XEmacs is running. \n Shall I try to start one?\n  " \
		     warning 0 "Yes" "No"]
	if {$ans == 0} {
	    if {[catch {exec xemacs +$line $file &} msg]} {
		show_error "Can't run XEmacs. \n Perhaps XEmacs is not properly installed. See the SMV installation instructions."
	    }
	} else {
	    show_error "If XEmacs is already running, it may be that it is not running gnuserv. See the SMV installation instructions."
	}
    }
}

proc save_editor_files {} {
    catch {
	exec gnuclient -batch -eval "(let ((last-command-event (make-event 'button-press '(button 1)))) (raise-frame)  (focus-frame (selected-frame)) (save-some-buffers))"
    }
    raise .
    focus .
    wm deiconify .
}

proc check_mod_time {} {
    global smv_init_time
    global the_props

    save_editor_files

    if {[smv_modTime] > $smv_init_time} {
	set ans [tk_dialog .d "Warning" \
		     "Source files are modified on disk." \
		     warning 0 "Reopen" "Cancel"]
	if {$ans == 0} {
	    set foo $the_props
	    shut_it_down
	    set the_props $foo
	    fire_it_up
	} else {throw "Files modified on disk"}
    }
}
	

proc fire_it_up {} {
  global have_model
  global the_props
    global smv_file_name
    global smv_init_time
    
    set have_model 0
    if {![string compare $smv_file_name ""]} {return}

    wm title . "$smv_file_name"
    wm iconname . "$smv_file_name"


  if {[catch {eval "smv_init $smv_file_name"} msg]} {
        show_error $msg
	set have_model 0
  } else {
    set smv_init_time [smv_modTime]
    if {[llength $the_props] != 0} {
        if {[catch {eval "smv_props $the_props"} msg]} {
	  show_error $msg
	  set the_props ""
        }
    } else {
      set choices [smv_update]
	if {[llength $choices] == 1} {choose_prop [list [lindex $choices 0]]}
    }
      get_results
#      tracegrid_restore_view [smv_extension traces] 0
      global tracegrid
      set tracegrid(show_all) [expr ![file exists [smv_extension traces]]]
      set have_model 1
      global signals_list
      set e [lindex $signals_list  0]
#      SetFile [lindex $e 2] [lindex $e 3]
      setup_groups
      toplevel .bsr
    wm title .bsr "$smv_file_name browser"
    wm iconname .bsr "$smv_file_name browser"
    wm protocol .bsr WM_DELETE_WINDOW { }
    wm withdraw .bsr

      browsebox .bsr.bsr bsr_fun
      pack .bsr.bsr
  }
}

proc shut_it_down {} {
    global moded
    global have_model
    global the_props
    global the_traces
    if {$have_model} {
	if {$moded} {
	    set ans  [tk_messageBox -icon question -type yesnocancel \
			  -title "File Modified" -parent .\
			  -message "Save changes to abstraction?"]
	    
	    case $ans {
		yes my_write_using
		cancel {throw "Cancelled"}
	    }
	}
	global tracegrid
	if {$tracegrid(show_all)} {
	    file delete [smv_extension traces]
	} else {
	    tracegrid_save_view [smv_extension traces]
	}
	teardown_groups
	catch {destroy .bsr}
	smv_quit
	set have_model 0
	set the_props ""
	set the_traces ""
    }
    global cur_file
    set cur_file ""
}

proc make_options_from_hash {the_options} {
    global options_hash
    set res ""
    foreach option $the_options {
	set name [lindex $option 0]
	catch {
	    set val $options_hash($name)
	    if {[string length $val] > 0} {
		if {[lindex $option 2] == 0} {
		    append res " $name=$val"
		} elseif {[lindex $option 2] == 1} {
		    append res " $name=$val"
		}
	    }
	}
    }
    return $res
}

proc make_options {} {
  set the_options [smv_options]
  set res ""
  foreach option $the_options {
    set switch [lindex $option 1]
    set arg [lindex $option 2]
    set val [lindex $option 4]
    if {[string length $val] > 0} {
        if {$arg == 0} {
          if {$val} {append res " -"  $switch}
        } else {
        if {$arg == 1} {
	  append res " -"  $switch " " $val
        }}}
   }
  return $res
}


#  .p.p2.nb.nbframe.textframe.text configure -state normal
#  .p.p2.nb.nbframe.textframe.text insert end "Copyright 1996 Cadence Berkeley Labs. Cadence Design Systems."
#  .p.p2.nb.nbframe.textframe.text configure -state disabled

proc flash_window {w} {
    set x [expr [winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
	    - [winfo vrootx [winfo parent $w]]]
    set y [expr [winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
	    - [winfo vrooty [winfo parent $w]]]
    wm geom $w +$x+$y
    wm deiconify $w

    update idletasks
    tkwait visibility $w
    after 3000 destroy $w
}


update idletasks



proc flash_license {} {
    global tkPriv

    set oldFocus [focus]

    toplevel .lic
    set w .lic
    wm title .lic "License Agreement"
    wm iconname $w Dialog
    wm protocol $w WM_DELETE_WINDOW { }
    wm transient $w [winfo toplevel [winfo parent $w]]

    label .lic.msg -wraplength 6i -justify left -text \
     {This software is made available subject to the following
lecense agreement. Please read it carefully, and if you
agree to the terms, click "I agree" below.
}\
    -font {Times 11}
    pack .lic.msg -side top -fill x -expand 1 -padx 3m -pady 3m

    frame $w.top -relief raised -bd 1
    pack $w.top -side top -fill both
    frame $w.bot -relief raised -bd 1
    pack $w.bot -side bottom -fill both

    # 2. Fill the top part with the text

    tixScrolledText $w.top.st
    [$w.top.st subwidget text] insert 1.0 \
{

SOFTWARE LICENSE AGREEMENT FOR RESEARCH AND EVALUATION

 Copyright 2002 Cadence Design Systems, Inc.  All Rights Reserved.


THIS SOFTWARE LICENSE AGREEMENT ("AGREEMENT") IS A LEGAL DOCUMENT BETWEEN
YOU AND CADENCE DESIGN SYSTEMS, INC. ("CADENCE"). PLEASE READ THIS
AGREEMENT CAREFULLY BEFORE ACCESSING THE SOFTWARE FROM THIS LOCATION (THE
"LICENSED PROGRAM"). BY USING, COPYING, DOWNLOADING OR DISTRIBUTING THE
LICENSED PROGRAM, YOU ARE AGREEING TO BE BOUND BY THE TERMS OF THIS
AGREEMENT AS OF THE DATE YOU TAKE SUCH ACTION.  You are also representing
to Cadence that you have the legal authority to accept the terms of this
Agreement on behalf of yourself or the party you represent.  In this
Agreement, "You" refers to both yourself individually and your company or
employer for whom you are using, copying, downloading or distributing the
Licensed Program.


If you agree to the terms and conditions of this Agreement, click on the "I
AGREE" button at the end of the Agreement, and you will be permitted to
proceed to access the Software.  IF YOU DO NOT WANT TO BE BOUND BY THE
TERMS OF THIS AGREEMENT, CADENCE IS UNWILLING TO LICENSE THE SOFTWARE TO
YOU.  If you do not agree to all of the terms and conditions of this
Agreement, click on the "I DO NOT AGREE" button at the end of this
Agreement and you will be returned to the previous page.


--------------------------------


THIS AGREEMENT sets out the terms under which Cadence is prepared to allow
you access to the Licensed Programs.  The Licensed Programs accessed
through this Site shall be used solely for testing and evaluation purposes.
 YOU ARE NOT AUTHORIZED TO USE THE LICENSED PROGRAMS FOR COMMERCIAL OR
DEVELOPMENT ACTIVITIES.  If you wish to obtain a license for use in
commercial or development activities, please contact mcmillan@cadence.com.



1.  GRANT OF LICENSE.


So long as you comply with the terms of this Agreement, Cadence grants to
You a nonexclusive, non-transferable, temporary, royalty-free, limited
right to use the Licensed Program and any documentation provided with it
("Product") solely for the purpose of testing and evaluating the Licensed
Program for its suitability for use with Your internal designs and design
processes.  YOU ARE NOT AUTHORIZED TO USE THE LICENSED PROGRAMS FOR
COMMERCIAL OR DEVELOPMENT ACTIVITIES.  Cadence reserves the right to
terminate your rights under this Agreement and to seek any other legal
remedies if you violate any provisions hereof and, in the event of such
termination, you agree to return the Product to Cadence or completely
delete all copies from your systems.


2.  SINGLE USER LICENSE.

This license entitles You to use one copy of the Product on a single
computer at a time at Your location.  You are not entitled to make copies
of the Product, except one archival copy for back-up purposes only.  All
legends, trademarks, trade names, copyright marks and other identifications
must also be copied when copying the Product.


3.  OTHER RESTRICTIONS.


The Product is the sole and exclusive property of Cadence.


You agree not to copy, modify, sell, lease, permit third parties to use or
access, or transfer the Product or any copy, in whole or in part.  You
agree not to reverse engineer, decompile, disassemble, or make any attempt
to discover the source code to the Licensed Program.



4. TERM AND TERMINATION.


Your license to use the Product expires 6 months after you obtain access to
it.


All Your rights under this Agreement shall terminate if You fail  to  comply
with any of the material  terms  or  conditions  of  this  Agreement.   Upon
termination of  this  Agreement,  your  license  to  use  the  Product  will
immediately terminate and You agree to destroy all copies of the Product  as
soon as  reasonably  practicable.   However,  Your  obligations  under  this
Agreement shall survive such termination.



5.  NO WARRANTY.


THE PRODUCT IS LICENSED TO YOU "AS IS", WITHOUT WARRANTIES OF ANY KIND,
EITHER EXPRESS OR IMPLIED, INCLUDING ANY WARRANTY OF MERCHANTABILITY OR
FITNESS FOR A PARTICULAR PURPOSE OR NONINFRINGEMENT.  YOU ARE solely
responsible for determining the appropriateness of use OF THE PRODUCT and
assume all risks associated with YOUR exercise of rights under this
Agreement.


Cadence does not provide any support, assistance, installation, training or
other services, updates, or enhancements related to the Product.



6.  LIMITATION OF LIABILITY.


CADENCE SHALL HAVE NO LIABILITY FOR ANY DAMAGE, HOWEVER CAUSED, ARISING OUT
OF THE USE OF THE PRODUCT, INCLUDING ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING WITHOUT LIMITATION
LOST PROFITS), WHETHER FOR BREACH OF WARRANTY, CONTRACT, TORT, NEGLIGENCE,
STRICT LIABILITY OR OTHERWISE.


7.  NO ASSIGNMENT.


You may not transfer or assign this Agreement, or any part thereof, to any
other party (by operation of law or otherwise), and any attempt to do so
shall be void.


8.  EXPORT.


This Agreement does not permit export of the Licensed Program or related
documentation outside of the United States.  You agree to comply with all
U.S. laws regarding export and all necessary approval and license
requirements of the U.S. Department of Commerce and other agencies or
departments of the U.S. Government.



9.  U.S.A. GOVERNMENT RESTRICTED RIGHTS.


The Product includes "commercial computer software" and "commercial
computer software documentation" as such terms are used in 48 C.F.R. 12.212
(SEPT 1995) and is provided to the Government (i) for acquisition by or on
behalf of civilian agencies, consistent with the policy set forth in 48
C.F.R. 12.212; or (ii) for acquisition by or on behalf of units of the
Department of Defense, consistent with the policies set forth in 48 C.F.R.
227.7202-1 (JUNE 1995) and 227.7202-3 (JUNE 1995). For further information,
contact Cadence Design Systems, Inc., 555 River Oaks Parkway, San Jose, CA
95134 U.S.A.



10.  GENERAL.


The invalidity or unenforceability of any provision hereof shall in  no  way
affect the validity or enforceability of any other provision.


This Agreement is governed by the laws of California, without  reference  to
conflict of laws principles.  Each party waives its rights to a  jury  trial
in any resulting litigation.  Any  litigation  relating  to  this  Agreement
shall be subject to the jurisdiction of the federal and state courts of  the
Northern District of California, with venue lying  in  Santa  Clara  County,
California, or the Santa Clara County Superior  Court.  The  application  of
the United Nations Convention on Contracts for  the  International  Sale  of
Goods is expressly excluded.  The provisions  of  this  Agreement  shall  be
construed fairly in accordance with its terms and no rules  of  construction
for or against either party  shall  be  applied  in  the  interpreting  this
Agreement.


This Agreement constitutes the complete agreement between  You  and  Cadence
and may not be modified unless a written amendment is signed by a  corporate
officer of Cadence.


Cadence is a registered trademark and the Cadence logo  is  a  trademark  of
Cadence Design Systems, Inc. All others are properties of their holders.



ACCEPTANCE


By clicking on the  "I  AGREE"  button  below,  or  by  using  the  Licensed
Program, you are legally  binding  yourself  to  the  terms  and  conditions
contained in this Agreement.


To accept  the  terms  and  conditions  of  this  Agreement,  indicate  your
acceptance by clicking  on  the  "I  AGREE  "  button  at  the  end  of  the
Agreement.





}     
    pack $w.top.st -side top -fill both
    
    # 3. Create a row of buttons at the bottom of the dialog.
    
    set default 1
    set i 0
    foreach but [list "I AGREE" "I DISAGREE"] {
	button $w.button$i -text $but -command "set tkPriv(button) $i"
	if {$i == $default} {
	    frame $w.default -relief sunken -bd 1
	    raise $w.button$i $w.default
	    pack $w.default -in $w.bot -side left -expand 1 -padx 3m -pady 2m
	    pack $w.button$i -in $w.default -padx 2m -pady 2m
	    bind $w <Return> "$w.button$i flash; set tkPriv(button) $i"
	} else {
	    pack $w.button$i -in $w.bot -side left -expand 1 \
		-padx 3m -pady 2m
	}
	incr i
    }

    # 4. Withdraw the window, then update all the geometry information
    # so we know how big it wants to be, then center the window in the
    # display and de-iconify it.

    wm withdraw $w
    update idletasks
    set x [expr [winfo screenwidth $w]/2 - [winfo reqwidth $w]/2 \
	    - [winfo vrootx [winfo parent $w]]]
    set y [expr [winfo screenheight $w]/2 - [winfo reqheight $w]/2 \
	    - [winfo vrooty [winfo parent $w]]]
    wm geom $w +$x+$y
    wm deiconify $w

    # 5. Set a grab and claim the focus too.

    grab $w
    tkwait visibility $w
    if {$default >= 0} {
	focus $w.button$default
    } else {
	focus $w
    }

    # 6. Wait for the user to respond, then restore the focus and
    # return the index of the selected button.

    tkwait variable tkPriv(button)
    destroy $w
    focus $oldFocus

    if {$tkPriv(button) != 0} exit
}

if {[string compare $tcl_platform(platform) windows]} {
  if {![file exists $env(HOME)/.smv6386536]} {
    flash_license
    exec touch $env(HOME)/.smv6386536
    }
}

wm protocol . WM_TAKE_FOCUS

toplevel .h
wm title .h "Copyright notice"
label .h.msg -wraplength 6i -justify center -text {This is vw, the smv viewer.

"It does what it does, no more, no less."

Copyright 1998 Cadence Design Systems.
Copyright 1992 Carnegie Mellon University.}\
    -font {Times 11}
pack .h.msg -side right -expand 1 -fill both -padx 3m -pady 3m
wm withdraw .h
update idletasks
tkwait visibility .
flash_window .h
# focus .

proc tixScrolledGrid:B1-Leave {x} {}
proc tixScrolledGrid:B1-Enter {x y z} {}

fire_it_up
#last line
