Changeset 8bbfd4d in tol for tol/stdlib/general/grammars/_text.tol

Timestamp:

Feb 8, 2012, 6:57:11 PM (15 years ago)

Author:

Víctor de Buen <vdebuen@…>

Branches:

1941-docker-image-to-test, devel, master

Children:

aaf0528

Parents:

b83b8ed3

Message:

Fixes #1423
Downloading traces are controlled by TolConfigManager::Config::Various::Verbose::DownloadingUrl

git-svn-id: ​https://www.tol-project.org/svn/tolp/trunk@4081 be4846ae-f051-483a-831f-b64e7d08527f

File:

• tol/stdlib/general/grammars/_text.tol (modified) (5 diffs)

tol/stdlib/general/grammars/_text.tol

@@ -1172 +1172 @@
 //////////////////////////////////////////////////////////////////////////////
 {
-  Write("[GetUrlContents.tcl.uri] Downloading from \""+url+"\" ... ");
+  If(TolConfigManager::Config::Various::Verbose::DownloadingUrl,
+  Write("[GetUrlContents.tcl.uri] Downloading from \""+url+"\" ... "));
   Text tcl_helper = 
     "package require uri\n"+
@@ -1192 +1193 @@
     Text If(result["status"], 
     {
-      WriteLn("OK");
+      If(TolConfigManager::Config::Various::Verbose::DownloadingUrl,
+      WriteLn("OK"));
       Text result["result"]
     },
@@ -1212 +1214 @@
 //////////////////////////////////////////////////////////////////////////////
 {
-  Write("[GetUrlContents.tcl.curl] Downloading from \""+url_+"\" ... ");
+  If(TolConfigManager::Config::Various::Verbose::DownloadingUrl,
+  Write("[GetUrlContents.tcl.curl] Downloading from \""+url_+"\" ... "));
   Set result1 = CurlApi::GetUrl( [[ Text url = url_ ]] );
   If( result1::failStatus, 
@@ -1221 +1224 @@
   }, 
   {
-    WriteLn("OK");
+    If(TolConfigManager::Config::Various::Verbose::DownloadingUrl,
+    WriteLn("OK"));
     result1::bodyData
   })
@@ -1230 +1234 @@
 //////////////////////////////////////////////////////////////////////////////
 {
-  WriteLn("[GetUrlContents.sys.wget]Downloading from \""+url+"\" ...");
+  If(TolConfigManager::Config::Various::Verbose::DownloadingUrl,
+  WriteLn("[GetUrlContents.sys.wget]Downloading from \""+url+"\" ..."));
   Text tmp = TmpDir+"wget."<<IntRand(111111111,999999999)+".tmp";
   Text order = "wget -O"+tmp+" "+url;