The parser (the lexer indeed) now use the locate query to locate an object

[helm.git] / helm / gTopLevel / gTopLevel.ml

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 ();