From: natile <??>
Date: Fri, 22 Nov 2002 18:39:19 +0000 (+0000)
Subject: toplevel.ml patched but it doesn't compile with open and free variables.
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=226aef203391e48b13bc9142d57cca5d4e25ef53;p=helm.git

toplevel.ml patched but it doesn't compile with open and free variables.
---

diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 78aceae26..d4af37c23 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -1,4 +1,4 @@
-let connection_param = "host=mowgli.cs.unibo.it dbname=helm user=helm"
+let connection_param = "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm"
 
 let show_queries = ref false
 
@@ -25,13 +25,13 @@ let get_terms () =
    let lexbuf = Lexing.from_channel stdin in
    try
       while true do
-         match CicTextualParserContext.main  
-	    (UriManager.uri_of_string "cic:/dummy") [] []
-	    CicTextualLexer.token lexbuf
-	    with
-            | None           -> ()
-            | Some (_, expr) -> terms := expr :: ! terms
-      done;
+       let dom,mk_term =
+        CicTextualParserContext.main [] [] CicTextualLexer.token lexbuf
+       in
+        match dom with
+	   [] -> terms := (snd (mk_term (function _ -> None))) :: !terms
+	 | _ -> assert false
+      done ;
       ! terms
    with
       CicTextualParser0.Eof -> ! terms
@@ -120,7 +120,7 @@ let mbackward n m l =
 	    if Mqint.get_stat () then 
 	       print_string ("? " ^ CicPp.ppterm term ^ nl);
 	    let t0 = Sys.time () in
-            let r = Gen.backward [] [] term level in
+            let r = Gen.searchPattern [] [] term level in
 	    let t1 = Sys.time () -. t0 in
 	    let info = Gen.get_query_info () in
 	    let num = List.nth info 0 in
@@ -192,7 +192,6 @@ let parse_args () =
 
 let _ =
    let module Gen = MQueryGenerator in
-   CicCooking.init () ; 
    Logger.log_callback :=
       (Logger.log_to_html
       ~print_and_flush:(function s -> print_string s ; flush stdout)) ;