From 3c0c88529205896b69c91e072342262e65062529 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Wed, 11 Dec 2019 17:15:51 +0100
Subject: [PATCH] [Server] Add service for retrieving the current project
source filenames.
---
src/plugins/server/kernel_project.ml | 12 ++++++++++++
1 file changed, 12 insertions(+)
diff --git a/src/plugins/server/kernel_project.ml b/src/plugins/server/kernel_project.ml
index f2fd2ec4d9e..052bc13e3f8 100644
--- a/src/plugins/server/kernel_project.ml
+++ b/src/plugins/server/kernel_project.ml
@@ -121,3 +121,15 @@ let () = Request.register ~page
(ProjectRequest.process `EXEC)
(* -------------------------------------------------------------------------- *)
+(* --- Project Management --- *)
+(* -------------------------------------------------------------------------- *)
+
+let () =
+ Request.register
+ ~kind:`GET
+ ~page ~name:"kernel.project.getSourceFiles"
+ ~descr:(Md.plain "Get the files of the current project")
+ ~input:(module Junit) ~output:(module Jstring.Jlist)
+ Kernel.Files.get
+
+(* -------------------------------------------------------------------------- *)
--
GitLab