# ***************************************************************************
# * FC2 PACKAGE SOURCE FILE
# * 
# * xeve-help.tcl -- Tcl Procedures for the Help
# ***************************************************************************

proc Help {contentsList arrayName} {
    global $arrayName

    upvar #0 $arrayName sectionArray
    set w .$sectionArray(Name)
    if [winfo exists $w] {
        wm deiconify $w
        raise $w
        return
    }

    # build widget .help
    catch "destroy $w"
    toplevel $w
    wm withdraw $w
    wm group $w .


    menubutton $w.menubutton \
        -menu "$w.menubutton.m" \
        -text {Section} \
        -anchor w \
        -underline {0}

    menu $w.menubutton.m -tearoff 0
    
    $w.menubutton.m add command \
        -label "Open section" \
        -command "ShowCurrentSection $w [list $contentsList] $arrayName"
    $w.menubutton.m add separator
    $w.menubutton.m add command \
        -label Close \
        -command "CloseHelp $w"

    listbox $w.listbox  \
        -exportselection 0 \
        -setgrid 1 \
        -relief groove

    # $w.listbox configure -cursor hand2
    $w.listbox configure -foreground #0000ff

    $w.listbox configure -selectforeground #ff0000
    $w.listbox configure -selectborderwidth 0

    bind $w.listbox <ButtonPress-1> "SetHelpSectionView %W %y [list $contentsList] $arrayName"
    bind $w.listbox <B1-Motion> "SetHelpSectionView %W %y [list $contentsList] $arrayName"
    # bind $w.listbox <Double-ButtonPress-1> "SetHelpSectionView %W %y [list $contentsList] $arrayName"

    pack $w.menubutton -side top -anchor w
    pack $w.listbox -side top -fill both -expand 1

    set contentsMaxWidth 30
    set contentsMaxHeight 40
    set sectionMaxWidth 55
    set sectionMaxHeight 60

    set contentsWidth 20
    set contentsHeight $contentsMaxHeight
    set sectionWidth 30
    set sectionHeight 20

    set currentindex 1.0
    set i 1
    foreach item $contentsList {
        set el [lindex $item 0]
        $w.listbox insert end "$el\n"
        if {[string length $el] > $contentsWidth} {
            set contentsWidth [string length $el]
        }
        incr i
    }

    set sectionNumber [llength $contentsList]
    if {$sectionNumber <= $contentsMaxHeight} {
        set contentsHeight $sectionNumber
    }

    # Window manager specific configurations
    wm maxsize $w $contentsWidth $contentsHeight
    wm minsize $w $contentsWidth $contentsHeight
    wm title $w $sectionArray(Title)
    wm geometry $w ${contentsWidth}x$contentsHeight

    wm deiconify $w
    raise $w
    return
}

proc CloseHelp { w } {


    catch "destroy $w-section"
    destroy $w
}
    
proc XeveHelp {} {
    global helpContents
    global helpSections

    Help $helpContents helpSections
}

proc AdvancedVerificationHelp {} {
    global advContents
    global advSections

    Help $advContents advSections
}

proc AboutXeve {} {
    global aboutContents
    global aboutSections
    global tcl_version
    global tk_version
    global blifName

    # Help $aboutContents aboutSections

    if {[winfo exists .about]} {
        return
    }
    toplevel .about
    wm withdraw .about
    wm transient .about .
    wm group .about .
    update idletasks
    set x [expr [winfo screenwidth .about]/2 - [winfo reqwidth .about]/2 \
            - [winfo vrootx [winfo parent .about]]]
    set y [expr [winfo screenheight .about]/2 - [winfo reqheight .about]/2 \
            - [winfo vrooty [winfo parent .about]]]
    wm geom .about +$x+$y

    label .about.logo -image $blifName(photo:xeve) -background #ffffff
    message .about.info -background #ffffff -aspect 1500

    bind .about.logo <Any-Button> {catch "destroy .about"}
    bind .about.info <Any-Button> {catch "destroy .about"}
    bind .about <Any-Button> {catch "destroy .about"}

    if {![info exists blifName(xeve:info)]} {
        set blifName(xeve:info) [get_info]
    }

    if {![regexp "version (v\[0-9\]+_\[0-9\]+)"\
            $blifName(xeve:info) str version]} {
        set version "unknown"
    }
    if {![regexp "rcs name: (r\[0-9\]+)" $blifName(xeve:info) str rcs]} {
        set rcs ""
    }
    if {![regexp "released: (\[0-9/\]+)" $blifName(xeve:info) str date]} {
        set date "unknown"
    }
    if {![regexp "compiled on: (\[a-zA-Z0-9/ .\]+)"\
            $blifName(xeve:info) str arch]} {
        set arch "unknown platform"
    }
    if {![regexp "tiger: (\[0-9\.\]+)" $blifName(xeve:info) str tiger]} {
        set tiger "unknown"
    }

    .about.info configure -text \
            "Version: $version ($rcs) for $arch\nBased on TiGeR version $tiger, Tcl/Tk version $tcl_version/$tk_version\nRelease date: $date\nWWW site: http://www.inria.fr/meije/verification/esterel\nAuthor: Amar Bouali -- Contact: esterel-request@sophia.inria.fr"

    pack .about.info -side bottom -fill x -ipadx 10m -ipady 3m

    pack .about.logo -side top -expand 1 -fill both

    wm deiconify .about
}

proc SetHelpSectionView {w y contentsList arrayName} {
    global symbolicName
    global $arrayName

    upvar #0 $arrayName sectionArray
    set index [$w nearest $y]
    $w selection clear 0 end
    $w selection set $index $index
    ShowHelpSection $w $index $contentsList $arrayName
}

proc ShowCurrentSection {w contentsList arrayName} {
    global symbolicName
    global $arrayName

    upvar #0 $arrayName sectionArray
    set index [lindex [$w.listbox curselection] 0]
    if {$index == ""} {
        return
    }
    ShowHelpSection $w.listbox $index $contentsList $arrayName
}

proc ShowHelpSection { sw index contentsList arrayName } {
    global $arrayName

    upvar #0 $arrayName sectionArray

    set contents [lindex $contentsList $index]
    set helpType [lindex $contents 1]
    set section [lindex $contents 0]

    $sw selection clear 0 end
    $sw selection set $index $index

    set w .$sectionArray(Name)-section

    set sectionHelp $sectionArray($section)

    if {![winfo exists $w]} {
        toplevel $w
        wm withdraw $w
        wm title $w $section
        wm minsize $w 40 10
        wm maxsize $w 80 24
        wm geometry $w 49x20
        wm group $w $sw

        frame $w.frame1 -borderwidth 2
        scrollbar $w.frame1.scrollbar \
                -relief {raised} \
                -command "$w.frame1.text yview"

        text $w.frame1.text \
                -yscrollcommand "$w.frame1.scrollbar set" \
                -wrap {word} \
                -padx 5m \
                -pady 1.5m \
                -height 30 \
                -width 50 \
                -setgrid 1

        frame $w.frame2 -borderwidth 2

        button $w.frame2.next -text "Next"
        button $w.frame2.previous -text "Previous"
        button $w.frame2.dismiss -text "Dismiss" -command "destroy $w"

        pack $w.frame2.next -side left -expand 1 -ipadx 2m -ipady 2m
        pack $w.frame2.previous -side left -expand 1 -ipadx 2m -ipady 2m
        pack $w.frame2.dismiss -side left -expand 1 -ipadx 2m -ipady 2m

        pack $w.frame2 -side bottom -fill x

        pack $w.frame1.scrollbar -side right -fill y
        pack $w.frame1.text -side left -expand 1 -fill both

        pack $w.frame1 -side top -expand 1 -fill both
    }
    wm title $w $section
    $w.frame1.text configure -state normal
    $w.frame1.text delete 1.0 end
    switch -exact $helpType {
        text { $w.frame1.text insert end $sectionHelp }
        command { $w.frame1.text insert end [$sectionArray($section)] }
    }
    $w.frame1.text configure -state disabled
    if {$index == 0} {
        $w.frame2.previous configure -state disabled
    } {
        set id [expr $index - 1]
        $w.frame2.previous configure -state normal \
        -command "ShowHelpSection $sw $id [list $contentsList] $arrayName"
    }
    incr index
    if {$index < [llength $contentsList]} {
        $w.frame2.next configure -state normal \
        -command "ShowHelpSection $sw $index [list $contentsList] $arrayName"
    } {
        $w.frame2.next configure -state disabled
    }

    wm deiconify $w
    SetHelpBalloonHelp $w
    update
}

if {![info exist env(XEVE_LIB)]} {
    set env(XEVE_LIB) [pwd]
}
option add *help.helpfile "$env(XEVE_LIB)/help-sections.tcl"

global onLineHelp
set onLineHelp(InitialStep) {
                      Intial Step

To start, select a Blif file as generated by the Esterel compiler
using the call :
   esterel -Lblif foo.strl
or
   esterel -Lblif:-soft foo.strl
if your program has valued signals. The generated Blif file is
called foo.blif. The compiler generates another Blif
file named foo.rel.blif whenever you have defined some relations
over the input signals in your Esterel program. The file foo.rel.blif
is a combinatorial circuit defining a boolean function whose
domain is the valid inputs as characterized by the relations.
To load a Blif file and possibly with its relation file, select
the menu entry "Files:Open FSM (blif format)". Select your
file within the file browser that is popped-up. Atfer that,
a question box asks you if a relation file has to be loaded.
If yes, the file browser is popped-up again to select the
relation file.

Next Tip: FSM Loading and Verification Selection}
set onLineHelp(InitialStep:nextTip) LoadBlif
set onLineHelp(LoadBlif:previousTip) InitialStep

set onLineHelp(LoadBlif) {
                FSM Loading and Verification Selection

You have selected a Blif (or Bddf) file containing the description of
an FSM:

1- Select the verification function you want to apply on the FSM
(either "REDUCE" of "CHECK OUTPUT") by setting the corresponding radio
button.
2- Fix the input/output signals that are
relevant for the verification you want to perform.
3- Push finaly the "Apply" button to call the verification function.

Previous Tip: Initial Step
Next Tip: Signal Fixing}
set onLineHelp(LoadBlif:nextTip) SignalSelection
set onLineHelp(SignalSelection:previousTip) LoadBlif

set onLineHelp(SignalSelection) {
                    Signal Fixing

Signal fixing is available for each verification function. Though
it has a particular meaning in each case, the signal fixing
mechanism is the same in both case.

There are two modes for fixing signals: the selection mode, and the
painting mode.

Selection mode: It is the default mode when you launch Xeve. A signal
list area is in selection mode whenever the button on the bottom of the
signal list area that represents a selection arrow is in a sunken
relief. The selection mode allows you to select signals with mouse
clicks possibly in conjunction with keyboard keys. A selected signal
appears with a gray background. To fix the selected signals to a
specific color, just  click on the desired color. After such a
coloring, the selection remains in its state.

Painting mode: A signal list area is in painting mode whenever the
button on the bottom of the signal list area that represents a
painting brush is in a sunken relief. To pain signals in some color,
select that color. Then pass over the signals with mouse clicks
possibly in conjunction with keyboard keys, to color them in the
selected color.

Previous Tip: FSM Loading and Verification Selection
Next Tip: Signal Selection/Painting Bindings}
set onLineHelp(SignalSelection:nextTip) SignalSelectionBindings
set onLineHelp(SignalSelectionBindings:previousTip) SignalSelection

set onLineHelp(SignalSelectionBindings) {
                Signal Selection/Painting Bindings

The mouse clicks and keyboard keys to select or paint signals are:

<Control-a> | <Control-A> :
     * global selection/painting
<Button-1> :
     * select/paint the underlying signal. In selection mode deselects
       all other selected signals.
<Button-1-Motion> : 
     * selection mode: select all the signals from the
       firstly selected signal to the lastly selected one.
     * painting mode: paint all the signals on which the brush
       passes over.
<Shift-Button-1> :
     * selection mode: select all the signals from the
       lastly selected signal to the underlying signal.
     * painting mode : same as <Button-1>.
<Control-Button-1> :
     * selection mode: add to the current selection the underlying
       signal.
     * painting mode : same as <Button-1>.

Previous Tip: Signal fixing
Next Tip: Color Meanings}
set onLineHelp(SignalSelectionBindings:nextTip) ColorMeanings
set onLineHelp(ColorMeanings:previousTip) SignalSelectionBindings

set onLineHelp(ColorMeanings) {
                        Color Meanings

You can modulate the verification by selecting the signals that 
are relevant for you. You may hide signals from observation, or fix 
some of them to a constant value (0 for absent or 1 for present).
Different possibilities are offered depending on the verification
function that is under selection. A particular palette of colors is
provided for each, with a particular meaning of the colors in each
case. To set a signal to some color, click on the color box in the
corresponding palette and then click on the signal name.

Palette for FSM minimization:
   Both input and output signals may be either observed or hidden,
   i.e. taken and not taken into account during behavior comparison of
   states, respectively. Each signal list is linked to a color palette
   made of two colors:
      - black, for observed;
      - grey, for hidden.

Palette for Output Signal Emission Checking"
   Inputs signals can be given a fixed value or let free:
      - black, to let the signal have any value;
      - blue, to fix the signal to 0 (always absent)
      - red, to fix the signal to 1 (always present)
   Output signal have to be selected for emission checking:"
      - black, not selected;
      - blue, to check the signal is possibly not emitted
      - red, to check the signal is possibly emitted

Previous Tip: Signal Selection/Painting bindings
Next Tip: Output Signals Checking
}
set onLineHelp(ColorMeanings:nextTip) CheckOutput
set onLineHelp(CheckOutput:previousTip) ColorMeanings

set onLineHelp(CheckOutput) {
                     Output Signals Checking

This command checks the emission status of the output signals
you have selected (possibly emitted for red signals, possibly not
emitted for blue ones). When a signal enjoys the status an execution
sequence to a state showing that status is extracted and saved in a
text file in the csimul format. In this case, the file name is
<signal-name>.esi if <signal-name> is the name of the signal. This
file can be loaded and played in the tape player of the Esterel
graphical simulator Xes.

Previous Tip: Color Meanings
Next Tip: FSM Minimization
}
set onLineHelp(CheckOutput:nextTip) Reduce
set onLineHelp(Reduce:previousTip) CheckOutput

set onLineHelp(Reduce) {
                        FSM Minimization

The FSM minimization functionwill reduce your FSM with respect to
a notion of bisimulation equivalence, taking into account only the
relevant signals you have selected. The reduced FSM is generated in
an FC2 format file. This file can be graphically explored by invoking
the "Draw Automaton" button. If you already have a running Atg, use
rather the "Files:Load fc" menu entry from Atg to open any newly
generated FC2 file.

Previous Tip: Output Signals Checking
Next Tip: Minimized FSM Drawing
}
set onLineHelp(Reduce:nextTip) DrawFc2File
set onLineHelp(Fc2File:previousTip) Reduce

set onLineHelp(Fc2File) {
                Minimized FSM Saving in FC2 Files

The minimized FSM is saved in an FC2 format file. Select an
FC2 file name to save your result or simply click on the SAVE button
to select the suggested file name.

Previous Tip: FSM Minimization
Next Tip: Minimized FSM Drawing
}
set onLineHelp(Fc2File:nextTip) DrawFc2File
set onLineHelp(DrawFc2File:previousTip) Fc2File

set onLineHelp(DrawFc2File) {
                   Minimized FSM Drawing

Atg provides exploration functions through a menu bar. Initially, Atg
is in exploring mode: click on a state with your mouse's left button
to drag and place the state's next states and outgoing transitions.
Do the same to all new displayed states. Use the mouse's middle button
to move states, transitions or transition labels.

Previous Tip: Minimized FSM Saving in FC2 Files
}


# -----------------------------------------------------------------------------
# cb_balloonHelp: A simple balloon help for arbitrary widgets.
# Options: w: widget name, text: help text
#
global cb_balloonHelp
option add *balloon.Background LemonChiffon
#option add *balloon.Font fixed

set cb_balloonHelp(stay_on_screen) 1

set cb_balloonHelp(screen_width) [winfo screenwidth .]
set cb_balloonHelp(screen_height) [winfo screenheight .]

proc cb_balloonHelp {w text {delay 1000}} {
    global cb_balloonHelp

    set me ""
    if {[llength $w] > 1} {
        # 2nd element is the number of a menu entry
        set me [lindex $w 1]
        # 1st element the menu itself
        set w [lindex $w 0]
    }
    
    set cb_balloonHelp($w,cursor) [$w cget -cursor]
    set cb_balloonHelp($w,shown) 0

    if {$me == ""} {
        bind $w <Enter> "
        set cb_balloonHelp(id) \
                \[after $delay _cb_balloonDisplay $w \\\{$text\\\} %X\]
        "
        if {! $cb_balloonHelp(stay_on_screen) } {
            bind $w <Motion> "
            set tmp_w \[winfo containing %X %Y\]
            catch \{destroy .cb_balloon\}
            catch \{after cancel \$cb_balloonHelp(id)\}
            catch \{after cancel \$cb_balloonHelp(id,timeout)\}
            if {\$tmp_w == \"%W\"} {
                set cb_balloonHelp(id) \
                \[after $delay _cb_balloonDisplay $w \\\{$text\\\} %X\]
            }
            unset tmp_w
            "
        }
        bind $w <Leave> {
            catch {destroy .cb_balloon}
            catch {after cancel $cb_balloonHelp(id)}
            catch {after cancel $cb_balloonHelp(id,timeout)}
            set cb_balloonHelp(%W,shown) 0
        }
        bind $w <Any-ButtonPress> {
            catch {destroy .cb_balloon}
            catch {after cancel $cb_balloonHelp(id)}
            catch {after cancel $cb_balloonHelp(id),timeout}
            set cb_balloonHelp(%W,shown) 1
        }
        bind $w <Any-Key> [bind $w <Any-ButtonPress>]
    } else {
        set cb_balloonHelp($w,$me,text) $text
        bind $w <Enter> "
        set tmp_me \[%W index @%y\]
        if {\[info exists cb_balloonHelp(%W,\$tmp_me,text)\]} {
            set cb_balloonHelp(id) \
                    \[after $delay _cb_balloonDisplay \
                    $w \\\{\$cb_balloonHelp(%W,\$tmp_me,text)\\\} %X 1\]
        }
        unset tmp_me
        "
        bind $w <Motion> "
        catch \{destroy .cb_balloon\}
        catch \{after cancel \$cb_balloonHelp(id)\}
        catch \{after cancel \$cb_balloonHelp(id,timeout)\}
        set tmp_me \[%W index @%y\]
        set cb_balloonHelp($w,shown) 0
        if {\[info exists cb_balloonHelp(%W,\$tmp_me,text)\]} {
            set cb_balloonHelp(id) \
                    \[after $delay _cb_balloonDisplay \
                    $w \\\{\$cb_balloonHelp(%W,\$tmp_me,text)\\\} %X 1\]
        }
        unset tmp_me
        "
        bind $w <Leave> {
            catch {destroy .cb_balloon}
            catch {after cancel $cb_balloonHelp(id)}
            catch {after cancel $cb_balloonHelp(id,timeout)}
            #catch {%W config -cursor $cb_balloonHelp(%W,cursor)}
            set cb_balloonHelp(%W,shown) 0
        }
        bind $w <Any-ButtonPress> [bind $w <Leave>]
        bind $w <Any-Key> [bind $w <Any-ButtonPress>]
    }
}

set cb_tools(balloon_help) 1

proc _cb_balloonDisplay {win text rx {menu 0}} {
    global cb_balloonHelp cb_tools

    if {!$cb_tools(balloon_help) || $cb_balloonHelp($win,shown)} {
        return
    }
    if {[winfo containing [winfo pointerx .] [winfo pointery .]] != $win} {
        return
    }

    if {$text == ""} {
        return
    }

    set cb_balloonHelp($win,shown) 1
    
    catch {destroy [set t .cb_balloon]}
    toplevel $t
    wm withdraw $t
    label $t.balloon -text $text -wraplength 200 -justify left \
            -bd 1 -relief raised
    pack $t.balloon ;# -padx 1 -pady 1
    wm overrideredirect $t 1

    set bw  [winfo reqwidth $t.balloon]
    set bh  [winfo reqheight $t.balloon]

    set px [winfo pointerx $win]
    if {$px != -1 } {
        set rx $px
    }
    set x [expr $rx + 2]
    set y [expr [winfo rooty $win] + [winfo height $win] + 2]

    # make help window be completely visible
    if {$x + $bw > $cb_balloonHelp(screen_width)} {
        set x [expr $cb_balloonHelp(screen_width) - $bw]
    }
    if {$y + $bh > $cb_balloonHelp(screen_height)} {
        set y [expr [winfo rooty $win] - $bh - 2]
        if {$y < 0} {
            set y 0
        }
    }

    wm geometry $t +$x+$y
    wm deiconify $t
    # the original cursor is saved in cb_balloonHelp
    #$w config -cursor arrow

    # remove the balloon window after 5 seconds:
    if {! $cb_balloonHelp(stay_on_screen)} {
        set cb_balloonHelp(id,timeout) \
                [after [expr 3000 + [string length $text] * 50] \
                "catch \{destroy $t\}"]
    }
}

proc SetBalloonHelp {} {
    global symbolicName

    cb_balloonHelp $symbolicName(VerifyButton) \
            "Apply the selected verification on the FSM" 500

    cb_balloonHelp $symbolicName(CheckOutputButton) \
            "Selects the output emission status verification" 500
    cb_balloonHelp $symbolicName(ReduceButton) \
            "Selects the FSM minimization verification" 500
    
}


proc SetKernelBalloonHelp { w } {

    cb_balloonHelp $w.frame1.button6 "Dismiss the result window" 500
    cb_balloonHelp $w.frame1.button7 "Abort the computation" 500
    
}

proc SetReduceBalloonHelp {} {
    global symbolicName

    set w .reduce
    SetKernelBalloonHelp $w
    cb_balloonHelp $w$symbolicName(DrawAutomaton) \
            "Calls Atg to draw the generated automaton" 500
}

proc SetCheckOutputBalloonHelp {} {
    set w .checkoutput

    SetKernelBalloonHelp $w
}

proc SetHelpBalloonHelp {w} {

    cb_balloonHelp $w.frame2.next "Display next help section" 500
    cb_balloonHelp $w.frame2.previous "Display previous help section" 500
    cb_balloonHelp $w.frame2.dismiss "Dismiss this section window" 500
}


