From 226aef203391e48b13bc9142d57cca5d4e25ef53 Mon Sep 17 00:00:00 2001 From: natile Date: Fri, 22 Nov 2002 18:39:19 +0000 Subject: [PATCH] toplevel.ml patched but it doesn't compile with open and free variables. --- helm/gTopLevel/topLevel/topLevel.ml | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) 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)) ; -- 2.39.2