From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 5 Sep 2002 14:15:47 +0000 (+0000)
Subject: mQueryGenerator and topLevel patched
X-Git-Tag: new_mathql_before_first_merge~45
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=86ec68f575f6f781572d14d0aba9a98a860c94a6;p=helm.git

mQueryGenerator and topLevel patched
---

diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index eea031f56..5c6fb27d7 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -1,28 +1,63 @@
-open MQueryUtil
-open MathQL
-open Cic
-
-(* raw HTML representation *)
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     Ferruccio Guidi <fguidi@cs.unibo.it>                   *)
+(*                                 30/04/2002                                 *)
+(*                                                                            *)
+(*                                                                            *)
+(******************************************************************************)
 
-let res s = "<font color=\"brown\">\"" ^ s ^ "\" </font>"
-
-let nl () = "<br>"
-
-let par () = "<p>"
+open Cic
+open MathQL
+open MQueryHTML
+open MQueryUtil
 
-(* CIC term inspecting functions *)
+(* CIC term inspecting functions ********************************************)
 
-let env = ref []   (* metasemv *)
-let cont = ref []  (* context  *)
+let env = ref []     (* metasemv *)
+let cont = ref []    (* context  *)
 
 let ie_out (r, b, v) =
    let pos = string_of_int v ^ if b then " HEAD: " else " TAIL: " in
-   res (pos ^ str_uref r) ^ nl () (* FG: si puo' usare xp_str_uref se si vuole xpointer *) 
+   res (pos ^ str_uref r) ^ nl () 
+      (* FG: si puo' usare xp_str_uref se si vuole xpointer *) 
 
 let rec il_out = function
    | []           -> ""
    | head :: tail -> ie_out head ^ il_out tail
 
+let rec il_max = function
+   | []                -> 0
+   | (_, _, v) :: tail -> 
+      let v0 = il_max tail in
+      if v > v0 then v else v0
+
 let ie_str_uri (u, b, v) = xp_str_uref u
 
 let rec il_restrict level = function
@@ -112,13 +147,22 @@ let rec inspect_backbone = function
 
 let inspect t = inspect_backbone t  
 
-(* query building functions *)
+(* query building functions *************************************************)
+
+let issue = ref (fun _ -> true)
 
 let save s = 
    let och = open_out_gen [Open_wronly; Open_append; Open_creat; Open_text]
                           (64 * 6 + 8 * 6 + 4) "MQGenLog.htm" in
    output_string och s; flush och; s
 
+let build_result query =
+   if ! issue query then
+      let html = par () ^ out_query query ^ nl () in
+      let result = Mqint.execute query in
+      save (html ^ out_result result)
+    else ""
+    
 let build_select (r, b, v) n  =
    let rvar = "ref" ^ string_of_int n in
    let svar = "str" ^ string_of_int n in
@@ -158,11 +202,6 @@ let restrict_universe query =
         )
       )
 
-let build_result query =
-   let html = par () ^ out_query query ^ nl () in
-   let result = Mqint.execute query in
-   save (html ^ out_result result)
-
 let init = Mqint.init
 
 let close = Mqint.close
@@ -184,11 +223,14 @@ let locate_query s =
 let locate s = Mqint.execute (locate_query s)
 let locate_html s = build_result (locate_query s)
 
-let levels e c t level =
+let levels e c t =
    env := e; cont := c;
    let il = inspect t in
    par () ^ il_out il ^ nl ()
 
+let call_back f =
+   issue := f
+
 let backward e c t level =
    env := e; cont := c;
    let il = inspect t in
diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index 0282c3c8d..69cbfeba5 100644
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -33,9 +33,11 @@
 (*                                                                            *)
 (******************************************************************************)
 
-val levels  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
+val levels    : Cic.metasenv -> Cic.context -> Cic.term -> string
                                  (* level assignment testing function *)
 
+val call_back : (MathQL.mquery -> bool) -> unit
+
 val init      : unit -> unit     (* INIT database function *)
 
 val close     : unit -> unit     (* CLOSE database function *)
diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 32ae4d1cb..7736c1a29 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -28,7 +28,7 @@ let pp_type_of uri =
    in print_endline s; flush stdout
 
 let locate name = 
-   print_endline (MQueryGenerator.locate name);
+   print_endline (MQueryGenerator.locate_html name);
    flush stdout
 
 let rec display = function