[isabelle-dev] Dead code smells

[Makarius]

Some notes concerning the following recent changes:

   082edd97ffe1 huffman
   comment out dead code to avoid compiler warnings

   6f28f96a09bf huffman
   avoid warnings

A priori, warnings are really just warnings, not errors.


When Poly/ML acquired this very useful warning for unused identifiers, I 
did go through all my code and cross-checked if I agree with the compiler. 
There were typically one of the following cases:

   (1) There is genuine unused stuff that is better removed altogether.
       (Maybe 90% of the time.)

   (2) Certain unused arguments indicate a deeper problem in the code -- it
       requires some care and understanding how things work exactly to amend this.
       Removing the offending identifiers merely makes things worse,
       because semantic unclarities are swept under the carpet.
       (May happens a few % of the time.)

   (3) Small named arguments that actually improved readability and
       uniformity.  (Up to 10% of the time.)

       Here is a trivial example from src/Pure/library.ML:

         fun fst (x, y) = x;
         fun snd (x, y) = y;

       Replacing everything by "_" blindly is not really progress in code quality.


I have occasionally tried to clean up things like positivstellensatz.ML 
myself, but failed to do it right without substantial involvement. 
(Without the latter the preferred style of the original author takes 
precedence, even if it happens to be suboptimal.)

Dead code really starts smelling quickly and should not be introduced at 
all.  Either it is left in and statically checked, or removed from the 
text.  (The history is 100% persistent so interested parties can retrieve 
old material any time.)


 	Makarius