diff --git a/compile_server/app/static/book_base.css b/compile_server/app/static/book_base.css index 9d67492..5f68e6b 100755 --- a/compile_server/app/static/book_base.css +++ b/compile_server/app/static/book_base.css @@ -44,6 +44,10 @@ This is the parent `
` that contains the menu and the content area. The content `
` is where all your content goes. */ +#main { + margin: 0 0 0 330px; +} + .content { margin: 0 auto; padding: 0 2em; @@ -105,7 +109,6 @@ appears on the left side of the page. background: #191818; overflow-y: auto; overflow-x: hidden; - overflow-wrap: break-word; -webkit-overflow-scrolling: touch; } @@ -116,7 +119,9 @@ appears on the left side of the page. #sidebar a { color: #999; border: none; - padding: 0.6em 0 0.6em 0.6em; + padding: 0.6em 0.6em 0.6em 0.6em; + + white-space: normal; } /* @@ -138,6 +143,10 @@ appears on the left side of the page. border-top: 1px solid #333; } +#sidebar ul ul { + margin-left: 15px; +} + /* Change color of the anchor links on hover/focus. */ @@ -240,7 +249,7 @@ small screens. Hides the menu at `48em`, but modify this based on your app's needs. */ -@media (min-width: 48em) { +@media (min-width: 1165px) { .header, .content { @@ -268,7 +277,7 @@ Hides the menu at `48em`, but modify this based on your app's needs. } } -@media (max-width: 48em) { +@media (max-width: 1165px) { /* Only apply this when the window is small. Otherwise, the following case results in extra padding on the left: * Make the window small. diff --git a/compile_server/app/static/common.css b/compile_server/app/static/common.css index bac62e4..87b4da1 100644 --- a/compile_server/app/static/common.css +++ b/compile_server/app/static/common.css @@ -53,3 +53,9 @@ div.output_row button{ margin-right:4px; margin-top:2px; } + +.read-only { + background-color: #c0c0c0; + opacity: 0.2; + position: absolute; +} diff --git a/compile_server/app/static/editors.js b/compile_server/app/static/editors.js index bd482f5..8c3da50 100644 --- a/compile_server/app/static/editors.js +++ b/compile_server/app/static/editors.js @@ -1,8 +1,8 @@ // Log an error message in the output area -function output_error(output_area, message){ - var div = $('
') - div.text(message) - div.appendTo(output_area) +function output_error(output_area, message) { + var div = $('
') + div.text(message) + div.appendTo(output_area) } // Process the result of a check @@ -11,137 +11,144 @@ function output_error(output_area, message){ // status: the exit status // message: any message coming back from the application // TODO: make use of message -function process_check_output(editors, output_area, output, status, completed, message){ - // Process the lines +function process_check_output(editors, output_area, output, status, completed, message) { + // Process the lines - read_lines = 0 + read_lines = 0 - output.forEach(function (l){ - read_lines++ + output.forEach(function (l) { + read_lines++ - // Look for lines that contain an error message - var match_found = l.match(/^([a-zA-Z._-]+):(\d+):(\d+):(.+)$/) - var klass = match_found?"output_msg":"output_line" + // Look for lines that contain an error message + var match_found = l.match(/^([a-zA-Z._-]+):(\d+):(\d+):(.+)$/) + var klass = match_found ? "output_msg" : "output_line" - // Print the line in the output area - var div = $('
') - div.text(l) - div.appendTo(output_area) + // Print the line in the output area + var div = $('
') + div.text(l) + div.appendTo(output_area) - if (match_found != null){ - output_area.error_count++ + if (match_found != null) { + output_area.error_count++ - // Lines that contain a sloc are clickable: - div.on('click', function(x){ - // find the corresponding editor - var basename = match_found[1] - editors.forEach(function (e){ - if (e.basename == basename){ - // Switch to the tab that contains the editor - $("#" + e.unique_id + "-tab").tab('show') + // Lines that contain a sloc are clickable: + div.on('click', function (x) { + // find the corresponding editor + var basename = match_found[1] + editors.forEach(function (e) { + if (e.basename == basename) { + // Switch to the tab that contains the editor + $("#" + e.unique_id + "-tab").tab('show') - // Jump to the corresponding line - e.gotoLine(parseInt(match_found[2]), - // looks like column numbers are indexed from 0 - parseInt(match_found[3] - 1), - true) - e.focus() - } - }) - }) - } + // Jump to the corresponding line + e.gotoLine(parseInt(match_found[2]), + // looks like column numbers are indexed from 0 + parseInt(match_found[3] - 1), + true) + e.focus() + } + }) + }) + } }) // Congratulations! - if (completed){ - if ( status != 0 ) { - output_error(output_area, "exit status: " + status) - } else if (output_area.error_count == 0) { - var div = $('
') - div.text("Success!") - div.appendTo(output_area) - } else if (output_area.error_count == 1) { - var div = $('
') - div.text("One error.") - div.appendTo(output_area) - } else { - var div = $('
') - div.text(output_area.error_count + " errors.") - div.appendTo(output_area) - } + if (completed) { + if (status != 0) { + output_error(output_area, "exit status: " + status) + } else if (output_area.error_count == 0) { + var div = $('
') + div.text("Success!") + div.appendTo(output_area) + } else if (output_area.error_count == 1) { + var div = $('
') + div.text("One error.") + div.appendTo(output_area) + } else { + var div = $('
') + div.text(output_area.error_count + " errors.") + div.appendTo(output_area) + } } return read_lines } function get_output_from_identifier(container, editors, output_area, identifier, already_read) { - data = {"identifier": identifier, "already_read": already_read} - $.ajax({ - url: container.example_server + "/check_output/", - data: JSON.stringify(data), - type: "POST", - dataType : "json", - contentType: 'application/json; charset=UTF-8', - }) - .done(function( json ) { - read_lines = process_check_output( - editors, output_area, - json.output_lines, json.status, json.completed, json.message - ) - if (!json.completed) { - // We have not finished processing the output: call this again - setTimeout(function(){ - get_output_from_identifier(container, editors, output_area, identifier, already_read + read_lines) - }, 250) - } - }) - .fail(function( xhr, status, errorThrown ) { - output_error(output_area, "could not download output") - console.log( "Error: " + errorThrown ); - console.log( "Status: " + status ); - console.dir( xhr ); - }) - .fail(function(json) { - output_error(output_area, json.message) - }) + data = { + "identifier": identifier, + "already_read": already_read + } + $.ajax({ + url: container.example_server + "/check_output/", + data: JSON.stringify(data), + type: "POST", + dataType: "json", + contentType: 'application/json; charset=UTF-8', + }) + .done(function (json) { + read_lines = process_check_output( + editors, output_area, + json.output_lines, json.status, json.completed, json.message + ) + if (!json.completed) { + // We have not finished processing the output: call this again + setTimeout(function () { + get_output_from_identifier(container, editors, output_area, identifier, already_read + read_lines) + }, 250) + } + }) + .fail(function (xhr, status, errorThrown) { + output_error(output_area, "could not download output") + console.log("Error: " + errorThrown); + console.log("Status: " + status); + console.dir(xhr); + }) + .fail(function (json) { + output_error(output_area, json.message) + }) } // Launch a run on the given example editor function query_operation_result(container, example_name, editors, output_area, operation_url) { - files = [] + files = [] - editors.forEach(function(e){ - files.push({'basename': e.basename, - 'contents': e.getValue()}) - }) + editors.forEach(function (e) { + files.push({ + 'basename': e.basename, + 'contents': e.getValue() + }) + }) - data = {"example_name": example_name, - "files": files} + data = { + "example_name": example_name, + "files": files + } - // request the examples - $.ajax({ - url: container.example_server + operation_url, - data: JSON.stringify(data), - type: "POST", - dataType : "json", - contentType: 'application/json; charset=UTF-8', - }) - .done(function( json ) { - if (json.identifier == ""){ - output_error(output_area, json.message) - } else { - get_output_from_identifier(container, editors, output_area, json.identifier, 0) - } - }) - .fail(function( xhr, status, errorThrown ) { - // - alert( "could not run the example" ); - console.log( "Error: " + errorThrown ); - console.log( "Status: " + status ); - console.dir( xhr ); - }) + // request the examples + $.ajax({ + url: container.example_server + operation_url, + data: JSON.stringify(data), + type: "POST", + dataType: "json", + contentType: 'application/json; charset=UTF-8', + }) + .done(function (json) { + if (json.identifier == "") { + output_error(output_area, json.message) + } else { + get_output_from_identifier(container, editors, output_area, json.identifier, 0) + } + }) + .fail(function (xhr, status, errorThrown) { + // + alert("could not run the example"); + console.log("Error: " + errorThrown); + console.log("Status: " + status); + console.dir(xhr); + }) } // Fills a
with an editable representation of an example. @@ -151,170 +158,378 @@ function query_operation_result(container, example_name, editors, output_area, o var unique_id = 0 function fill_editor(container, example_name, example_server) { - unique_id++; - container.attr("the_id", unique_id); - container.example_server = example_server; + unique_id++; + container.attr("the_id", unique_id); + container.example_server = example_server; - // request the examples - $.ajax({ - url: container.example_server + "/example/" + example_name, - data: {}, - type: "GET", - // dataType : "json", - contentType: 'text/plain', - crossDomain: true, -// headers: { "Origin": "http://www.adacore.com" } - }) - .done(function( json ) { - // On success, create editors for each of the resources + // request the examples + $.ajax({ + url: container.example_server + "/example/" + example_name, + data: {}, + type: "GET", + // dataType : "json", + contentType: 'text/plain', + crossDomain: true, + // headers: { "Origin": "http://www.adacore.com" } - // First create the tabs + }) + .done(function (json) { + // On success, create editors for each of the resources - var ul = $( '