- added and exposed get_current_status_as_xml

[helm.git] / helm / gTopLevel / mQueryLevels.ml

diff --git a/helm/gTopLevel/mQueryLevels.ml b/helm/gTopLevel/mQueryLevels.ml
index ecadbd84bf48898aaf89d97cbcb8441e04ca1893..977638dba90adbb4d3dbd4008a5d25cc60b5f92a 100644 (file)
--- a/helm/gTopLevel/mQueryLevels.ml
+++ b/helm/gTopLevel/mQueryLevels.ml
@@ -33,10 +33,6 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(* level managing functions *************************************************)
-
-type levels_spec = (string * bool * int) list
-
 let levels_of_term metasenv context term =
    let module TC = CicTypeChecker in
    let module Red = CicReduction in
@@ -130,31 +126,12 @@ let levels_of_term metasenv context term =
    in 
    inspect_backbone term  
 
-let string_of_levels l sep =
-   let entry_out (s, b, v) =
-      let pos = if b then " HEAD: " else " TAIL: " in
-      string_of_int v ^ pos ^ s ^ sep 
-   in
-   let rec levels_out = function
-      | []           -> ""
-      | head :: tail -> entry_out head ^ levels_out tail
-   in
-   levels_out l
-
-
 let out_restr e c t =   
-(*  let rec restrict level = function
-       | []                -> []
-       | (u, b, v) :: tail ->
-          if v <= level then (u, b, v) :: restrict level tail
-          else restrict level tail
-  in*)
-
   let can = levels_of_term e c t in  (* can restrictions *)
-print_endline "";
-         print_string "#### IN LEVELS @@@@ lunghezza can:";
-         print_int (List.length can); flush stdout;
-         print_endline "";
+prerr_endline "";
+prerr_endline
+ ("#### IN LEVELS @@@@ lunghezza can: " ^ string_of_int (List.length can));
+prerr_endline "";
 (*  let rest = restrict level levels in   *)
   let uri_pos (u,b,v) = (u,b) in
   let can_use = List.map uri_pos can in
@@ -168,5 +145,4 @@ print_endline "";
   let mrest = List.map lofl can in
   let must_use = organize_restr mrest [] in (* must restrictions *)
   (must_use,can_use)
-
-
+;;