Merge branch 'master' into highprecision

examples/quickcheck/src/main/java/quickcheck/commands/QCConsole.java

@@ -24,16 +24,17 @@
 
 package quickcheck.commands;
 
-import com.fujitsu.vdmj.Settings;
 import com.fujitsu.vdmj.messages.Console;
+import com.fujitsu.vdmj.plugins.PluginConsole;
 
 /**
- * This copies the PluginConsole from VDMJ to allow us to have "global" quiet
+ * This extends the PluginConsole from VDMJ to allow us to have "global" quiet
  * setting within the QC command environment, without affecting the outer
- * environment.
+ * environment. By extending PluginConsole, we get a "private" quiet flag
+ * that won't interfere with the global one, but we can still use the inherited
+ * methods as well.
  */
-
-public class QCConsole
+public class QCConsole extends PluginConsole
 {
 	private static boolean quiet = false;
 
@@ -46,20 +47,12 @@ public static boolean getQuiet()
 	{
 		return quiet;
 	}
-
-	public static void verbose(String format, Object... args)
-	{
-		if (Settings.verbose)
-		{
-			Console.out.printf(format, args);
-		}
-	}
 
-	public static void verboseln(String m)
+	public static void info(String m)
 	{
-		if (Settings.verbose)
+		if (!quiet)
 		{
-			Console.out.println(m);
+			Console.out.print(m);
 		}
 	}
 
@@ -78,24 +71,4 @@ public static void infoln(Object m)
 			Console.out.println(m.toString());
 		}
 	}
-
-	public static void println(Object m)
-	{
-		Console.out.println(m.toString());
-	}
-
-	public static void printf(String format, Object... args)
-	{
-		Console.out.printf(format, args);
-	}
-
-	public static void errorln(Object m)
-	{
-		Console.err.println(m.toString());
-	}
-
-	public static void errorf(String format, Object... args)
-	{
-		Console.err.printf(format, args);
-	}
 }

examples/quickcheck/src/main/java/quickcheck/plugin/QuickCheckLSPPlugin.java

@@ -27,6 +27,7 @@
 import com.fujitsu.vdmj.lex.Dialect;
 import com.fujitsu.vdmj.util.Utils;
 
+import json.JSONObject;
 import quickcheck.commands.QuickCheckLSPCommand;
 import vdmj.commands.AnalysisCommand;
 import vdmj.commands.HelpList;
@@ -51,6 +52,17 @@ public void init()
 		// Get everything from PO?
 	}
 
+	@Override
+	public void setServerCapabilities(JSONObject capabilities)
+	{
+		JSONObject experimental = capabilities.get("experimental");
+
+		if (experimental != null)
+		{
+			experimental.put("quickCheckProvider", true);
+		}
+	}
+
 	@Override
 	public AnalysisCommand getCommand(String line)
 	{

vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INExplicitFunctionDefinition.java

@@ -145,7 +145,7 @@ public NameValuePairList getNamedValues(Context ctxt)
 			postfunc.uninstantiated = (typeParams != null);
 		}
 
-		if (measureDef != null && measureDef.name.getName().startsWith("measure_"))
+		if (measureDef != null && measureDef.name.isMeasureName())
 		{
 			// Add implicit measure_* functions and any pre_measure_*s too.
 			nvl.addAll(measureDef.getNamedValues(ctxt));

vdmj/src/main/java/com/fujitsu/vdmj/in/definitions/INImplicitFunctionDefinition.java

@@ -157,7 +157,7 @@ public NameValuePairList getNamedValues(Context ctxt)
 			postfunc.uninstantiated = (typeParams != null);
 		}
 
-		if (measureDef != null && measureDef.name.getName().startsWith("measure_"))
+		if (measureDef != null && measureDef.name.isMeasureName())
 		{
 			// Add implicit measure_* functions and any pre_measure_*s too.
 			nvl.addAll(measureDef.getNamedValues(ctxt));

vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POExplicitFunctionDefinition.java

@@ -185,7 +185,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			}
 		}
 
-		if (measureDef != null && measureName != null && measureName.getName().startsWith("measure_"))
+		if (measureDef != null && measureName != null && measureName.isMeasureName())
 		{
 			ctxt.push(new PONameContext(new TCNameList(measureName)));
 			obligations.addAll(measureDef.getProofObligations(ctxt, env));

vdmj/src/main/java/com/fujitsu/vdmj/po/definitions/POImplicitFunctionDefinition.java

@@ -179,7 +179,7 @@ public ProofObligationList getProofObligations(POContextStack ctxt, Environment
 			}
 		}
 
-		if (measureDef != null && measureName != null && measureName.getName().startsWith("measure_"))
+		if (measureDef != null && measureName != null && measureName.isMeasureName())
 		{
 			ctxt.push(new PONameContext(new TCNameList(measureName)));
 			obligations.addAll(measureDef.getProofObligations(ctxt, env));

vdmj/src/main/java/com/fujitsu/vdmj/runtime/Breakpoint.java

@@ -270,13 +270,19 @@ public void enterDebugger(Context ctxt)
 	{
 		Thread current = Thread.currentThread();
 
+		/**
+		 * We can only debug expression breakpoints that occur from within SchedulableThreads,
+		 * usually MainThread or InitThread etc. But it is possible to perform very high
+		 * performance evaluations without creating extra SchedulableThreads, though these
+		 * cannot be debugged and they are responsible for handling their own ContextExceptions
+		 * and so on...
+		 */
 		if (current instanceof SchedulableThread)
 		{
 			SchedulableThread th = (SchedulableThread)current;
 			th.suspendOthers();
+			DebugLink.getInstance().breakpoint(ctxt, this);
 		}
-
-		DebugLink.getInstance().breakpoint(ctxt, this);
 	}
 
 	/**

vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCExplicitFunctionDefinition.java

@@ -368,7 +368,7 @@ else if (measureExp != null)
 
 		if (!(body instanceof TCNotYetSpecifiedExpression) &&
 			!(body instanceof TCSubclassResponsibilityExpression) &&
-			!(name.getName().startsWith("measure_")))
+			!(name.isMeasureName()))
 		{
 			checked.unusedCheck();	// Look underneath qualified definitions, if any
 		}
@@ -646,7 +646,7 @@ public TCDefinitionList getDefinitions()
 			defs.add(postdef);
 		}
 
-		if (measureName != null && measureName.getName().startsWith("measure_"))
+		if (measureName != null && measureName.isMeasureName())
 		{
 			defs.add(measureDef);
 		}

vdmj/src/main/java/com/fujitsu/vdmj/tc/definitions/TCImplicitFunctionDefinition.java

@@ -513,7 +513,7 @@ public TCDefinitionList getDefinitions()
 			defs.add(postdef);
 		}
 
-		if (measureName != null && measureName.getName().startsWith("measure_"))
+		if (measureName != null && measureName.isMeasureName())
 		{
 			defs.add(measureDef);
 		}

vdmj/src/main/java/com/fujitsu/vdmj/tc/lex/TCNameToken.java

@@ -212,6 +212,11 @@ public TCNameToken getMeasureName(LexLocation l)
 		return new TCNameToken(l, getModule(), "measure_" + getName(), false, false);
 	}
 
+	public boolean isMeasureName()
+	{
+		return lexname.name.startsWith("measure_");		// True, if a generated measure function
+	}
+
 	public TCNameToken getResultName(LexLocation l)
 	{
 		return new TCNameToken(l, getModule(), "RESULT", false, false);

vdmj/src/main/java/com/fujitsu/vdmj/util/Utils.java

@@ -237,11 +237,18 @@ public static String getVersion()
 		{
 			String path = VDMJ.class.getName().replaceAll("\\.", "/");
 			URL url = VDMJ.class.getResource("/" + path + ".class");
-			JarURLConnection conn = (JarURLConnection)url.openConnection();
-		    JarFile jar = conn.getJarFile();
-			Manifest mf = jar.getManifest();
-			String version = (String)mf.getMainAttributes().get(Attributes.Name.IMPLEMENTATION_VERSION);
-			return version;
+
+			if (url.getProtocol().equals("jar"))
+			{
+				JarURLConnection conn = (JarURLConnection)url.openConnection();
+			    JarFile jar = conn.getJarFile();
+				Manifest mf = jar.getManifest();
+				return (String)mf.getMainAttributes().get(Attributes.Name.IMPLEMENTATION_VERSION);
+			}
+			else
+			{
+				return "(no version available in " + url.getProtocol() + ")";
+			}
 		}
 		catch (Exception e)
 		{