/**
 * Removes the item from the view, performing necessary
 * cleanup.
 * 
 * @param item
 */
private void removeItem(ExpandItem item)
{
    // remove the source viewer's control from the
    // font listener since it no longer needs to be
    // notified of font changes.
    fontListener.removeControl(((SourceViewer) viewers.get(item)).getControl());

    // retrieve the id for the item
    // the id is stored in the item's data, which should be a marker,
    // as set in the updateItem method
    final Object data = item.getData(KEY);
    items.remove(Integer.parseInt(data.toString()));

    item.getControl().dispose();
    item.dispose();
}
 

public ObligationsView()
{
    items = new HashMap<Integer, ExpandItem>();
    viewers = new HashMap<ExpandItem, SourceViewer>();
    fontListener = new FontPreferenceChangeListener(null, JFaceResources.TEXT_FONT);
    JFaceResources.getFontRegistry().addListener(fontListener);
}
 

/**
 * Fill data
 * @param specLoaded
 */
private void fillData(Spec specLoaded)
{
    if (specLoaded == null)
    {
        hide();
        return;
    } else
    {

        // retrieve the markers associated with the loaded spec
        IMarker[] markers = TLAMarkerHelper.getProblemMarkers(specLoaded.getProject(), null);

        if (markers == null || markers.length == 0)
        {
            hide();
        }

        // sort the markers
        List<IMarker> markersList = new ArrayList<IMarker>(Arrays.asList(markers));
        Collections.sort(markersList, new MarkerComparator());

        // Bug fix: 2 June 2010.  It takes forever if
        // there are a large number of markers, which
        // can easily happen if you remove a definition
        // that's used hundreds of times.
        int iterations = Math.min(markers.length, 20);
        for (int j = 0; j < iterations; j++)
        {
            final IMarker problem = markersList.get(j);

            // listener
            Listener listener = new Listener() {
                // goto marker on click
                public void handleEvent(Event event)
                {
                    TLAMarkerHelper.gotoMarker(problem, ((event.stateMask & SWT.MOD1) != 0));
                }
            };

            // contents of the item
            Composite problemItem = new Composite(bar, SWT.LINE_SOLID);
            problemItem.setLayout(new RowLayout(SWT.VERTICAL));
            problemItem.addListener(SWT.MouseDown, listener);

            String[] lines = problem.getAttribute(IMarker.MESSAGE, "").split("\n");
            for (int i = 0; i < lines.length; i++)
            {
                StyledText styledText = new StyledText(problemItem, SWT.INHERIT_DEFAULT);
                styledText.setEditable(false);
                styledText.setCursor(styledText.getDisplay().getSystemCursor(SWT.CURSOR_HAND));
                styledText.setText(lines[i]);
                styledText.addListener(SWT.MouseDown, listener);

                if (isErrorLine(lines[i], problem))
                {
                    StyleRange range = new StyleRange();
                    range.underline = true;
                    range.foreground = styledText.getDisplay().getSystemColor(SWT.COLOR_RED);
                    range.start = 0;
                    range.length = lines[i].length();
                    styledText.setStyleRange(range);
                }
            }

            ExpandItem item = new ExpandItem(bar, SWT.NONE, 0);
            item.setExpanded(true);
            
            String markerType = TLAMarkerHelper.getType(problem);
            item.setText(AdapterFactory.getMarkerTypeAsText(markerType) + " " + AdapterFactory.getSeverityAsText(problem.getAttribute(IMarker.SEVERITY,
                    IMarker.SEVERITY_ERROR)));
            item.setHeight(problemItem.computeSize(SWT.DEFAULT, SWT.DEFAULT).y);
            item.setControl(problemItem);
            item.addListener(SWT.MouseDown, listener);
        }
    }
    return ;
}
 

/**
  * Used to refresh the obligation view if it is currently open. If the view
  * is not currently open, this method does nothing. If the view is currently open,
  * this takes the following two steps:
  * 
  * 1.) Removes all items from the expand bar for this view.
  * 
  * 2.) Retrieve all obligation statuses by calling {@link ProverHelper#getObligationStatuses()}.
  *     Fills the view with information from these statuses.
  * 
  * 3.) If there are no interesting obligations in the view after steps 1 and 2, then
  * the view is hidden.
  */
 public static void refreshObligationView()
 {
 	UIHelper.runUIAsync(new Runnable() {
/* (non-Javadoc)
 * @see java.lang.Runnable#run()
 */
public void run() {

       final ObligationsView oblView = (ObligationsView) UIHelper.findView(VIEW_ID);
       if (oblView != null)
       {

           /*
            * Remove all items in the bar.
            * 
            * For each item:
            * 1.) Dispose the item's control.
            * 2.) Dispose the item.
            * 
            * After disposing of all items, clear
            * the map of ids to items.
            */
           ExpandItem[] expandItems = oblView.bar.getItems();
           for (int i = 0; i < expandItems.length; i++)
           {
               oblView.removeItem(expandItems[i]);
           }

           /*
            * Fill the obligation view with markers from the current spec.
            * If the obligations view is empty after doing this (there are
            * no interesting obligations) then hide the view.
            */
           oblView.fillFromCurrentSpec();

           if (oblView.isEmpty())
           {
               UIHelper.getActivePage().hideView(oblView);
           }

       }
}
 	});
 }
 

public static void relayoutExpandBar(ExpandBar expandBar, boolean relayoutParents)
{
	Composite c = expandBar;
	int tempMaxControlX = 0;
	
	logger.debug( "----- relayoutExpandBar (relayoutParents: " + relayoutParents + " expandBar: " + expandBar + " -----" );
	
	do
	{
		logger.debug( "c: " + c.getClass() + " c.getParent(): " + c.getParent().getClass() );
		
		if ( c instanceof ExpandBar )
		{
			ExpandBar eb = (ExpandBar) c;
			
			logger.debug( "ExpandBar.getSize(): " + eb.getSize() );
			
			for ( ExpandItem expandItem : eb.getItems() )
			{
				logger.debug( "expandItem: " + expandItem + " text: " + expandItem.getText() + " control: " + expandItem.getControl() + " controlLocation: " + expandItem.getControl().getLocation());					
				logger.debug( "before pack(): expandItem.getControl().getSize(): " + expandItem.getControl().getSize() );

				expandItem.getControl().pack();
				
				if ( expandItem.getControl().getSize().x > tempMaxControlX )
				{
					tempMaxControlX = expandItem.getControl().getSize().x;
				}

				logger.debug( "before: expandItem.getHeight(): " + expandItem.getHeight() + " expandItem.getControl().getSize(): " + expandItem.getControl().getSize() );

				expandItem.setHeight( expandItem.getControl().computeSize( eb.getSize().x, SWT.DEFAULT, true ).y );
			}

			// -- Need to set ExpandBar's GridData.widthHint to the width of the widest control within it -- 
			GridData tempGridData2 = (GridData) expandBar.getLayoutData();
			tempGridData2.widthHint = tempMaxControlX;
			// do not set height as ExpandBar handles this tempGridData2.heightHint = expandBar.getSize().y;
			expandBar.setLayoutData( tempGridData2 );
			
				
			if ( relayoutParents )
			{
				Control p = c.getParent();
				
				if ( p instanceof ScrolledComposite )
				{
					ScrolledComposite scrolledComposite = (ScrolledComposite) p;
					if ( scrolledComposite.getExpandHorizontal() || scrolledComposite.getExpandVertical() )
					{
						scrolledComposite.setMinSize( scrolledComposite.getContent().computeSize( SWT.DEFAULT, SWT.DEFAULT, true ) );
					}
					else
					{
						scrolledComposite.getContent().pack( true );
					}
				}

				if ( p instanceof Composite )
				{
					Composite composite = (Composite) p;
					composite.layout();
				}
			}
			else
			{
				// -- this (or relayoutParents=true) is needed (otherwise ExampleStrategyPanelTests2.xml with 2 "columns" of StrategyPanels may not draw all of the ExpandBars initially) --
				expandBar.getParent().layout();
			}

		}
		c = c.getParent();
	}
	while ( c != null && c.getParent() != null && !( c instanceof ScrolledComposite ) );


	// -- Needed to ensure that strategy panel is expanded vertically as panels go from collapsed to expanded
	expandBar.getShell().layout();
	expandBar.getShell().pack();
}