# HG changeset patch # User Adam Chlipala # Date 1322947509 18000 # Node ID bd34a4af516a3bdcec5023d30f448c6a2694820f # Parent f96e708b4b93ef8801acadd79a3a71e47195efb8 Change client-side debug to use console.debug diff -r f96e708b4b93 -r bd34a4af516a lib/js/urweb.js --- a/lib/js/urweb.js Sat Dec 03 16:05:06 2011 -0500 +++ b/lib/js/urweb.js Sat Dec 03 16:25:09 2011 -0500 @@ -338,6 +338,16 @@ // Error handling +function uw_debug(msg) { + try { + console.debug(msg); + } catch (e) { + alert("DEBUG: " + msg); + } + + return 0; +} + function whine(msg) { alert(msg); throw msg; diff -r f96e708b4b93 -r bd34a4af516a src/settings.sml --- a/src/settings.sml Sat Dec 03 16:05:06 2011 -0500 +++ b/src/settings.sml Sat Dec 03 16:25:09 2011 -0500 @@ -270,8 +270,8 @@ ("lt_time", "lt"), ("le_time", "le"), - ("debug", "alert"), - ("naughtyDebug", "alert"), + ("debug", "uw_debug"), + ("naughtyDebug", "uw_debug"), ("floatFromInt", "float"), ("ceil", "ceil"), diff -r f96e708b4b93 -r bd34a4af516a tests/csdebug.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/csdebug.ur Sat Dec 03 16:25:09 2011 -0500 @@ -0,0 +1,5 @@ +fun main () : transaction page = + n <- source 0; + return +