Commit 7dc2451f authored by Kisslinger's avatar Kisslinger
Browse files

formal specifications are now added to the report

fixed bug with images introduced by release review
refs 290
parent 0f943824
......@@ -18,6 +18,7 @@ $Id$
package org.fortiss.af3.mira.ui.action;
import static org.conqat.lib.commons.filesystem.FileSystemUtils.copyFile;
import static org.fortiss.af3.mira.ui.utils.ImageUtils.getImageFile;
import java.io.File;
import java.io.IOException;
......@@ -36,7 +37,7 @@ import org.fortiss.tooling.kernel.ui.extension.base.EObjectActionBase;
* @author kisslinger
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 1AB2CEC552D9C1EB5166787B81AA8265
* @ConQAT.Rating YELLOW Hash: 048228FEB1388C66C2A0D1357BFCDF66
*/
public class ExportImagesAction extends EObjectActionBase<EObject> {
......@@ -74,8 +75,7 @@ public class ExportImagesAction extends EObjectActionBase<EObject> {
private void exportImages(IImageContainer element) {
for(ImageItem imageItem : element.getImages()) {
try {
copyFile(new File(imageItem.getAbsolutePath()),
new File(imageFolder, imageItem.getPath()));
copyFile(getImageFile(imageItem), new File(imageFolder, imageItem.getPath()));
} catch(IOException e) {
e.printStackTrace();
}
......
......@@ -44,7 +44,7 @@ import org.fortiss.tooling.kernel.ui.extension.base.EObjectActionBase;
* @author uden
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 4DD3703FA29DECFE96392AD812367038
* @ConQAT.Rating YELLOW Hash: 4C66BE00DF53EE06880B83E5BDFBF2A1
*/
public class ExportReportAction extends EObjectActionBase<EObject> {
......@@ -52,7 +52,7 @@ public class ExportReportAction extends EObjectActionBase<EObject> {
private Shell shell;
/**
* Constructor
* Constructor.
*
* @param target
* the object to be exported
......@@ -106,7 +106,7 @@ public class ExportReportAction extends EObjectActionBase<EObject> {
}
new ExportImagesAction(getTarget(), htmfile.getParentFile()).run();
new ExportMSCImagesAction(getTarget(), htmfile.getParentFile()).run();
new ExportSpecificationImagesAction(getTarget(), htmfile.getParentFile()).run();
try {
new ExportReportCommand(getTarget(), getTemplatePath(getTarget()), htmfile, isWindows
......
......@@ -18,35 +18,45 @@ $Id$
package org.fortiss.af3.mira.ui.action;
import static org.fortiss.af3.mira.ui.utils.ImageUtils.exportEditorContentAsImage;
import static org.fortiss.af3.mira.utils.MiraUtils.getProjectName;
import static org.fortiss.af3.mode.utils.ModeAutomatonUtils.getModeAutomaton;
import static org.fortiss.af3.state.utils.StateAutomatonUtils.getStateAutomaton;
import static org.fortiss.af3.state.utils.StateAutomatonUtils.hasStateAutomaton;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
import java.io.File;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.ecore.EObject;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.mira.model.Analysis;
import org.fortiss.af3.mira.model.usecase.UseCase;
import org.fortiss.af3.mira.model.Requirement;
import org.fortiss.af3.mira.model.functional.FormalSpecification;
import org.fortiss.af3.mode.model.Mode;
import org.fortiss.af3.msc.model.MSCSpecification;
import org.fortiss.af3.state.model.State;
import org.fortiss.tooling.base.ui.editor.DiagramEditorBase;
import org.fortiss.tooling.kernel.model.IIdLabeled;
import org.fortiss.tooling.kernel.ui.extension.IModelEditor;
import org.fortiss.tooling.kernel.ui.extension.base.EObjectActionBase;
import org.fortiss.tooling.kernel.ui.service.IModelEditorBindingService;
/**
* Action to export the MSCs contained by an {@link UseCase} or an {@link Analysis} (all MSCs
* contained by the containedElements) as images to the filesystem
* Action to export the MSCs and formal specifications contained by an {@link Requirement} or an
* {@link Analysis} (all MSCs and formal specifications contained by the containedElements) as
* images to the filesystem
*
* @author kisslinger
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 09437D0791B119E20168B6439EC1212E
* @ConQAT.Rating YELLOW Hash: DA83B80EFA65F11B9BB97E1D0EE32313
*/
public class ExportMSCImagesAction extends EObjectActionBase<EObject> {
public class ExportSpecificationImagesAction extends EObjectActionBase<EObject> {
/** folder which should contain the images in the end */
private final File imageFolder;
/** Constructor. */
public ExportMSCImagesAction(EObject target, File targetPath) {
public ExportSpecificationImagesAction(EObject target, File targetPath) {
super(target, "Export images");
imageFolder = new File(targetPath, "images");
......@@ -57,12 +67,12 @@ public class ExportMSCImagesAction extends EObjectActionBase<EObject> {
/** {@inheritDoc} */
@Override
public void run() {
if(getTarget() instanceof UseCase) {
exportMSCImages((UseCase)getTarget());
if(getTarget() instanceof Requirement) {
exportSpecificationImages((Requirement)getTarget());
}
if(getTarget() instanceof Analysis) {
for(UseCase uc : ((Analysis)getTarget()).getUseCase())
exportMSCImages(uc);
for(Requirement req : ((Analysis)getTarget()).getRequirementsList())
exportSpecificationImages(req);
}
// if no images have been copied and the image folder is empty, delete
......@@ -72,27 +82,93 @@ public class ExportMSCImagesAction extends EObjectActionBase<EObject> {
}
/**
* Exports the MSC images of one {@link UseCase}
* Exports the MSC and formal specification images of one {@link Requirement}
*/
private void exportMSCImages(UseCase uc) {
private void exportSpecificationImages(Requirement req) {
IModelEditor<EObject> editorOpenedBefore =
IModelEditorBindingService.INSTANCE.getActiveEditor();
EList<MSCSpecification> mscSpecs =
pickInstanceOf(MSCSpecification.class, uc.getContainedElementsList());
// export MSCs
EList<MSCSpecification> mscSpecs =
pickInstanceOf(MSCSpecification.class, req.getContainedElementsList());
for(MSCSpecification mscSpec : mscSpecs) {
// the specification must be opened in an editor in order to export the graphical
// content
IModelEditorBindingService.INSTANCE.openInEditor(mscSpec);
exportEditorContentAsImage(
(DiagramEditorBase<EObject>)IModelEditorBindingService.INSTANCE
.getActiveEditor(),
new File(imageFolder, "msc" + mscSpec.getId()));
exportObjectAsImage(mscSpec);
}
// export formal specifications
EList<FormalSpecification> formalSpecs =
pickInstanceOf(FormalSpecification.class, req.getContainedElementsList());
for(FormalSpecification formalSpec : formalSpecs) {
handleExportComponent(formalSpec.getTopComponent());
}
// workaround to return to the editor which as opened before
// workaround to return to the editor which was opened before
if(editorOpenedBefore != null)
IModelEditorBindingService.INSTANCE.openInEditor(editorOpenedBefore.getEditedObject());
}
/**
* Handles the export for a component (including sub-components and specifications)
*/
private void handleExportComponent(Component component) {
if(hasStateAutomaton(component)) {
handleExportState(getStateAutomaton(component).getRootState());
} else if(getModeAutomaton(component) != null) {
handleExportMode(getModeAutomaton(component).getRootMode());
} else if((!component.getSubComponents().isEmpty()) ||
!(component.getContainer() instanceof Component)) {
// the component view must be exported if the component contains sub-components or if it
// is the top-component
exportObjectAsImage(component);
for(Component subComponent : component.getSubComponents()) {
handleExportComponent(subComponent);
}
}
}
/**
* Handles the export for a state of a state automaton (including sub-states)
*/
private void handleExportState(State state) {
if(!state.getSubStates().isEmpty()) {
exportObjectAsImage(state);
for(State subState : state.getSubStates()) {
handleExportState(subState);
}
}
}
/**
* Handles the export for a mode of a mode automaton (including sub-modes and sub-components)
*/
private void handleExportMode(Mode mode) {
if(!mode.getSubModes().isEmpty()) {
exportObjectAsImage(mode);
for(Mode subMode : mode.getSubModes()) {
handleExportMode(subMode);
}
}
if(mode.getModeComponentStructureSpecification() != null) {
handleExportComponent(mode.getModeComponentStructureSpecification().getTopComponent());
}
}
/**
* Exports the specified object (must be something which can be opened in an graphical editor)
* as image.
*/
private void exportObjectAsImage(IIdLabeled object) {
// the specification must be opened in an editor in order to export the graphical
// content
IModelEditorBindingService.INSTANCE.openInEditor(object);
exportEditorContentAsImage(
(DiagramEditorBase<EObject>)IModelEditorBindingService.INSTANCE.getActiveEditor(),
new File(imageFolder, getProjectName(object) + "-object" + object.getId()));
}
}
......@@ -19,6 +19,7 @@ package org.fortiss.af3.mira.ui.editor.glossary;
import static java.util.Collections.sort;
import static org.fortiss.af3.mira.ui.utils.GlossaryUtils.match;
import static org.fortiss.af3.mira.ui.utils.ImageUtils.getImageFile;
import java.util.ArrayList;
import java.util.List;
......@@ -42,7 +43,7 @@ import org.fortiss.af3.mira.model.glossary.WordElement;
* @author kisslinger
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 936E2569DB8E700B518C4096ABA138F4
* @ConQAT.Rating YELLOW Hash: D61511EBBA5D6CDBD03AFCDD10C73DD3
*/
public class GlossaryTextHover extends DefaultTextHover implements ITextHoverExtension2 {
......@@ -82,7 +83,8 @@ public class GlossaryTextHover extends DefaultTextHover implements ITextHoverExt
hoverText
.append("<div style='width:150px; font-size:80%; text-align:center;float:right;margin-left:15px;margin-bottom:10px'>" +
"<div><img src='" +
resultListEntry.getEntry().getImages(0).getAbsolutePath() +
getImageFile(resultListEntry.getEntry().getImages(0))
.getAbsolutePath() +
"' width='150' /></div>" +
(resultListEntry.getEntry().getImages(0).getName() != null
? resultListEntry.getEntry().getImages(0).getName()
......
......@@ -19,6 +19,7 @@ package org.fortiss.af3.mira.ui.editor.images;
import static java.awt.Desktop.getDesktop;
import static org.eclipse.jface.layout.GridDataFactory.swtDefaults;
import static org.fortiss.af3.mira.ui.utils.ImageUtils.getImageFile;
import static org.fortiss.af3.project.ui.utils.NewProjectUtils.getDefaultGeneralProjectPath;
import static org.fortiss.tooling.kernel.model.FortissToolingKernelPackage.Literals.INAMED_ELEMENT__NAME;
import static org.fortiss.tooling.kernel.ui.util.DataBindingUtils.bind;
......@@ -55,7 +56,7 @@ import org.fortiss.tooling.kernel.service.ICommandStackService;
* @author kisslinger
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 5404B031A5706C37BAD3737D7A1E0CCB
* @ConQAT.Rating YELLOW Hash: A70D69FB0CFE8FB1A9EE3115B91526B6
*/
public class ImageBox {
/** composite on which all elements should created */
......@@ -105,8 +106,7 @@ public class ImageBox {
public boolean createBox() {
// load the image
try {
File imageFile = new File(imageItem.getAbsolutePath());
image = new Image(composite.getDisplay(), imageFile.getAbsolutePath());
image = new Image(composite.getDisplay(), getImageFile(imageItem).getAbsolutePath());
} catch(Exception e) {
return false;
}
......
......@@ -17,6 +17,9 @@ $Id$
+--------------------------------------------------------------------------*/
package org.fortiss.af3.mira.ui.utils;
import static org.fortiss.af3.project.ui.utils.NewProjectUtils.getDefaultGeneralProjectPath;
import static org.fortiss.tooling.base.ui.editpart.ExtendedLayerRootEditPart.LABEL_LAYER;
import java.io.File;
import org.eclipse.draw2d.Graphics;
......@@ -33,6 +36,7 @@ import org.eclipse.swt.graphics.Image;
import org.eclipse.swt.graphics.ImageData;
import org.eclipse.swt.graphics.ImageLoader;
import org.eclipse.swt.widgets.Display;
import org.fortiss.af3.mira.model.ImageItem;
import org.fortiss.tooling.base.ui.editor.DiagramEditorBase;
import org.fortiss.tooling.base.ui.editpart.ExtendedLayerRootEditPart;
......@@ -42,7 +46,7 @@ import org.fortiss.tooling.base.ui.editpart.ExtendedLayerRootEditPart;
* @author kisslinger
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 8F1FE3F2372B57F28FDB869C664ACD55
* @ConQAT.Rating YELLOW Hash: 2C261DF5D58B1901C37269B2A5B46116
*/
public class ImageUtils {
......@@ -57,47 +61,91 @@ public class ImageUtils {
.get(LayerManager.ID);
IFigure rootFigure = ((LayerManager)rootEditPart).getLayer(LayerConstants.PRINTABLE_LAYERS);
Rectangle rootFigureBounds = rootFigure.getBounds();
// the necessary size of the resulting image is calculated here from the positions and
// bounds of the image elements, because the rootFigureBounds (and the bounds of edit part
// bounds of the image elements, because the bounds of the root figure (and the bounds of
// edit part
// of the top-level model element) are sometimes too high (probably a GEF bug?)
int minWidth = 1;
int minHeight = 1;
int maxLeft = rootFigureBounds.width;
int maxTop = rootFigureBounds.height;
for(Object o : editor.getViewer().getEditPartRegistry().values())
// the Rectangle clippingBounds holds four values which describe which part of the original
// image is needed.
// The x&y values define top-left point and the width&height values define the
// right-bottom point of the area
Rectangle clippingBounds =
new Rectangle(rootFigure.getBounds().width, rootFigure.getBounds().height, 0, 0);
for(Object o : editor.getViewer().getEditPartRegistry().values()) {
if(o instanceof AbstractGraphicalEditPart) {
AbstractGraphicalEditPart editPart = (AbstractGraphicalEditPart)o;
Rectangle partRec = editPart.getFigure().getBounds();
// it is assumed that the first (and only) children of the rootEditPart is the edit
// part of the top-level model element (e.g. the MSCDiagram)
// this assumption is true at least for the MSCs, but it should be checked if the
// code is used somewhere else
if(!editPart.equals(rootEditPart) &&
!editPart.equals(rootEditPart.getChildren().get(0))) {
if(partRec.x + partRec.width > minWidth)
minWidth = partRec.x + partRec.width;
if(partRec.y + partRec.height > minHeight)
minHeight = partRec.y + partRec.height;
if(partRec.x < maxLeft)
maxLeft = partRec.x;
if(partRec.y < maxTop)
maxTop = partRec.y;
adjustClippingBounds(clippingBounds, partRec);
}
}
}
Image image = new Image(Display.getDefault(), minWidth - maxLeft, minHeight - maxTop);
GC gc = new GC(image);
Graphics graphics = new SWTGraphics(gc);
graphics.translate(-maxLeft, -maxTop);
rootFigure.paint(graphics);
// also check the labels, else they can be cut of (because they are not contained in the
// editPartRegistry)
for(Object o : rootEditPart.getLayer(LABEL_LAYER).getChildren()) {
if(o instanceof IFigure) {
IFigure labelFigure = (IFigure)o;
adjustClippingBounds(clippingBounds, labelFigure.getBounds());
}
}
Image image;
GC gc = null;
if(clippingBounds.width - clippingBounds.x <= 0 ||
clippingBounds.height - clippingBounds.y <= 0) {
// if there are no elements to paint, just give out a small empty image
image = new Image(Display.getDefault(), 10, 10);
} else {
image =
new Image(Display.getDefault(), clippingBounds.width - clippingBounds.x,
clippingBounds.height - clippingBounds.y);
gc = new GC(image);
Graphics graphics = new SWTGraphics(gc);
graphics.translate(-clippingBounds.x, -clippingBounds.y);
rootFigure.paint(graphics);
}
ImageLoader imgLoader = new ImageLoader();
imgLoader.data = new ImageData[] {image.getImageData()};
imgLoader.save(destination.getAbsolutePath(), SWT.IMAGE_JPEG);
gc.dispose();
if(gc != null)
gc.dispose();
image.dispose();
}
/**
* Adjusts the clippingBounds if necessary so that the partRec rectangle is contained
*/
private static void adjustClippingBounds(Rectangle clippingBounds, Rectangle partRec) {
if(partRec.x + partRec.width > clippingBounds.width)
clippingBounds.width = partRec.x + partRec.width;
if(partRec.y + partRec.height > clippingBounds.height)
clippingBounds.height = partRec.y + partRec.height;
if(partRec.x < clippingBounds.x)
clippingBounds.x = partRec.x;
if(partRec.y < clippingBounds.y)
clippingBounds.y = partRec.y;
}
/**
* Returns the file with the absolute path for the image item. For the image only its name
* is saved because the location is always the image folder in the AF3
* Project directory. Like this the data can easily exchanged and the
* system-dependent absolute path is only generated if needed.
*
* @param item
* item for which the path should be returned
* @return the absolute path
*/
public static File getImageFile(ImageItem item) {
File f1 = new File(getDefaultGeneralProjectPath(), "images");
return new File(f1, item.getPath());
}
}
......@@ -37,7 +37,9 @@ Export-Package: org.fortiss.af3.mira,
org.fortiss.af3.mira.verification,
test.org.fortiss.af3.mira
Require-Bundle: org.fortiss.af3.component;bundle-version="2.2.0";visibility:=reexport,
org.fortiss.af3.msc;bundle-version="2.2.0";visibility:=reexport
org.fortiss.af3.msc;bundle-version="2.2.0";visibility:=reexport,
org.fortiss.af3.state;bundle-version="2.2.0";visibility:=reexport,
org.fortiss.af3.mode;bundle-version="2.2.0";visibility:=reexport
Bundle-ActivationPolicy: lazy
Bundle-NativeCode: lib/com4j-x86.dll; lib/com4j-amd64.dll
Bundle-Activator: org.fortiss.af3.mira.AF3MiraActivator
......@@ -118,11 +118,6 @@
</eOperations>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="ImageItem" eSuperTypes="platform:/plugin/org.fortiss.tooling.kernel/model/kernel.ecore#//INamedElement">
<eOperations name="getAbsolutePath" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="body" value="return ImageItemStaticImpl.getAbsolutePath(this);"/>
</eAnnotations>
</eOperations>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="path" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="IImageContainer">
......
......@@ -53,7 +53,6 @@
</genClasses>
<genClasses ecoreClass="mira.ecore#//ImageItem">
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute mira.ecore#//ImageItem/path"/>
<genOperations ecoreOperation="mira.ecore#//ImageItem/getAbsolutePath"/>
</genClasses>
<genClasses ecoreClass="mira.ecore#//IImageContainer">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference mira.ecore#//IImageContainer/images"/>
......
/*--------------------------------------------------------------------------+
$Id$
| |
| Copyright 2012 ForTISS GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.mira.model.impl;
import java.io.File;
import org.fortiss.af3.mira.model.ImageItem;
/**
* Static implementation of {@link ImageItem}
*
* @author kisslinger
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 8C60F546E1A0BD2EED6856C1A9B88D71
*/
public class ImageItemStaticImpl {
/**
* Returns the absolute path for the image item. For the image only its name
* is saved because the location is always the image folder in the AF3
* Project directory. Like this the data can easily exchanged and the
* system-dependent absolute path is only generated if needed.
*
* @param item
* item for which the path should be returned
* @return the absolute path
*/
public static String getAbsolutePath(ImageItem item) {
File f1 = new File("AF3-Project-Directory", "images");
return new File(f1, item.getPath()).getAbsolutePath();
}
}
......@@ -18,15 +18,24 @@ $Id$
package org.fortiss.af3.mira.report;
import static org.conqat.lib.commons.string.StringUtils.concat;
import static org.fortiss.af3.component.utils.BehaviorUtils.getCodeSpecification;
import static org.fortiss.af3.expression.utils.ExpressionUtils.formatStatements;
import static org.fortiss.af3.mira.utils.MiraUtils.getProjectName;
import static org.fortiss.af3.mira.utils.MiraUtils.getRequirementShortInfo;
import static org.fortiss.af3.mode.utils.ModeAutomatonUtils.getModeAutomaton;
import static org.fortiss.af3.state.utils.StateAutomatonUtils.getStateAutomaton;
import static org.fortiss.af3.state.utils.StateAutomatonUtils.hasStateAutomaton;
import static org.fortiss.tooling.base.utils.BaseModelElementUtils.getIndex;
import java.util.ArrayList;
import org.eclipse.emf.ecore.EObject;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.mira.model.Analysis;
import org.fortiss.af3.mira.model.ImageItem;
import org.fortiss.af3.mira.model.Requirement;
import org.fortiss.af3.mira.model.RequirementRelation;
import org.fortiss.af3.mira.model.functional.FormalSpecification;
import org.fortiss.af3.mira.model.glossary.Glossary;
import org.fortiss.af3.mira.model.glossary.GlossaryEntry;
import org.fortiss.af3.mira.model.glossary.WordElement;
......@@ -38,8 +47,13 @@ import org.fortiss.af3.mira.model.usecase.UseCase;
import org.fortiss.af3.mira.relation.IRelationHandler;
import org.fortiss.af3.mira.relation.IRelationService;
import org.fortiss.af3.mira.report.template.EvaluationContext;
import org.fortiss.af3.mode.model.Mode;
import org.fortiss.af3.mode.model.ModeAutomaton;
import org.fortiss.af3.msc.model.MSCSpecification;
import org.fortiss.tooling.base.utils.BaseModelElementUtils;
import org.fortiss.af3.state.model.State;
import org.fortiss.af3.state.model.StateAutomaton;
import org.fortiss.tooling.kernel.model.IIdLabeled;
import org.fortiss.tooling.kernel.model.INamedElement;
import org.fortiss.tooling.kernel.utils.EcoreUtils;
/**
......@@ -48,7 +62,7 @@ import org.fortiss.tooling.kernel.utils.EcoreUtils;
* @author mou
* @author $Author$
* @version $Rev$
* @ConQAT.Rating GREEN Hash: 8DCE73A2CE2B30E6E76FD1C902133339
* @ConQAT.Rating YELLOW Hash: 0385CA172E7ABF89F78199D7130EE142
*/
public class ContextFactory {
......@@ -141,6 +155,17 @@ public class ContextFactory {
}
ctx.defineContextList("formalspecs_short");
ctx.defineContextList("formalspecs");
for(FormalSpecification formalSpec : EcoreUtils.pickInstanceOf(FormalSpecification.class,
r.getContainedElementsList())) {
EvaluationContext nestctx = new EvaluationContext();
nestctx.set("name", formalSpec.getName());
ctx.addContext("formalspecs_short", nestctx);
handleTopComponent(formalSpec.getTopComponent(), formalSpec.getName(), ctx,
"formalspecs");