From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Sep 2002 17:53:22 +0000 (+0000)
Subject: The parser (the lexer indeed) now use the locate query to locate an object
X-Git-Tag: new_mathql_before_first_merge~49
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5017b0b1d58b9431129055b82a40f73c979bf3ae;p=helm.git

The parser (the lexer indeed) now use the locate query to locate an object
whose identifier is unknown. In ambigous cases, no choice is given to the
user and the usual exception (identifier not found) is raised. It works
only for constants and for the first inductive type of a mutual inductive
type block.
---

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 1a4e6ce65..da00761f9 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -47,9 +47,9 @@ let htmlfooter =
  "</html>"
 ;;
 
-let prooffile = "/home/tassi/miohelm/currentproof";;
+let prooffile = "/public/sacerdot/currentproof";;
 (*CSC: the getter should handle the innertypes, not the FS *)
-let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";;
+let innertypesfile = "/public/sacerdot/innertypes";;
 
 (* GLOBAL REFERENCES (USED BY CALLBACKS) *)
 
@@ -1096,7 +1096,7 @@ let locate rendering_window () =
            | [] -> ""
            | head :: tail ->
 	       inputt#delete_text 0 inputlen;
-	       MQueryGenerator.locate head 
+	       MQueryGenerator.locate_html head 
      with
         e -> "<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>"
   )
@@ -1508,7 +1508,35 @@ let initialize_everything () =
 
 let _ =
  CicCooking.init () ;
- if !usedb then MQueryGenerator.init () ;
+ if !usedb then
+  begin
+   MQueryGenerator.init () ;
+   CicTextualParser0.set_locate_object
+    (function id ->
+      let MathQL.MQRefs uris = MQueryGenerator.locate id in
+       let uri = 
+        match uris with
+           [] -> None
+         | [uri] -> Some uri
+         | _ -> None (* here we must let the user choose one uri *)
+       in
+        match uri with
+           Some uri' ->
+            if String.sub uri' (String.length uri' - 4) 4 = ".con" then
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+             Some (Cic.Const (UriManager.uri_of_string uri',0))
+            else
+             let uri'',typeno =
+(*CSC: the locate query now looks only for inductive type blocks ;-( *)
+(*CSC: when it will be correctly implemented we will have to work    *)
+(*CSC: here on the fragment identifier                               *)
+              uri',0
+             in
+(*CSC: what cooking number? Here I always use 0, which may be bugged *)
+              Some (Cic.MutInd (UriManager.uri_of_string uri'',0,typeno))
+         | None -> None
+    )
+  end ;
  ignore (GtkMain.Main.init ()) ;
  initialize_everything () ;
  if !usedb then MQueryGenerator.close ();
diff --git a/helm/gTopLevel/mQueryGenerator.ml b/helm/gTopLevel/mQueryGenerator.ml
index e08847c8f..eea031f56 100644
--- a/helm/gTopLevel/mQueryGenerator.ml
+++ b/helm/gTopLevel/mQueryGenerator.ml
@@ -167,8 +167,7 @@ let init = Mqint.init
 
 let close = Mqint.close
 
-let locate s = 
-   let query = 
+let locate_query s = 
 (*CSC: next query to be fixed
   1) I am exploiting the bug that does not quote '|'
   2) I am searching only constants and mutual inductive definition blocks
@@ -181,8 +180,9 @@ let locate s =
                              )
                        )
              )
-   in
-   build_result query
+
+let locate s = Mqint.execute (locate_query s)
+let locate_html s = build_result (locate_query s)
 
 let levels e c t level =
    env := e; cont := c;
diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index a07019688..0282c3c8d 100644
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -40,7 +40,8 @@ val init      : unit -> unit     (* INIT database function *)
 
 val close     : unit -> unit     (* CLOSE database function *)
 
-val locate    : string -> string (* LOCATE query building function *)
+val locate    : string -> MathQL.mqresult (* LOCATE query building function *)
+val locate_html : string -> string (* LOCATE query building function *)
 
 val backward  : Cic.metasenv -> Cic.context -> Cic.term -> int -> string
                                  (* BACKWARD query building function *)