From 22c1709c72244a2270d6258a2a206a1ee9d496a7 Mon Sep 17 00:00:00 2001 From: Christoph Schwering Date: Thu, 6 Apr 2017 11:52:50 +1000 Subject: [PATCH] Fixed: custom Sudoku bug. --- examples/sudoku/sudoku-js.html | 34 +++++++++++++++++++++++++--------- examples/tui/tui-js.html | 8 ++++++-- 2 files changed, 31 insertions(+), 11 deletions(-) diff --git a/examples/sudoku/sudoku-js.html b/examples/sudoku/sudoku-js.html index 4134b06..1ae852f 100644 --- a/examples/sudoku/sudoku-js.html +++ b/examples/sudoku/sudoku-js.html @@ -17,6 +17,7 @@ form .label { display: inline-block; min-width: 15em; } form input.number { width: 5em; } + #custom { font-family: monospace; } #play-button { background-color: black; color: #eee; font-family: inherit; font-weight: bold; font-size: 100%; margin-top: 1ex; margin-left: 1em; padding-left: 3em; padding-right: 3em; padding-top: 1ex; padding-bottom: 1ex; } #play-button { background: @@ -44,6 +45,13 @@ + @@ -64,9 +72,9 @@ For further demos and details on the reasoner, click here.
Sudoku game:
- +
Max. number of case splits:

@@ -79,13 +87,15 @@ $(document).ready(function() { $('#configs').change(function() { var config = document.getElementById('configs').value; if (config) { - initGame(); $('#custom').hide(); } else { - $('#custom').show(); + $('#custom').show().focus(); } + initGame(); }); - $('#custom').change(function() { initGame($('#custom').val()); }).hide(); + $('#custom').change(function() { initGame(); }); + $('#custom').keyup(function() { initGame(); }); + $('#custom').hide(); $.ajax({ url : 'sudokus.txt', dataType: 'text', @@ -114,14 +124,20 @@ $(document).ready(function() { var t0 = null; -function initGame(config, max_k) { +function initGame() { + if (!runtimeIsReadyFlag) { + return; + } $('#output').empty(); + config = document.getElementById('configs').value; if (!config) { - config = document.getElementById('configs').value; + config = $('#custom').val(); } - if (!max_k) { - max_k = document.getElementById('max_k').value; + if (!config) { + config = ''; } + config = config.replace(/\s/g,''); + max_k = document.getElementById('max_k').value; if (max_k == null) { max_k = 2; } diff --git a/examples/tui/tui-js.html b/examples/tui/tui-js.html index 4fb2dd4..f4f3323 100644 --- a/examples/tui/tui-js.html +++ b/examples/tui/tui-js.html @@ -42,7 +42,7 @@ +
-- GitLab