This commit was manufactured by cvs2svn to create branch

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

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
deleted file mode 100644 (file)
index 2166393..0000000
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ /dev/null
@@ -1,65 +0,0 @@
-let get_terms () =
-   let terms = ref [] in
-   let lexbuf = Lexing.from_channel stdin in
-   try
-      while true do
-         match CicTextualParser.main CicTextualLexer.token lexbuf with
-            | None -> ()
-            | Some expr -> terms := expr :: ! terms
-      done;
-      ! terms
-   with
-      CicTextualParser0.Eof -> ! terms
-
-let locate name = 
-   print_endline (MQueryGenerator.locate name);
-   flush stdout
-
-let rec display = function
-   | []           -> ()
-   | term :: tail -> 
-      display tail;
-      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-      flush stdout
-
-let rec levels level = function
-   | []           -> ()
-   | term :: tail -> 
-      levels level tail;
-      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-      print_endline (MQueryGenerator.levels [] [] term level);
-      flush stdout
-
-let rec backward level = function
-   | []           -> ()
-   | term :: tail -> 
-      backward level tail;
-      print_endline ("? " ^ CicPp.ppterm term ^ "<p>");
-      print_endline (MQueryGenerator.backward [] [] term level);
-      flush stdout
-      
-let parse_args () =
-   let rec parse = function
-      | [] -> ()
-      | ("-l"|"-locate") :: arg :: rem -> 
-         locate arg; parse rem
-      | ("-d"|"-display") :: rem -> 
-         display (get_terms ())
-      | ("-t"|"-test") :: arg :: rem -> 
-        levels (int_of_string arg) (get_terms ())
-      | ("-b"|"-backward") :: arg :: rem -> 
-         backward (int_of_string arg) (get_terms ())
-      | _ :: rem -> parse rem
-   in  
-      parse (List.tl (Array.to_list Sys.argv))
-
-let _ =
-   CicCooking.init () ;
-   Logger.log_callback :=
-      (Logger.log_to_html
-      ~print_and_flush:(function s -> print_string s ; flush stdout)) ;
-   MQueryGenerator.init ();
-   parse_args ();
-   MQueryGenerator.close ();
-   exit 0
-;;