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 1a4e6ce65be5230979a62104db7ee913c4d17f5f..da00761f932f2aa7842149c940e3fcd576839ee4 100644 (file)
--- 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 e08847c8fd7290b27a5a73eb43432405a5065c45..eea031f562b2bbde5d04d0d358e898a0b9a52ce7 100644 (file)
--- 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 a07019688f06e837ebacd465ce65cf72b6aae792..0282c3c8dacf71dac985810d17d4d5eb29145dd9 100644 (file)
--- 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 *)