runtime: notify when a file has changed

Also save these new informations into the files database.

src/resource/data_compiler.cpp

@@ -120,6 +120,18 @@ static void notify_remove_tree(const char *path)
 	console_server()->broadcast(string_stream::c_str(ss));
 }
 
+static void notify_change_file(const char *path, Stat& st)
+{
+	TempAllocator512 ta;
+	StringStream ss(ta);
+	ss << "{\"type\":\"change_file\"";
+	ss << ",\"path\":\"" << path << "\"";
+	ss << ",\"size\":\"" << st.size << "\"";
+	ss << ",\"mtime\":\"" << st.mtime << "\"";
+	ss << "}";
+	console_server()->broadcast(string_stream::c_str(ss));
+}
+
 SourceIndex::SourceIndex()
 	: _paths(default_allocator())
 {
@@ -1363,6 +1375,8 @@ void DataCompiler::file_monitor_callback(FileMonitorEvent::Enum fme, bool is_dir
 				Stat st;
 				st = fs.stat(filename);
 				hash_map::set(_source_index._paths, resource_name, st);
+
+				notify_change_file(resource_name.c_str(), st);
 			}
 			break;
 

tools/level_editor/level_editor.vala

@@ -1091,6 +1091,12 @@ public class LevelEditorApplication : Gtk.Application
 			string path = (string)msg["path"];
 
 			_project.remove_tree(path);
+		} else if (msg_type == "change_file") {
+			string path = (string)msg["path"];
+			uint64 size = uint64.parse((string)msg["size"]);
+			uint64 mtime = uint64.parse((string)msg["mtime"]);
+
+			_project.change_file(path, size, mtime);
 		} else if (msg_type == "compile") {
 			// Guid id = Guid.parse((string)msg["id"]);
 

tools/level_editor/project.vala

@@ -51,6 +51,7 @@ public class Project
 	public signal void file_removed(string type, string name);
 	public signal void tree_added(string name);
 	public signal void tree_removed(string name);
+	public signal void file_changed(string type, string name, uint64 size, uint64 mtime);
 	public signal void project_reset();
 	public signal void project_loaded();
 
@@ -424,6 +425,18 @@ public class Project
 		tree_removed(path);
 	}
 
+	public void change_file(string path, uint64 size, uint64 mtime)
+	{
+		string type = path_extension(path);
+		string name = type == "" ? path : path.substring(0, path.last_index_of("."));
+
+		Guid id = _map[path];
+		_files.set_property_string(id, "size", size.to_string());
+		_files.set_property_string(id, "mtime", mtime.to_string());
+
+		file_changed(type, name, size, mtime);
+	}
+
 	public string resource_filename(string absolute_path)
 	{
 		string prefix = _source_dir.get_path();