From 2553de3e2b74919d23f950ed7785bc48b64f231e Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Mon, 4 Sep 2017 13:16:18 -0400
Subject: [PATCH 1/5] Goto line 1 in editors after refresh

Fixes an issue where the initial content was
selected.
---
 compile_server/app/static/editors.js | 4 +++-
 design/notes.txt                     | 1 -
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js
index 2a642e4..dc1e38e 100644
--- a/compile_server/app/static/editors.js
+++ b/compile_server/app/static/editors.js
@@ -66,7 +66,8 @@ function fill_editor(container, example_name) {
           editor.session.setMode("ace/mode/ada");
 
           // ... and their contents
-          editor.insert(resource.contents)
+          editor.setValue(resource.contents)
+          editor.gotoLine(1)
           editor.initial_contents = resource.contents
           editor.filename = resource.basename
 
@@ -84,6 +85,7 @@ function fill_editor(container, example_name) {
       reset_button.on('click', function (x){
           reset_button.editors.forEach(function (x){
              x.setValue(x.initial_contents)
+             x.gotoLine(1)
           })
       })
 
diff --git a/design/notes.txt b/design/notes.txt
index 9857713..013d756 100644
--- a/design/notes.txt
+++ b/design/notes.txt
@@ -9,7 +9,6 @@ Notes just for myself
 
 Frontend
 
-* fix selection after clicking the "reset" button
 * nicer display when an example was not found
 * grab the bits that are currently served by CDNs
 

From f96b572b68c7da63c7a6537bc9c20f671a7783ec Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Mon, 4 Sep 2017 13:20:30 -0400
Subject: [PATCH 2/5] Add missing pyyaml requirement

---
 REQUIREMENTS.txt | 1 +
 1 file changed, 1 insertion(+)

diff --git a/REQUIREMENTS.txt b/REQUIREMENTS.txt
index 6e5370e..f5de22c 100644
--- a/REQUIREMENTS.txt
+++ b/REQUIREMENTS.txt
@@ -1,2 +1,3 @@
 django
 djangorestframework
+pyyaml

From b011b1252d7b279b5f7d9551d1e8cb7778a9d4aa Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Mon, 4 Sep 2017 14:01:38 -0400
Subject: [PATCH 3/5] Add a page which lists all the examples.

And slightly improve the decision as to which file(s) to import
as an example.
---
 .../app/management/commands/fill_examples.py     | 16 ++++++++++------
 compile_server/app/static/editors.js             |  1 -
 compile_server/app/templates/code_page.html      |  1 +
 compile_server/app/templates/examples_list.html  | 16 ++++++++++++++++
 compile_server/app/views.py                      |  5 ++++-
 compile_server/urls.py                           |  6 +++++-
 design/notes.txt                                 |  1 -
 7 files changed, 36 insertions(+), 10 deletions(-)
 create mode 100644 compile_server/app/templates/examples_list.html

diff --git a/compile_server/app/management/commands/fill_examples.py b/compile_server/app/management/commands/fill_examples.py
index 0cb46fa..4a26c74 100644
--- a/compile_server/app/management/commands/fill_examples.py
+++ b/compile_server/app/management/commands/fill_examples.py
@@ -7,6 +7,9 @@ from django.core.management.base import BaseCommand
 
 from compile_server.app.models import Resource, Example
 
+included_extensions = ['.ads', '.adb']
+# The extensions for the files that we want to show in the examples
+
 
 class Command(BaseCommand):
 
@@ -26,7 +29,7 @@ class Command(BaseCommand):
             Example.objects.all().delete()
 
         if options.get('dir', None):
-            d = options.get('dir')[0]
+            d = os.path.abspath(options.get('dir')[0])
 
             # For now, consider all files in the directory to be part of the
             # example
@@ -56,11 +59,12 @@ class Command(BaseCommand):
 
             resources = []
             for file in glob.glob(os.path.join(d, '*')):
-                with open(file, 'rB') as f:
-                    r = Resource(basename=os.path.basename(file),
-                                 contents=f.read())
-                    r.save()
-                    resources.append(r)
+                if any([file.endswith(ext) for ext in included_extensions]):
+                    with open(file, 'rB') as f:
+                        r = Resource(basename=os.path.basename(file),
+                                     contents=f.read())
+                        r.save()
+                        resources.append(r)
 
             e = Example(description=metadata['description'],
                         name=metadata['name'])
diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js
index dc1e38e..6b4b15f 100644
--- a/compile_server/app/static/editors.js
+++ b/compile_server/app/static/editors.js
@@ -92,7 +92,6 @@ function fill_editor(container, example_name) {
       check_button = $('<button type="button" class="btn btn-primary">').text("Check").appendTo(toolbar)
       check_button.editors = editors
       check_button.on('click', function (x){
-         alert(check_button.editors[1].filename)
       })
    })
    .fail(function( xhr, status, errorThrown ) {
diff --git a/compile_server/app/templates/code_page.html b/compile_server/app/templates/code_page.html
index abca53c..425dd60 100644
--- a/compile_server/app/templates/code_page.html
+++ b/compile_server/app/templates/code_page.html
@@ -1,6 +1,7 @@
 {% extends 'base.html' %}
 {% block content %}
 
+ <h3>{{ example_name }}</h3>
  <div example_editor="{{ example_name }}"></div>
 
 {% endblock%}
diff --git a/compile_server/app/templates/examples_list.html b/compile_server/app/templates/examples_list.html
new file mode 100644
index 0000000..fb05da0
--- /dev/null
+++ b/compile_server/app/templates/examples_list.html
@@ -0,0 +1,16 @@
+{% extends 'base.html' %}
+{% block content %}
+
+{% for e in examples %}
+   <h3>{{ e.name }}</h3>
+
+   <div class="row">
+      <div class="col-md-8">
+         {{ e.description }}
+      </div>
+      <div class="col-md-4">
+         <a href="/code_page/{{ e.name }}" class="btn btn-primary btn-lg" role="button" aria-pressed="true">Go</a>
+      </div>
+    </div>
+{% endfor %}
+{% endblock%}
diff --git a/compile_server/app/views.py b/compile_server/app/views.py
index 2b7a3f0..66a48af 100644
--- a/compile_server/app/views.py
+++ b/compile_server/app/views.py
@@ -80,6 +80,9 @@ def example(request, name):
 
 
 def code_page(request, example_name):
-    # TODO: move to a separate file
     context = {'example_name': example_name}
     return render(request, 'code_page.html', context)
+
+def examples_list(request):
+    context = {'examples': Example.objects.all}
+    return render(request, 'examples_list.html', context)
diff --git a/compile_server/urls.py b/compile_server/urls.py
index 8593384..65571e8 100644
--- a/compile_server/urls.py
+++ b/compile_server/urls.py
@@ -25,7 +25,6 @@ router.register(r'users', views.UserViewSet)
 router.register(r'groups', views.GroupViewSet)
 
 urlpatterns = [
-    url(r'^', include(router.urls)),
     url(r'^api-auth/', include('rest_framework.urls',
                                namespace='rest_framework')),
     url(r'^admin/', admin.site.urls),
@@ -44,4 +43,9 @@ urlpatterns = [
     # Get the code viewer on one example
     url(r'^code_page/([^\/]+)$', views.code_page),
 
+    # Get a list of all the examples
+    url(r'^examples_list/', views.examples_list),
+
+    # The landing page
+    url(r'', views.examples_list),
 ]
diff --git a/design/notes.txt b/design/notes.txt
index 013d756..6ff9319 100644
--- a/design/notes.txt
+++ b/design/notes.txt
@@ -16,7 +16,6 @@ Backend
 
 * cleanup the status of imported/invisible files (exclude yaml, project)
 * implement the "check" button
-* implement a page which lists all the examples
 
 Production
 

From 54a1ce7b4f60eb14facc0719c11aa55de22a3fc7 Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Mon, 4 Sep 2017 20:16:02 -0400
Subject: [PATCH 4/5] (WIP) work on checker

---
 compile_server/app/static/editors.js | 35 +++++++++++++++++++++++++++-
 compile_server/app/views.py          |  9 -------
 compile_server/urls.py               |  4 ++--
 3 files changed, 36 insertions(+), 12 deletions(-)

diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js
index 6b4b15f..d2f0b6f 100644
--- a/compile_server/app/static/editors.js
+++ b/compile_server/app/static/editors.js
@@ -1,3 +1,35 @@
+function query_check_result(editors, container) {
+
+   files = []
+
+   editors.forEach(function(e){
+       files.push({'basename': e.basename,
+                   'contents': e.getValue()})
+   })
+
+   data = {"files": files}
+
+   // request the examples
+   $.ajax({
+      url: "/check_program/",
+      data: JSON.stringify(data),
+      type: "POST",
+      dataType : "json",
+      contentType: 'application/json; charset=UTF-8',
+   })
+   .done(function( json ) {
+      alert(json)
+   })
+   .fail(function( xhr, status, errorThrown ) {
+     //
+     alert( "could not run the example" );
+     console.log( "Error: " + errorThrown );
+     console.log( "Status: " + status );
+     console.dir( xhr );
+   })
+}
+
+
 // Fills a <div> with an editable representation of an example.
 //    container: the <div> in question
 //    example_name: the name of the example to load
@@ -69,7 +101,7 @@ function fill_editor(container, example_name) {
           editor.setValue(resource.contents)
           editor.gotoLine(1)
           editor.initial_contents = resource.contents
-          editor.filename = resource.basename
+          editor.basename = resource.basename
 
           // TODO: place the cursor at 1,1
 
@@ -92,6 +124,7 @@ function fill_editor(container, example_name) {
       check_button = $('<button type="button" class="btn btn-primary">').text("Check").appendTo(toolbar)
       check_button.editors = editors
       check_button.on('click', function (x){
+          query_check_result(check_button.editors, container)
       })
    })
    .fail(function( xhr, status, errorThrown ) {
diff --git a/compile_server/app/views.py b/compile_server/app/views.py
index 66a48af..c63d1e8 100644
--- a/compile_server/app/views.py
+++ b/compile_server/app/views.py
@@ -40,15 +40,6 @@ class ResourceSet(viewsets.ModelViewSet):
     serializer_class = ResourceSerializer
 
 
-@api_view(['POST'])
-def check_program(request):
-    received_json = json.loads(request.body)
-    p = Program(code=received_json['program'])
-    serializer = ProgramSerializer(p)
-
-    return Response(serializer.data)
-
-
 @api_view(['GET'])
 def examples(request):
     """Return a list of example names and their description"""
diff --git a/compile_server/urls.py b/compile_server/urls.py
index 65571e8..6efc5b0 100644
--- a/compile_server/urls.py
+++ b/compile_server/urls.py
@@ -18,7 +18,7 @@ from django.contrib import admin
 
 from rest_framework import routers
 
-from compile_server.app import views
+from compile_server.app import views, checker
 
 router = routers.DefaultRouter()
 router.register(r'users', views.UserViewSet)
@@ -30,7 +30,7 @@ urlpatterns = [
     url(r'^admin/', admin.site.urls),
 
     # Check one program
-    url(r'^check_program/', views.check_program),
+    url(r'^check_program/', checker.check_program),
 
     # Get a list of the examples
     url(r'^examples/', views.examples),

From 6e41451a08276f9b1215d79c2b91d501e366c4bc Mon Sep 17 00:00:00 2001
From: Nicolas Setton <setton@adacore.com>
Date: Wed, 6 Sep 2017 09:14:18 -0400
Subject: [PATCH 5/5] Initial revision of checker, work in progress

---
 compile_server/app/checker.py                 | 24 +++++++++++++++++++
 .../app/management/commands/fill_examples.py  |  1 +
 compile_server/app/models.py                  |  3 +++
 compile_server/app/serializers.py             |  8 ++++++-
 compile_server/app/static/editors.js          |  8 ++++---
 compile_server/app/templates/code_page.html   |  6 +++--
 compile_server/app/views.py                   | 12 ++++++++--
 design/notes.txt                              | 14 +++++++++++
 8 files changed, 68 insertions(+), 8 deletions(-)
 create mode 100644 compile_server/app/checker.py

diff --git a/compile_server/app/checker.py b/compile_server/app/checker.py
new file mode 100644
index 0000000..675ab9c
--- /dev/null
+++ b/compile_server/app/checker.py
@@ -0,0 +1,24 @@
+# -*- coding: utf-8 -*-
+
+import json
+
+from rest_framework.response import Response
+from rest_framework.decorators import api_view
+
+from compile_server.app.models import Resource, Example
+
+
+@api_view(['POST'])
+def check_program(request):
+    received_json = json.loads(request.body)
+
+    matches = Example.objects.filter(name=received_json['example_name'])
+
+    if not matches:
+        return Response()
+
+    e = matches[0]
+    print received_json
+    print e
+    result = {'output': "bla\nbla\nbla"}
+    return Response(result)
diff --git a/compile_server/app/management/commands/fill_examples.py b/compile_server/app/management/commands/fill_examples.py
index 4a26c74..c014bef 100644
--- a/compile_server/app/management/commands/fill_examples.py
+++ b/compile_server/app/management/commands/fill_examples.py
@@ -67,6 +67,7 @@ class Command(BaseCommand):
                         resources.append(r)
 
             e = Example(description=metadata['description'],
+                        original_dir=d,
                         name=metadata['name'])
             e.save()
             e.resources.add(*resources)
diff --git a/compile_server/app/models.py b/compile_server/app/models.py
index 1c11e82..8a5c33e 100644
--- a/compile_server/app/models.py
+++ b/compile_server/app/models.py
@@ -40,5 +40,8 @@ class Example(models.Model):
     # A description
     description = models.TextField()
 
+    # The directory which contains the original contents
+    original_dir = models.TextField()
+
     # An example is a contains a set of resources
     resources = models.ManyToManyField(Resource)
diff --git a/compile_server/app/serializers.py b/compile_server/app/serializers.py
index 17a6614..c9390d3 100644
--- a/compile_server/app/serializers.py
+++ b/compile_server/app/serializers.py
@@ -1,6 +1,6 @@
 from django.contrib.auth.models import User, Group
 from rest_framework import serializers
-from compile_server.app.models import Resource
+from compile_server.app.models import Resource, Example
 
 
 class UserSerializer(serializers.HyperlinkedModelSerializer):
@@ -31,3 +31,9 @@ class ResourceSerializer(serializers.Serializer):
         instance.basename = validated_data.get('basename', instance.basename)
         instance.save()
         return instance
+
+
+class ExampleSerializer(serializers.ModelSerializer):
+    class Meta:
+        model = Example
+        fields = ('name', 'description')
diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js
index d2f0b6f..cda006b 100644
--- a/compile_server/app/static/editors.js
+++ b/compile_server/app/static/editors.js
@@ -1,4 +1,5 @@
-function query_check_result(editors, container) {
+// Launch a check on the given example editor
+function query_check_result(example_name, editors, container) {
 
    files = []
 
@@ -7,7 +8,8 @@ function query_check_result(editors, container) {
                    'contents': e.getValue()})
    })
 
-   data = {"files": files}
+   data = {"example_name": example_name,
+           "files": files}
 
    // request the examples
    $.ajax({
@@ -124,7 +126,7 @@ function fill_editor(container, example_name) {
       check_button = $('<button type="button" class="btn btn-primary">').text("Check").appendTo(toolbar)
       check_button.editors = editors
       check_button.on('click', function (x){
-          query_check_result(check_button.editors, container)
+         query_check_result(example_name, check_button.editors, container)
       })
    })
    .fail(function( xhr, status, errorThrown ) {
diff --git a/compile_server/app/templates/code_page.html b/compile_server/app/templates/code_page.html
index 425dd60..8dd0a3a 100644
--- a/compile_server/app/templates/code_page.html
+++ b/compile_server/app/templates/code_page.html
@@ -1,7 +1,9 @@
 {% extends 'base.html' %}
 {% block content %}
 
- <h3>{{ example_name }}</h3>
- <div example_editor="{{ example_name }}"></div>
+ <h3>{{ example.name }}</h3>
+ {{ example.description }}
+ <p></p>
+ <div example_editor="{{ example.name }}"></div>
 
 {% endblock%}
diff --git a/compile_server/app/views.py b/compile_server/app/views.py
index c63d1e8..6a7acb4 100644
--- a/compile_server/app/views.py
+++ b/compile_server/app/views.py
@@ -13,7 +13,8 @@ from rest_framework.decorators import api_view
 from rest_framework.response import Response
 from compile_server.app.serializers import (UserSerializer,
                                             GroupSerializer,
-                                            ResourceSerializer)
+                                            ResourceSerializer,
+                                            ExampleSerializer)
 
 from compile_server.app.models import Resource, Example
 
@@ -71,9 +72,16 @@ def example(request, name):
 
 
 def code_page(request, example_name):
-    context = {'example_name': example_name}
+    matches = Example.objects.filter(name=example_name)
+    if not matches:
+        return Response()
+
+    e = matches[0]
+    serializer = ExampleSerializer(e)
+    context = {'example': serializer.data}
     return render(request, 'code_page.html', context)
 
+
 def examples_list(request):
     context = {'examples': Example.objects.all}
     return render(request, 'examples_list.html', context)
diff --git a/design/notes.txt b/design/notes.txt
index 6ff9319..82886e4 100644
--- a/design/notes.txt
+++ b/design/notes.txt
@@ -33,3 +33,17 @@ curl -H 'Accept: application/json; indent=4' http://127.0.0.1:8000/check_program
 
 # get the examples
 curl -H 'Accept: application/json; indent=4' http://127.0.0.1:8000/examples/ --header "Content-Type:application/json"
+
+#############################
+# Import Yannick's examples #
+#############################
+
+# TODO: add a facility to do this
+
+# Setup:
+cd resources ; git clone https:AdaCore/Compile_And_Prove_Demo.git
+
+# Import:
+./manage.py fill_examples --remove_all
+list="hello_world absolute_value bitwise_swap saturate_angle sensor_average strings communications landing_procedure"
+for a in $list; do ./manage.py fill_examples --dir=resources/Compile_And_Prove_Demo/examples/$a ; done