]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/gTopLevel.ml
untested version of mQueryGenerator (was mquery part 2)
[helm.git] / helm / gTopLevel / gTopLevel.ml
index 4a8b0a382486a2e082811488e26a28f228b441df..d052040c5f8177502ac4e2a4c1cee1cb879cf3ea 100644 (file)
@@ -1072,7 +1072,7 @@ let locate rendering_window () =
            | [] -> ""
            | head :: tail ->
               inputt#delete_text 0 inputlen;
-              Mquery.locate head 
+              MQueryGenerator.locate head 
      with
         e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
   )
@@ -1096,7 +1096,7 @@ let backward rendering_window () =
              let (_,_,ty) =
               List.find (function (m,_,_) -> m=metano) metasenv
              in
-              Mquery.backward ty level
+              MQueryGenerator.backward ty level
        in 
    output_html outputhtml result
       
@@ -1471,8 +1471,8 @@ let initialize_everything () =
 
 let _ =
  CicCooking.init () ;
- Mquery.init () ;
+ MQueryGenerator.init () ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
- Mquery.close ()
+ MQueryGenerator.close ()
 ;;