]> matita.cs.unibo.it Git - helm.git/commitdiff
* fix bug detect blank nodes
authorLuca Padovani <luca.padovani@unito.it>
Tue, 9 Nov 2004 12:05:09 +0000 (12:05 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Tue, 9 Nov 2004 12:05:09 +0000 (12:05 +0000)
* output of file size

helm/papers/use_case/stats/Makefile
helm/papers/use_case/stats/stats.cc

index fa5f5e2e907ec882e5cbf0b1a9c4b6dff2a395b7..6db5d94691cfb9c3cddf30554c62b3a28b9974c0 100644 (file)
@@ -2,3 +2,14 @@
 stats: stats.cc
        g++ -o $@ `pkg-config gdome2-cpp-smart --cflags --libs` $<
 
+stats.xml:
+       echo "<statistics>" >stats.xml
+       find /local/helm/library/coq_contribs/$(CONTRIB) -type f -exec ./stats.sh {} \; >>stats.xml
+       echo "</statistics>" >>stats.xml
+
+stats.html: stats.xml
+       xsltproc mkhtml.xsl $< >$@
+
+stats.txt: stats.html
+       w3m -dump a.html > a.txt
+
index a7016f0ee83cdc44454ac42d5f4b402cf9d52399..f2b128faf89540d53d93ac115f6161923c53a6e6 100644 (file)
@@ -22,7 +22,7 @@ bool
 is_blank(const std::string& s)
 {
   for (int i = 0; i < s.length(); i++)
-    if (!isblank(s[i])) return false;
+    if (!isspace(s[i])) return false;
   return true;
 }
 
@@ -75,7 +75,7 @@ visit(DOM::Node node, int depth)
 }
 
 void
-print_results(const std::string& URI)
+print_results(const std::string& URI, long size)
 {
   int n_depths = 0;
   int tot_depth = 0;
@@ -92,6 +92,7 @@ print_results(const std::string& URI)
     tot_width += *p;
 
   std::cout << "<stats for=\"" << URI << "\">" << std::endl;
+  std::cout << "  <size>" << size << "</size>" << std::endl;
   std::cout << "  <depth>" << std::endl;
   std::cout << "    <max>" << max_depth << "</max>" << std::endl;
   std::cout << "    <leaf-avg>" << tot_depth / ((double) n_depths) << "</leaf-avg>" << std::endl;
@@ -118,13 +119,13 @@ print_results(const std::string& URI)
 int
 main(int argc, char* argv[])
 {
-  if (argc != 2) {
-    std::cerr << "Usage: stats <URI>" << std::endl;
+  if (argc != 3) {
+    std::cerr << "Usage: stats <URI> <size>" << std::endl;
     return -1;
   }
 
   DOM::DOMImplementation di;
   DOM::Document doc = di.createDocumentFromURI(argv[1]);
   visit(doc, 0);
-  print_results(argv[1]);
+  print_results(argv[1], atoi(argv[2]));
 }