Skip to content
Snippets Groups Projects
Select Git revision
  • 6ab5bc536075247b545a04535d43dd1860851f27
  • master default protected
  • exec_auto_adjust_trace
  • let_variables
  • v1.4.1
  • v1.4.0
  • v1.3.0
  • v1.2.0
  • v1.1.0
  • v1.0.0
10 results

LoadFileCommand.java

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    ShowCommand.java 5.58 KiB
    package de.prob2.jupyter.commands;
    
    import java.io.File;
    import java.nio.file.Path;
    import java.util.HashMap;
    import java.util.List;
    import java.util.Map;
    
    import com.google.inject.Inject;
    import com.google.inject.Provider;
    
    import de.prob.animator.command.GetAnimationMatrixForStateCommand;
    import de.prob.animator.command.GetImagesForMachineCommand;
    import de.prob.animator.command.GetPreferenceCommand;
    import de.prob.animator.domainobjects.AnimationMatrixEntry;
    import de.prob.statespace.AnimationSelector;
    import de.prob.statespace.Trace;
    import de.prob2.jupyter.Command;
    import de.prob2.jupyter.ParameterCompleters;
    import de.prob2.jupyter.ParameterInspectors;
    import de.prob2.jupyter.Parameters;
    import de.prob2.jupyter.ParsedArguments;
    import de.prob2.jupyter.ProBKernel;
    import de.prob2.jupyter.UserErrorException;
    
    import io.github.spencerpark.jupyter.kernel.display.DisplayData;
    
    import org.jetbrains.annotations.NotNull;
    
    public final class ShowCommand implements Command {
    	private final @NotNull AnimationSelector animationSelector;
    	private final @NotNull Provider<ProBKernel> proBKernelProvider;
    	
    	@Inject
    	private ShowCommand(final @NotNull AnimationSelector animationSelector, final @NotNull Provider<ProBKernel> proBKernelProvider) {
    		super();
    		
    		this.animationSelector = animationSelector;
    		this.proBKernelProvider = proBKernelProvider;
    	}
    	
    	@Override
    	public @NotNull String getName() {
    		return ":show";
    	}
    	
    	@Override
    	public @NotNull Parameters getParameters() {
    		return Parameters.NONE;
    	}
    	
    	@Override
    	public @NotNull String getSyntax() {
    		return ":show";
    	}
    	
    	@Override
    	public @NotNull String getShortHelp() {
    		return "Show the machine's animation function visualisation for the current state.";
    	}
    	
    	@Override
    	public @NotNull String getHelpBody() {
    		return "The visualisation is static, any defined right-click options cannot be viewed or used.";
    	}
    	
    	@Override
    	public @NotNull DisplayData run(final @NotNull ParsedArguments args) {
    		final Trace trace = this.animationSelector.getCurrentTrace();
    		
    		if (!trace.getCurrentState().isInitialised()) {
    			throw new UserErrorException("Machine is not initialised, cannot show animation function visualisation");
    		}
    		
    		final GetImagesForMachineCommand cmdImages = new GetImagesForMachineCommand();
    		final GetAnimationMatrixForStateCommand cmdMatrix = new GetAnimationMatrixForStateCommand(trace.getCurrentState());
    		final GetPreferenceCommand cmdImagePadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_PADDING");
    		final GetPreferenceCommand cmdStringPadding = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_STRING_PADDING");
    		final GetPreferenceCommand cmdFontName = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_NAME");
    		final GetPreferenceCommand cmdFontSize = new GetPreferenceCommand("TK_CUSTOM_STATE_VIEW_FONT_SIZE");
    		trace.getStateSpace().execute(
    			cmdImages,
    			cmdMatrix,
    			cmdImagePadding,
    			cmdStringPadding,
    			cmdFontName,
    			cmdFontSize
    		);
    		
    		if (cmdMatrix.getMatrix() == null) {
    			throw new UserErrorException("No animation function visualisation available");
    		}
    		
    		final Path machineDirectory = this.proBKernelProvider.get().getCurrentMachineDirectory();
    		final Map<Integer, String> images = new HashMap<>(cmdImages.getImages());
    		// Animation image paths are relative to the machine directory, which may not be the same as the kernel's working directory.
    		images.replaceAll((k, v) -> machineDirectory.resolve(v).toString());
    		
    		final int imagePadding = Integer.parseInt(cmdImagePadding.getValue());
    		final int stringPadding = Integer.parseInt(cmdStringPadding.getValue());
    		final String fontName = cmdFontName.getValue();
    		final int fontSize = Integer.parseInt(cmdFontSize.getValue());
    		
    		final StringBuilder tableBuilder = new StringBuilder("<table style=\"font-family:");
    		if (!fontName.isEmpty()) {
    			tableBuilder.append('"');
    			tableBuilder.append(fontName);
    			tableBuilder.append("\" ");
    		}
    		tableBuilder.append("monospace");
    		if (fontSize != 0) {
    			tableBuilder.append(";font-size:");
    			tableBuilder.append(fontSize);
    			tableBuilder.append("px");
    		}
    		tableBuilder.append("\"><tbody>");
    		for (final List<AnimationMatrixEntry> row : cmdMatrix.getMatrix()) {
    			tableBuilder.append("\n<tr>");
    			for (final AnimationMatrixEntry entry : row) {
    				final int padding;
    				final String contents;
    				if (entry == null) {
    					padding = 0;
    					contents = "";
    				} else if (entry instanceof AnimationMatrixEntry.Image) {
    					final AnimationMatrixEntry.Image imageEntry = (AnimationMatrixEntry.Image)entry;
    					padding = imagePadding;
    					contents = String.format(
    						"<img alt=\"%d\" src=\"%s\"/>",
    						imageEntry.getImageNumber(),
    						images.get(imageEntry.getImageNumber()).replace(File.separator, "/")
    					);
    				} else if (entry instanceof AnimationMatrixEntry.Text) {
    					padding = stringPadding;
    					contents = ((AnimationMatrixEntry.Text)entry).getText();
    				} else {
    					throw new AssertionError("Unhandled animation matrix entry type: " + entry.getClass());
    				}
    				tableBuilder.append("\n<td style=\"padding:");
    				tableBuilder.append(padding);
    				tableBuilder.append("px\">");
    				tableBuilder.append(contents);
    				tableBuilder.append("</td>");
    			}
    			tableBuilder.append("\n</tr>");
    		}
    		tableBuilder.append("\n</tbody></table>");
    		
    		final DisplayData result = new DisplayData("<Animation function visualisation>");
    		result.putMarkdown(tableBuilder.toString());
    		return result;
    	}
    	
    	@Override
    	public @NotNull ParameterInspectors getParameterInspectors() {
    		return ParameterInspectors.NONE;
    	}
    	
    	@Override
    	public @NotNull ParameterCompleters getParameterCompleters() {
    		return ParameterCompleters.NONE;
    	}
    }