diff --git a/src/main/java/common/ConfigurationTTool.java b/src/main/java/common/ConfigurationTTool.java index 850bf4594340c3fa71990db3bda980f5c0c6cbe6..6e321ddebb91d793f0f5e14a32c9e9fb670f3580 100755 --- a/src/main/java/common/ConfigurationTTool.java +++ b/src/main/java/common/ConfigurationTTool.java @@ -160,6 +160,8 @@ public class ConfigurationTTool { public static String URL_MODEL = "http://ttool.telecom-paristech.fr/networkmodels/models.txt"; // Others + public static String RGStyleSheet = ""; + public static String LastOpenFile = ""; public static boolean LastOpenFileDefined = false; @@ -172,6 +174,8 @@ public class ConfigurationTTool { public static String ExternalServer = ""; public static String ProVerifHash = ""; + + public static void makeDefaultConfiguration() { //System.out.println(Paths.get("").toAbsolutePath().toString()); //System.out.println("User.dir path:" + System.getProperty("user.dir")); @@ -496,6 +500,8 @@ public class ConfigurationTTool { sb.append("LastWindowAttributesHeight: ").append(LastWindowAttributesHeight).append("\n"); sb.append("LastWindowAttributesMax: ").append(LastWindowAttributesMax).append("\n"); + sb.append("\nRG stylesheet configuration:").append(RGStyleSheet).append("\n"); + //Huy Truong sb.append("ExternalServer ").append(ExternalServer).append("\n"); @@ -797,6 +803,10 @@ public class ConfigurationTTool { if (nl.getLength() > 0) LastWindowAttributes(nl); + nl = doc.getElementsByTagName("RGStyleSheet"); + if (nl.getLength() > 0) + RGStyleSheet(nl); + nl = doc.getElementsByTagName("ExternalServer"); if (nl.getLength() > 0) ExternalServer(nl); @@ -1569,6 +1579,14 @@ public class ConfigurationTTool { } } + private static void RGStyleSheet(NodeList nl) throws MalformedConfigurationException { + try { + Element elt = (Element) (nl.item(0)); + RGStyleSheet = elt.getAttribute("data"); + } catch (Exception e) { + throw new MalformedConfigurationException(e.getMessage()); + } + } private static void ExternalServer(NodeList nl) throws MalformedConfigurationException { try { diff --git a/src/main/java/ui/graph/AUTGraphDisplay.java b/src/main/java/ui/graph/AUTGraphDisplay.java index 3881d604d8ea548903c1f0f8c7dfd1ad4e769133..d0d2de9a0d29bc15f30dfbf8d21c534a4800858b 100755 --- a/src/main/java/ui/graph/AUTGraphDisplay.java +++ b/src/main/java/ui/graph/AUTGraphDisplay.java @@ -39,6 +39,7 @@ package ui.graph; +import common.ConfigurationTTool; import common.SpecConfigTTool; import myutil.TraceManager; import org.graphstream.graph.implementations.AbstractEdge; @@ -120,7 +121,13 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable System.setProperty("org.graphstream.ui.renderer", "org.graphstream.ui.j2dviewer.J2DGraphRenderer"); vGraph = new MultiGraph("TTool graph"); - vGraph.addAttribute("ui.stylesheet", STYLE_SHEET); + if ((ConfigurationTTool.RGStyleSheet != null) && (ConfigurationTTool.RGStyleSheet.trim().length() > 0)) { + TraceManager.addDev("Adding stylesheet:" + ConfigurationTTool.RGStyleSheet+ "\n\nvs default:" + STYLE_SHEET); + vGraph.addAttribute("ui.stylesheet", ConfigurationTTool.RGStyleSheet ); + } else { + vGraph.addAttribute("ui.stylesheet", STYLE_SHEET); + } + //vGraph.addAttribute("layout.weight", 0.5); int cpt = 0; graph.computeStates(); for (AUTState state : graph.getStates()) { @@ -145,6 +152,7 @@ public class AUTGraphDisplay implements MouseListener, ViewerListener, Runnable TraceManager.addDev("Transition=" + tmp);*/ edge.addAttribute("ui.label", transition.transition); edge.addAttribute("ui.class", "defaultedge"); + edge.addAttribute("layout.weight", 0.4); if (!(transition.transition.startsWith("i("))) { edge.addAttribute("ui.class", "external"); }