Minor UI improvements

Fiddle with spacing, margin, fonts.
Improve the display of errors.
Add framework for launching several processes in succession.

compile_server/app/checker.py

@@ -104,7 +104,7 @@ def check_program(request):
     command = ["gnatprove", "-P", "main"]
 
     try:
-        p = process_handling.SeparateProcess(command, target)
+        p = process_handling.SeparateProcess([command], target)
         RUNNING_PROCESSES[identifier] = p
         message = "running gnatprove"
 

compile_server/app/process_handling.py

@@ -7,30 +7,40 @@ from Queue import Queue, Empty
 
 class SeparateProcess(object):
 
-    def __init__(self, cmd, cwd):
-        """Launch the given command line in the background.
-           cmd is a list representing the command line
+    def __init__(self, cmd_lines, cwd):
+        """Launch the given command lines in sequence in the background.
+           cmd_lines is a list of lists representing the command lines
+           to launch.
            cwd is a directory in which the command line is run; this directory
-           is erased when the process is finished.
+           is erased when the processes are finished.
         """
-        self.p = subprocess.Popen(
-            cmd,
-            cwd=cwd,
-            stdout=subprocess.PIPE,
-            stderr=subprocess.STDOUT,
-            bufsize=1,
-            close_fds=True)
+        self.cmd_lines = cmd_lines
         self.q = Queue()
         self.working_dir = cwd
+        self.p = None
         t = Thread(target=self._enqueue_output)
         t.daemon = True
         t.start()
 
     def _enqueue_output(self):
         """The function that reads the output from the process"""
-        for line in iter(self.p.stdout.readline, b''):
-            self.q.put(line)
-        self.p.stdout.close()
+
+        # Launch each process in sequence, in the same task
+        for cmd in self.cmd_lines:
+            self.p = subprocess.Popen(
+                cmd,
+                cwd=self.working_dir,
+                stdout=subprocess.PIPE,
+                stderr=subprocess.STDOUT,
+                bufsize=1,
+                close_fds=True)
+
+            for line in iter(self.p.stdout.readline, b''):
+                self.q.put(line)
+
+            self.p.stdout.close()
+
+        # When all the processes are complete,
         shutil.rmtree(self.working_dir)
 
     def poll(self):
@@ -38,6 +48,8 @@ class SeparateProcess(object):
             return None if the process is still running, otherwise return
             the status code.
         """
+        if not self.p:
+            return None
         self.p.poll()
         return self.p.returncode
 

compile_server/app/static/common.css

@@ -25,3 +25,23 @@ div.output_info{
    padding-left:3px;
    padding-right:3px;
 }
+
+div.output_success{
+   color: #070;
+   padding-left:3px;
+   padding-right:3px;
+   font-weight:bold;
+}
+
+div.output_area{
+   font: 12px/normal 'Monaco', 'Menlo', 'Ubuntu Mono', 'Consolas', 'source-code-pro', monospace;
+   margin-top: 10px;
+}
+
+div.output_row{
+}
+
+div.output_row button{
+   margin-right:4px;
+   margin-top:2px;
+}

compile_server/app/static/editors.js

@@ -5,8 +5,6 @@
 //  message: any message coming back from the application
 //   TODO: make use of message
 function process_check_output(editors, output_area, output, status, completed, message){
-   var found_error_message = false;
-
    // Process the lines
    output.forEach(function (l){
       // Look for lines that contain an error message
@@ -19,7 +17,7 @@ function process_check_output(editors, output_area, output, status, completed, m
       div.appendTo(output_area)
 
       if (match_found != null){
-         found_error_message = true;
+         output_area.error_count++
 
          // Lines that contain a sloc are clickable:
          div.on('click', function(x){
@@ -43,10 +41,20 @@ function process_check_output(editors, output_area, output, status, completed, m
     })
 
     // Congratulations!
-    if (completed && status == 0){
-      var div = $('<div class="output_info">')
-      div.text("Done.")
-      div.appendTo(output_area)
+    if (completed){
+      if (output_area.error_count == 0) {
+         var div = $('<div class="output_success">')
+         div.text("Success!")
+         div.appendTo(output_area)
+      } else if (output_area.error_count == 1) {
+         var div = $('<div class="output_info">')
+         div.text("One error.")
+         div.appendTo(output_area)
+      } else {
+         var div = $('<div class="output_info">')
+         div.text(output_area.error_count + " errors.")
+         div.appendTo(output_area)
+      }
     }
 }
 
@@ -174,6 +182,7 @@ function fill_editor(container, example_name) {
 
           // ... and their contents
           editor.setValue(resource.contents)
+          editor.setShowPrintMargin(false)
           editor.gotoLine(1)
           editor.initial_contents = resource.contents
           editor.basename = resource.basename
@@ -185,12 +194,12 @@ function fill_editor(container, example_name) {
           editors.push(editor)
       })
 
-      var row = $('<div class="row">')
+      var row = $('<div class="row output_row">')
       row.appendTo(container)
 
       // create the buttons
 
-      var buttons_div = $('<div class="col-md-2">')
+      var buttons_div = $('<div class="col-md-3">')
       buttons_div.appendTo(row)
 
       reset_button = $('<button type="button" class="btn btn-secondary">'
@@ -202,7 +211,7 @@ function fill_editor(container, example_name) {
       check_button.editors = editors
       // Create the output area
 
-      var output_div = $('<div class="col-md-8">')
+      var output_div = $('<div class="col-md-9">')
       output_div.appendTo(row)
 
       var output_area = $('<div class="output_area">')
@@ -210,16 +219,18 @@ function fill_editor(container, example_name) {
 
       // Connect the buttons
       reset_button.on('click', function (x){
-          output_area.empty()
+         output_area.empty()
+         output_area.error_count = 0
 
-          reset_button.editors.forEach(function (x){
-             x.setValue(x.initial_contents)
-             x.gotoLine(1)
-          })
+         reset_button.editors.forEach(function (x){
+            x.setValue(x.initial_contents)
+            x.gotoLine(1)
+         })
       })
 
       check_button.on('click', function (x){
          output_area.empty()
+         output_area.error_count = 0
 
          var div = $('<div class="output_info">')
          div.text("Proving...")