From 5017b0b1d58b9431129055b82a40f73c979bf3ae Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 4 Sep 2002 17:53:22 +0000 Subject: [PATCH] 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. --- helm/gTopLevel/gTopLevel.ml | 36 ++++++++++++++++++++++++++---- helm/gTopLevel/mQueryGenerator.ml | 8 +++---- helm/gTopLevel/mQueryGenerator.mli | 3 ++- 3 files changed, 38 insertions(+), 9 deletions(-) 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 = "" ;; -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 -> "

" ^ Printexc.to_string e ^ "

" ) @@ -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 *) -- 2.39.2