Mirrors/mdBook
2
0
Fork 0
mirror of https://github.com/rust-lang/mdBook synced 2024-12-14 06:42:35 +00:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #754 from mattico/playpen-api

Browse source 
Use stable rust playground API
This commit is contained in:
Matt Ickstadt 2018-08-01 15:22:06 -05:00 committed by GitHub
commit 436c084b9e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 17 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/theme/book.js
View file

@ -19,9 +19,16 @@ function playpen_text(playpen) {
// Hide Rust code lines prepended with a specific character
var hiding_character = "#";
function fetch_with_timeout(url, options, timeout = 6000) {
return Promise.race([
fetch(url, options),
new Promise((_, reject) => setTimeout(() => reject(new Error('timeout')), timeout))
]);
}
var playpens = Array.from(document.querySelectorAll(".playpen"));
if (playpens.length > 0) {
fetch("https://play.rust-lang.org/meta/crates", {
fetch_with_timeout("https://play.rust-lang.org/meta/crates", {
headers: {
'Content-Type': "application/json",
},
@ -96,33 +103,28 @@ function playpen_text(playpen) {
let text = playpen_text(code_block);
var params = {
channel: "stable",
mode: "debug",
crateType: "bin",
tests: false,
code: text,
backtrace: false,
version: "stable",
optimize: "0",
code: text
};
if (text.indexOf("#![feature") !== -1) {
params.channel = "nightly";
params.version = "nightly";
}
result_block.innerText = "Running...";
var request = fetch("https://play.rust-lang.org/execute", {
fetch_with_timeout("https://play.rust-lang.org/evaluate.json", {
headers: {
'Content-Type': "application/json",
},
method: 'POST',
mode: 'cors',
body: JSON.stringify(params)
});
request
.then(function (response) { return response.json(); })
.then(function (response) { result_block.innerText = response.success ? response.stdout : response.stderr; })
.catch(function (error) { result_block.innerText = "Playground communication" + error.message; });
})
.then(response => response.json())
.then(response => result_block.innerText = response.result)
.catch(error => result_block.innerText = "Playground Communication: " + error.message);
}
// Syntax highlighting Configuration