GUI Improvements (#37)

* [macos] Make pkg instead of dmg since High Sierra screwed the javapackager * skip bin/bin_test * Markdown * - Fixing COPY/PASTE in evaluator - Markdown format supported - Table output * - Table output window that shows a Sig’s fields - Improved table output - removed the 0 if the only atom - removed first column name if same as previous line * [editor] Double click after text creates core dump Did not verify against the text length * [editor] Added support for tooltips and navigation - F3 now navigates to a declaration if possible - Tooltips show the type * [extra] Cleanup included docs (need more work) * [computer] Made the computer return an actual object instead of the string The computer was String compute(String expr). However, make a string is quite easy and sometimes it is better to have the actual object. * [lexer] Added support for HEX and BINARY numbers Now can use 0x56 and 0b11101 Also supports _ in numbers to separate digits 0x1000_0000 * [tooltip] If hex or binary numbers are used the tooltip shows the decimal value Also fixes an error that a trial was not removed and now also looks for Pos in facts of a sig for where the cursor is. * [tables] Made the table support nesting - Console now shows nested tables - Table view shows nested tables * [gui] Allow .md files * [tables] Better tables Still not there but making progress. * [macro] Explain/Clause tooltip support * [table support] Diverse table support * - Added a default command when no commands are defined - Made the parser always go through CompUtil, no more direct references to the parser. * [bold] Bold test failed * [markdown] Changes request by Aleksander * Review Aleksander Some files have already started new formatting.
AlloyTools · Mar 25, 2018 · f68241c · f68241c
1 parent 6611ccc
commit f68241c
Show file tree

Hide file tree

Showing 73 changed files with 5,789 additions and 2,439 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,6 +1,8 @@
 .DS_Store
 .gradle/
 generated/
+bin/
+bin_test/
 target/
 enroute.zip
 .metadata

diff --git a/cnf/central.xml b/cnf/central.xml
@@ -9,6 +9,11 @@
 	<packaging>pom</packaging>
 
 	<dependencies>
+		<dependency>
+			<groupId>org.eclipse.jdt</groupId>
+			<artifactId>org.eclipse.jdt.annotation</artifactId>
+			<version>2.1.100</version>
+		</dependency>
 		<dependency>
 			<groupId>org.apache.felix</groupId>
 			<artifactId>org.apache.felix.gogo.shell</artifactId>

diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java
@@ -107,7 +107,7 @@ public final class VizGUI implements ComponentListener {
 	private final JButton		projectionButton, openSettingsButton, closeSettingsButton, magicLayout,
 			loadSettingsButton, saveSettingsButton, saveAsSettingsButton, resetSettingsButton, updateSettingsButton,
 			openEvaluatorButton, closeEvaluatorButton, enumerateButton, vizButton, treeButton,
-			txtButton/* , dotButton, xmlButton */;
+			txtButton, tableButton/* , dotButton, xmlButton */;
 
 	/**
 	 * This list must contain all the display mode buttons (that is, vizButton,
@@ -265,6 +265,7 @@ private enum VisualizerMode {
 		// /** See the XML content. */ XML("xml"),
 		/** See the instance as text. */
 		TEXT("txt"),
+		TABLE("table"),
 		/** See the instance as a tree. */
 		Tree("tree");
 		/**
@@ -335,6 +336,7 @@ public static VisualizerMode get() {
 	 */
 	private boolean					wrap		= false;
 
+
 	/**
 	 * Wraps the calling method into a Runnable whose run() will call the
 	 * calling method with (false) as the only argument.
@@ -353,6 +355,10 @@ private Runner wrapMe() {
 				m = methods[i];
 				break;
 			}
+		if (m == null) {
+			throw new IllegalStateException("Missing method " + name);
+		}
+
 		final Method method = m;
 		return new Runner() {
 			private static final long serialVersionUID = 0;
@@ -391,6 +397,11 @@ private Runner wrapMe(final Object argument) {
 				m = methods[i];
 				break;
 			}
+
+		if (m == null) {
+			throw new IllegalStateException("Missing method " + name);
+		}
+
 		final Method method = m;
 		return new Runner() {
 			private static final long serialVersionUID = 0;
@@ -560,6 +571,8 @@ public void actionPerformed(ActionEvent e) {
 			// "images/24_plaintext.gif", doShowXML());
 			txtButton = makeSolutionButton("Txt", "Show the textual output for the Graph", "images/24_plaintext.gif",
 					doShowTxt());
+			tableButton = makeSolutionButton("Table", "Show the table output for the Graph", "images/24_plaintext.gif",
+					doShowTable());
 			treeButton = makeSolutionButton("Tree", "Show Tree", "images/24_texttree.gif", doShowTree());
 			if (frame != null)
 				addDivider();
@@ -711,6 +724,9 @@ private void updateDisplay() {
 			case TEXT :
 				txtButton.setEnabled(false);
 				break;
+			case TABLE :
+				tableButton.setEnabled(false);
+				break;
 			// case XML: xmlButton.setEnabled(false); break;
 			// case DOT: dotButton.setEnabled(false); break;
 			default :
@@ -760,6 +776,11 @@ public final void focusLost(FocusEvent e) {}
 				content = getTextComponent(textualOutput);
 				break;
 			}
+			case TABLE : {
+				String textualOutput = myState.getOriginalInstance().originalA4.format();
+				content = getTextComponent(textualOutput);
+				break;
+			}
 			// case XML: {
 			// content=getTextComponent(xmlFileName);
 			// break;
@@ -901,10 +922,14 @@ private JComponent getTextComponent(String text) {
 
 			@Override
 			public void setFont(Font font) {
-				ta.setFont(font);
+				super.setFont(font);
 			}
 		};
 		ans.setBorder(new OurBorder(true, false, true, false));
+		String fontName = OurDialog.getProperFontName("Lucida Console", "Monospaced");
+		Font font = new Font(fontName, Font.PLAIN, fontSize);
+		ans.setFont(font);
+		ta.setFont(font);
 		return ans;
 	}
 
@@ -1414,6 +1439,19 @@ public Runner doShowTxt() {
 		return wrapMe();
 	}
 
+	/**
+	 * This method changes the display mode to show the equivalent dot text (the
+	 * return value is always null).
+	 */
+	public Runner doShowTable() {
+		if (!wrap) {
+			currentMode = VisualizerMode.TABLE;
+			updateDisplay();
+			return null;
+		}
+		return wrapMe();
+	}
+
 	// /** This method changes the display mode to show the equivalent dot text
 	// (the return value is always null). */
 	// public Runner doShowDot() {

diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java
@@ -109,8 +109,11 @@
 import javax.swing.event.ChangeListener;
 import javax.swing.event.HyperlinkEvent;
 import javax.swing.event.HyperlinkListener;
+import javax.swing.plaf.FontUIResource;
 import javax.swing.text.html.HTMLDocument;
 
+import org.alloytools.alloy.core.AlloyCore;
+
 //import com.apple.eawt.Application;
 //import com.apple.eawt.ApplicationAdapter;
 //import com.apple.eawt.ApplicationEvent;
@@ -144,6 +147,10 @@
 import edu.mit.csail.sdg.alloy4.Version;
 import edu.mit.csail.sdg.alloy4.WorkerEngine;
 import edu.mit.csail.sdg.alloy4.XMLNode;
+import edu.mit.csail.sdg.alloy4viz.VizGUI;
+import edu.mit.csail.sdg.alloy4whole.SimpleReporter.SimpleCallback1;
+import edu.mit.csail.sdg.alloy4whole.SimpleReporter.SimpleTask1;
+import edu.mit.csail.sdg.alloy4whole.SimpleReporter.SimpleTask2;
 import edu.mit.csail.sdg.ast.Browsable;
 import edu.mit.csail.sdg.ast.Command;
 import edu.mit.csail.sdg.ast.Expr;
@@ -161,10 +168,6 @@
 import edu.mit.csail.sdg.translator.A4SolutionReader;
 import edu.mit.csail.sdg.translator.A4Tuple;
 import edu.mit.csail.sdg.translator.A4TupleSet;
-import edu.mit.csail.sdg.alloy4viz.VizGUI;
-import edu.mit.csail.sdg.alloy4whole.SimpleReporter.SimpleCallback1;
-import edu.mit.csail.sdg.alloy4whole.SimpleReporter.SimpleTask1;
-import edu.mit.csail.sdg.alloy4whole.SimpleReporter.SimpleTask2;
 import kodkod.engine.fol2sat.HigherOrderDeclException;
 
 /**
@@ -764,7 +767,7 @@ private Runner doNew() {
 	private Runner doOpen() {
 		if (wrap)
 			return wrapMe();
-		File file = OurDialog.askFile(true, null, ".als", ".als files");
+		File file = getFile(null);
 		if (file != null) {
 			Util.setCurrentDirectory(file.getParentFile());
 			doOpenFile(file.getPath());
@@ -776,13 +779,20 @@ private Runner doOpen() {
 	private Runner doBuiltin() {
 		if (wrap)
 			return wrapMe();
-		File file = OurDialog.askFile(true, alloyHome() + fs + "models", ".als", ".als files");
+		File file = getFile(alloyHome() + fs + "models");
 		if (file != null) {
 			doOpenFile(file.getPath());
 		}
 		return null;
 	}
 
+	private File getFile(String home) {
+		File file = OurDialog.askFile(true, home, new String[] {
+				".als", ".md", "*"
+		}, "Alloy (.als) or Markdown (.md) files");
+		return file;
+	}
+
 	/** This method performs File->ReloadAll. */
 	private Runner doReloadAll() {
 		if (!wrap)
@@ -1098,13 +1108,14 @@ private Runner doRefreshRun() {
 		List<Command> cp = commands;
 		if (cp == null) {
 			try {
-				cp = CompUtil.parseOneModule_fromString(text.get().getText());
+				String source = text.get().getText();
+				cp = CompUtil.parseOneModule_fromString(source);
 			} catch (Err e) {
 				commands = null;
 				runmenu.getItem(0).setEnabled(false);
 				runmenu.getItem(3).setEnabled(false);
 				text.shade(new Pos(text.get().getFilename(), e.pos.x, e.pos.y, e.pos.x2, e.pos.y2));
-				if ("yes".equals(System.getProperty("debug")) && VerbosityPref.get() == Verbosity.FULLDEBUG)
+				if (AlloyCore.isDebug() && VerbosityPref.get() == Verbosity.FULLDEBUG)
 					log.logRed("Fatal Exception!" + e.dump() + "\n\n");
 				else
 					log.logRed(e.toString() + "\n\n");
@@ -1216,7 +1227,7 @@ private Runner doRun(Integer commandIndex) {
 			int newmem = SubMemory.get(), newstack = SubStack.get();
 			if (newmem != subMemoryNow || newstack != subStackNow)
 				WorkerEngine.stop();
-			if ("yes".equals(System.getProperty("debug")) && VerbosityPref.get() == Verbosity.FULLDEBUG)
+			if (AlloyCore.isDebug() && VerbosityPref.get() == Verbosity.FULLDEBUG)
 				WorkerEngine.runLocally(task, cb);
 			else
 				WorkerEngine.run(task, newmem, newstack, alloyHome() + fs + "binary", "", cb);
@@ -1734,7 +1745,10 @@ public String compute(Object input) {
 			SimpleTask2 task = new SimpleTask2();
 			task.filename = arg;
 			try {
-				WorkerEngine.run(task, SubMemory.get(), SubStack.get(), alloyHome() + fs + "binary", "", cb);
+				if (AlloyCore.isDebug())
+					WorkerEngine.runLocally(task, cb);
+				else
+					WorkerEngine.run(task, SubMemory.get(), SubStack.get(), alloyHome() + fs + "binary", "", cb);
 				// task.run(cb);
 			} catch (Throwable ex) {
 				WorkerEngine.stop();
@@ -1795,7 +1809,7 @@ private static SimInstance convert(Module root, A4Solution ans) throws Err {
 	private static Computer evaluator = new Computer() {
 		private String filename = null;
 
-		public final String compute(final Object input) throws Exception {
+		public final Object compute(final Object input) throws Exception {
 			if (input instanceof File) {
 				filename = ((File) input).getAbsolutePath();
 				return "";
@@ -1840,11 +1854,12 @@ public final String compute(final Object input) throws Exception {
 			}
 			try {
 				Expr e = CompUtil.parseOneExpression_fromString(root, str);
-				if ("yes".equals(System.getProperty("debug")) && VerbosityPref.get() == Verbosity.FULLDEBUG) {
+				if (AlloyCore.isDebug() && VerbosityPref.get() == Verbosity.FULLDEBUG) {
 					SimInstance simInst = convert(root, ans);
-					return simInst.visitThis(e).toString() + (simInst.wasOverflow() ? " (OF)" : "");
-				} else
-					return ans.eval(e).toString();
+					if (simInst.wasOverflow())
+						return simInst.visitThis(e).toString() + " (OF)";
+				}
+				return ans.eval(e);
 			} catch (HigherOrderDeclException ex) {
 				throw new ErrorType("Higher-order quantification is not allowed in the evaluator.");
 			}
@@ -1867,6 +1882,12 @@ public static void main(final String[] args) throws Exception {
 
 			for (String cmd : args) {
 				switch (cmd) {
+
+					case "--worker" :
+					case "-w" :
+						WorkerEngine.main(args);
+						break;
+
 					case "--version" :
 					case "-v" :
 						System.out.println(Version.version());
@@ -1932,6 +1953,8 @@ public void run() {
 	 */
 	private SimpleGUI(final String[] args) {
 
+		UIManager.put("ToolTip.font", new FontUIResource("Courier New", Font.PLAIN, 14));
+
 		// Register an exception handler for uncaught exceptions
 		MailBug.setup();
 
@@ -2075,24 +2098,8 @@ private void finishInit(String[] args, int width) {
 
 		// Choose the appropriate font
 		int fontSize = FontSize.get();
-		String fontName = FontName.get();
-		while (true) {
-			if (!OurDialog.hasFont(fontName))
-				fontName = "Lucida Grande";
-			else
-				break;
-			if (!OurDialog.hasFont(fontName))
-				fontName = "Verdana";
-			else
-				break;
-			if (!OurDialog.hasFont(fontName))
-				fontName = "Courier New";
-			else
-				break;
-			if (!OurDialog.hasFont(fontName))
-				fontName = "Lucida Grande";
-			break;
-		}
+		String fontName = OurDialog.getProperFontName(FontName.get(), "Courier New", "Lucidia", "Courier",
+				"Monospaced");
 		FontName.set(fontName);
 
 		// Copy required files from the JAR
@@ -2261,7 +2268,7 @@ private void finishInit(String[] args, int width) {
 		text.get().requestFocusInWindow();
 
 		// Launch the welcome screen if needed
-		if (!"yes".equals(System.getProperty("debug")) && Welcome.get()) {
+		if (!AlloyCore.isDebug() && Welcome.get()) {
 			JCheckBox again = new JCheckBox("Show this message every time you start the Alloy Analyzer");
 			again.setSelected(true);
 			OurDialog.showmsg("Welcome", "Thank you for using the Alloy Analyzer " + Version.version(), " ",

diff --git a/...oytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java b/...oytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleReporter.java
@@ -28,6 +28,9 @@
 import java.util.List;
 import java.util.Map;
 import java.util.Set;
+
+import org.alloytools.alloy.core.AlloyCore;
+
 import edu.mit.csail.sdg.alloy4.A4Reporter;
 import edu.mit.csail.sdg.alloy4.ConstList;
 import edu.mit.csail.sdg.alloy4.ConstMap;
@@ -41,20 +44,20 @@
 import edu.mit.csail.sdg.alloy4.Pos;
 import edu.mit.csail.sdg.alloy4.Util;
 import edu.mit.csail.sdg.alloy4.Version;
-import edu.mit.csail.sdg.alloy4.XMLNode;
 import edu.mit.csail.sdg.alloy4.WorkerEngine.WorkerCallback;
 import edu.mit.csail.sdg.alloy4.WorkerEngine.WorkerTask;
+import edu.mit.csail.sdg.alloy4.XMLNode;
+import edu.mit.csail.sdg.alloy4viz.StaticInstanceReader;
+import edu.mit.csail.sdg.alloy4viz.VizGUI;
 import edu.mit.csail.sdg.ast.Command;
-import edu.mit.csail.sdg.ast.Sig;
 import edu.mit.csail.sdg.ast.Module;
+import edu.mit.csail.sdg.ast.Sig;
 import edu.mit.csail.sdg.parser.CompUtil;
 import edu.mit.csail.sdg.translator.A4Options;
 import edu.mit.csail.sdg.translator.A4Solution;
 import edu.mit.csail.sdg.translator.A4SolutionReader;
 import edu.mit.csail.sdg.translator.A4SolutionWriter;
 import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod;
-import edu.mit.csail.sdg.alloy4viz.StaticInstanceReader;
-import edu.mit.csail.sdg.alloy4viz.VizGUI;
 
 /** This helper method is used by SimpleGUI. */
 
@@ -555,7 +558,7 @@ private SimpleReporter(WorkerCallback cb, boolean recordKodkod) {
 	private static void writeXML(A4Reporter rep, Module mod, String filename, A4Solution sol,
 			Map<String,String> sources) throws Exception {
 		sol.writeXML(rep, filename, mod.getAllFunc(), sources);
-		if ("yes".equals(System.getProperty("debug")))
+		if (AlloyCore.isDebug())
 			validate(filename);
 	}
 
@@ -675,7 +678,7 @@ public void run(WorkerCallback out) throws Exception {
 				A4SolutionWriter.writeMetamodel(ConstList.make(sigs), options.originalFilename, of);
 				Util.encodeXMLs(of, "\n</alloy>");
 				Util.close(of);
-				if ("yes".equals(System.getProperty("debug")))
+				if (AlloyCore.isDebug())
 					validate(outf);
 				cb(out, "metamodel", outf);
 				synchronized (SimpleReporter.class) {