Skip to content
Snippets Groups Projects
Select Git revision
  • e1266bcdfd64a9ff6cf05220686a9a58d71e9d1d
  • 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

LoadCellCommand.java

Blame
  • user avatar
    dgelessus authored
    This way all information about a command is in a single place.
    The ProBKernel class now only needs to contain a list of all commands
    that exist, and all other information is obtained from the command
    objects.
    e1266bcd
    History
    Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    LoadCellCommand.java 3.79 KiB
    package de.prob2.jupyter.commands;
    
    import java.nio.file.Paths;
    import java.util.List;
    import java.util.Map;
    
    import com.google.inject.Inject;
    import com.google.inject.Provider;
    
    import de.prob.scripting.ClassicalBFactory;
    import de.prob.statespace.AnimationSelector;
    import de.prob.statespace.Trace;
    import de.prob2.jupyter.ProBKernel;
    import de.prob2.jupyter.UserErrorException;
    
    import io.github.spencerpark.jupyter.kernel.ReplacementOptions;
    import io.github.spencerpark.jupyter.kernel.display.DisplayData;
    
    import org.jetbrains.annotations.NotNull;
    import org.jetbrains.annotations.Nullable;
    
    public final class LoadCellCommand implements Command {
    	private final @NotNull ClassicalBFactory classicalBFactory;
    	private final @NotNull AnimationSelector animationSelector;
    	private final @NotNull Provider<ProBKernel> proBKernelProvider;
    	
    	@Inject
    	private LoadCellCommand(
    		final @NotNull ClassicalBFactory classicalBFactory,
    		final @NotNull AnimationSelector animationSelector,
    		final @NotNull Provider<ProBKernel> proBKernelProvider
    	) {
    		super();
    		
    		this.classicalBFactory = classicalBFactory;
    		this.animationSelector = animationSelector;
    		this.proBKernelProvider = proBKernelProvider;
    	}
    	
    	@Override
    	public @NotNull String getName() {
    		return "::load";
    	}
    	
    	@Override
    	public @NotNull String getSyntax() {
    		return "::load [PREF=VALUE ...]\nMACHINE\n...\nEND";
    	}
    	
    	@Override
    	public @NotNull String getShortHelp() {
    		return "Load the machine source code given in the cell body.";
    	}
    	
    	@Override
    	public @NotNull String getHelpBody() {
    		return "There must be a newline between the `::load` command name and the machine code.\n\n"
    			+ "Any number of preference assignments may be included after `::load` (only on the first line). Preferences can also be changed on a loaded machine using the `:pref` command, however certain preferences do not take full effect when set using `:pref` and must be set when the machine is loaded.";
    	}
    	
    	@Override
    	public @NotNull DisplayData run(final @NotNull String argString) {
    		final String[] split = argString.split("\n", 2);
    		if (split.length != 2) {
    			throw new UserErrorException("Missing command body");
    		}
    		final String prefsString = split[0];
    		final String body = split[1];
    		final List<String> args = CommandUtils.splitArgs(prefsString);
    		final Map<String, String> preferences = CommandUtils.parsePreferences(args);
    		
    		this.animationSelector.changeCurrentAnimation(new Trace(CommandUtils.withSourceCode(body, () ->
    			this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences)
    		)));
    		this.proBKernelProvider.get().setCurrentMachineDirectory(Paths.get(""));
    		return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent());
    	}
    	
    	@Override
    	public @Nullable DisplayData inspect(final @NotNull String argString, final int at) {
    		final int newlinePos = argString.indexOf('\n');
    		if (newlinePos == -1 || at < newlinePos) {
    			// Cursor is on the first line, provide preference inspections.
    			return CommandUtils.inspectInPreferences(this.animationSelector.getCurrentTrace(), argString, at);
    		} else {
    			// Cursor is in the body, provide B inspections.
    			return CommandUtils.inspectInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
    		}
    	}
    	
    	@Override
    	public @Nullable ReplacementOptions complete(final @NotNull String argString, final int at) {
    		final int newlinePos = argString.indexOf('\n');
    		if (newlinePos == -1 || at < newlinePos) {
    			// Cursor is on the first line, provide preference name completions.
    			return CommandUtils.completeInPreferences(this.animationSelector.getCurrentTrace(), argString, at);
    		} else {
    			// Cursor is in the body, provide B completions.
    			return CommandUtils.completeInBExpression(this.animationSelector.getCurrentTrace(), argString, at);
    		}
    	}
    }