]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/lib/log.ml
we removed some old code and fixed a reduction bug: two instances fo the
[helm.git] / helm / software / lambda-delta / lib / log.ml
index 4cea12cda89eef2d4e0c5d45bae5ebd9b9c8797b..9c2ecefa2721f90b8365651527a0314c93951a5e 100644 (file)
@@ -17,6 +17,7 @@ type ('a, 'b) item = Term of 'a * 'b
                    | Context of 'a
                    | Warn of string
                   | String of string
+                   | Loc
 
 type ('a, 'b) specs = {
    pp_term   : 'a -> F.formatter -> 'b -> unit;
@@ -25,6 +26,8 @@ type ('a, 'b) specs = {
 
 let level = ref 0
 
+let loc = ref 0
+
 (* Internal functions *******************************************************)
 
 let std = F.std_formatter
@@ -37,6 +40,7 @@ let pp_items frm st l items =
       | Context c   -> F.fprintf frm "%a" st.pp_context c
       | Warn s      -> F.fprintf frm "@,%s" s
       | String s    -> F.fprintf frm "%s " s
+      | Loc         -> F.fprintf frm " (line %u)" !loc 
    in
    let iter map frm l = List.iter (map frm) l in
    if !level >= l then F.fprintf frm "%a" (iter pp_item) items