Merge pull request #1036 from gusthoff/topic/issues/1020

Widget: include SPARK project in downloaded zip file

frontend/src/ts/download.ts

@@ -9,6 +9,13 @@ pragma Restrictions (No_Use_Of_Pragma => Linker_Options);
 pragma Restrictions (No_Dependence => System.Machine_Code);
 pragma Restrictions (No_Dependence => Machine_Code);\n`;
 
+const SPARK_ADC = `pragma Profile(GNAT_Extended_Ravenscar);
+pragma Partition_Elaboration_Policy(Sequential);
+pragma SPARK_Mode (On);
+pragma Warnings (Off, "no Global contract available");
+pragma Warnings (Off, "subprogram * has no effect");
+pragma Warnings (Off, "file name does not match");\n`;
+
 const MAIN_GPR = `project Main is
 
    --MAIN_PLACEHOLDER--
@@ -28,6 +35,25 @@ const MAIN_GPR = `project Main is
 
 end Main;\n`;
 
+const SPARK_GPR = `project Main_Spark is
+
+   --MAIN_PLACEHOLDER--
+
+   --LANGUAGE_PLACEHOLDER--
+
+   package Compiler is
+      for Default_Switches ("Ada") use ("-g", "-O0");
+      --COMPILER_SWITCHES_PLACEHOLDER--
+   end Compiler;
+
+   package Builder is
+      for Default_Switches ("Ada") use ("-g");
+      --BUILDER_SWITCHES_PLACEHOLDER--
+      for Global_Configuration_Pragmas use "main_spark.adc";
+   end Builder;
+
+end Main_Spark;\n`;
+
 const languageMapping = {
   '"Ada"': ['.adb', 'ads'],
   '"c"': ['.c', '.h'],
@@ -155,17 +181,24 @@ export function getMain(files: ResourceList, main: string): string {
  * @param {ResourceList} files to be zipped. Used in main finding logic.
  * @param {UnparsedSwitches} switches to be included in the gpr file.
  * @param {string} main provided by data-main for the project.
+ * @param {boolean} sparkMode SPARK is being used.
  * @return {string} the contents of the gpr file to be generated.
  */
 export function getGprContents(
     files: ResourceList,
     switches: UnparsedSwitches,
-    main: string
+    main: string,
+    sparkMode: boolean
 ): string {
   const languages = getLanguages(files);
   const parsedSwitches = parseSwitches(switches);
   const newMain = getMain(files, main);
   let gpr = MAIN_GPR;
+
+  if (sparkMode) {
+    gpr = SPARK_GPR;
+  }
+
   gpr = gpr.replace('--MAIN_PLACEHOLDER--', newMain);
   gpr = gpr.replace('--LANGUAGE_PLACEHOLDER--', languages);
   gpr = gpr.replace(
@@ -185,12 +218,14 @@ export function getGprContents(
  * @param {UnparsedSwitches} switches to be included in the gpr file
  * @param {string} main provided by data-main for the project
  * @param {string} name of the zip
+ * @param {boolean} sparkMode SPARK is being used.*
  */
 export function downloadProject(
     files: ResourceList,
     switches: UnparsedSwitches,
     main: string,
-    name: string
+    name: string,
+    sparkMode: boolean
 ): void {
   const zip = new JSZip();
 
@@ -199,13 +234,26 @@ export function downloadProject(
     zip.file(f.basename, f.contents);
   }
 
+  let adcFile = COMMON_ADC;
+
   // Add the ADC to the zip
-  zip.file('main.adc', COMMON_ADC);
+  zip.file('main.adc', adcFile);
 
   // Add the gpr to the zip
-  const gpr = getGprContents(files, switches, main);
+  const gpr = getGprContents(files, switches, main, false);
   zip.file('main.gpr', gpr);
 
+  if (sparkMode) {
+    adcFile = SPARK_ADC;
+
+    // Add the ADC to the zip
+    zip.file('main_spark.adc', adcFile);
+
+    // Add the gpr to the zip
+    const gpr = getGprContents(files, switches, main, sparkMode);
+    zip.file('main_spark.gpr', gpr);
+  }
+
   // Create and download the zip
   zip.generateAsync({type: 'blob'}).then((blob) => {
     FileSaver.saveAs(blob, `${name}.zip`);

frontend/src/ts/widget.ts

@@ -208,7 +208,8 @@ class Widget {
         Builder: switches['Builder'],
         Compiler: this.getActiveCompilerSwitches()};
       const main = this.container.dataset.main as string;
-      downloadProject(files, activeSwitches, main, this.name);
+      const sparkMode = true;
+      downloadProject(files, activeSwitches, main, this.name, sparkMode);
     });
 
     // grab reference to output area in the HTML and construct area

frontend/tests/ts/download.spec.ts

@@ -229,12 +229,18 @@ describe('Download', () => {
   describe('#getGprContents()', () => {
     it('should replace all placeholders', () => {
       const files: ResourceList = [{basename: 'main.adb', contents: ''}];
-      const gpr = getGprContents(files, {Builder: [], Compiler: []}, 'main.adb');
+      const gpr = getGprContents(files, {Builder: [], Compiler: []}, 'main.adb', false);
       expect(gpr).to.not.contain('--MAIN_PLACEHOLDER--');
       expect(gpr).to.not.contain('--LANGUAGE_PLACEHOLDER--');
       expect(gpr).to.not.contain('--COMPILER_SWITCHES_PLACEHOLDER--');
       expect(gpr).to.not.contain('--BUILDER_SWITCHES_PLACEHOLDER--');
       expect(gpr).to.not.contain('--');
+      const gpr_spark = getGprContents(files, {Builder: [], Compiler: []}, 'main.adb', true);
+      expect(gpr_spark).to.not.contain('--MAIN_PLACEHOLDER--');
+      expect(gpr_spark).to.not.contain('--LANGUAGE_PLACEHOLDER--');
+      expect(gpr_spark).to.not.contain('--COMPILER_SWITCHES_PLACEHOLDER--');
+      expect(gpr_spark).to.not.contain('--BUILDER_SWITCHES_PLACEHOLDER--');
+      expect(gpr_spark).to.not.contain('--');
     });
   });
 });