print_string ("? " ^ CicPp.ppterm term ^ nl);
flush stdout
-let levels l =
- let module Lev = MQueryLevels in
- let rec levels_aux = function
- | [] -> ()
- | term :: tail ->
- levels_aux tail;
- print_string ("? " ^ CicPp.ppterm term ^ nl);
- print_string (Lev.string_of_levels (Lev.levels_of_term [] [] term) nl);
- flush stdout
- in
- levels_aux l
-
let execute ich =
let module Util = MQueryUtil in
let module Gen = MQueryGenerator in
prerr_endline "-t -typeof URI outputs the CIC type of the given HELM object";
prerr_endline "-x -execute issues a query given in the input file";
prerr_endline "-d -disply outputs the CIC terms given in the input file";
- prerr_endline "-l -levels outputs the cut levels of the CIC terms given in the input file";
prerr_endline "-L -locate ALIAS issues the \"Locate\" query for the given alias";
prerr_endline "-B -backward LEVEL issues the \"Backward\" query for the given level on all CIC terms";
prerr_endline " in the input file";
| ("-h"|"-help") :: rem -> prerr_help ()
| ("-d"|"-display") :: rem -> display (get_terms ())
| ("-t"|"-typeof") :: arg :: rem -> pp_type_of arg; parse rem
- | ("-l"|"-levels") :: rem -> levels (get_terms ())
| ("-x"|"-execute") :: rem -> execute stdin; parse rem
| ("-q"|"-show-queries") :: rem -> show_queries := true; parse rem
| ("-s"|"-stat") :: rem -> Mqint.set_stat true; parse rem