From a75ee46e89747c8761331dd4c5229dbedfebfdad Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Wed, 28 Jun 2017 13:37:56 +0000
Subject: [PATCH] FileSetting: Only create editor/render when needed, i.e.,
 only from the GUI, not command-line.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11999 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/settings/FileSetting.java | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/prism/src/settings/FileSetting.java b/prism/src/settings/FileSetting.java
index db1da84c..6cb8edc3 100644
--- a/prism/src/settings/FileSetting.java
+++ b/prism/src/settings/FileSetting.java
@@ -35,12 +35,6 @@ public class FileSetting extends Setting
     private static FileRenderer renderer;
     private static FileEditor editor;
     
-    static
-    {
-        renderer = new FileRenderer();
-        editor = new FileEditor();
-    }
-	
 	private static FileSelector defaultSelector()
 	{
 		try {
@@ -106,11 +100,17 @@ public class FileSetting extends Setting
     
     public SettingEditor getSettingEditor()
     {
+        if (editor == null) {
+        	editor = new FileEditor();
+        }
         return editor;
     }
     
     public SettingRenderer getSettingRenderer()
     {
+        if (renderer == null) {
+        	renderer = new FileRenderer();
+        }
         return renderer;
     }