Minor code reorganization:

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

diff --git a/helm/gTopLevel/disambiguate.ml b/helm/gTopLevel/disambiguate.ml
index 11de21b18789afe44ffb8f20a2f48dd76d864bf5..ff794fd5b2d03052bbea92803443159b059dda2e 100644 (file)
--- a/helm/gTopLevel/disambiguate.ml
+++ b/helm/gTopLevel/disambiguate.ml
@@ -33,70 +33,6 @@
 (*                                                                            *)
 (******************************************************************************)
 
-(** Functions that should be moved in another module **)
-
-exception IllFormedUri of string;;
-
-let string_of_cic_textual_parser_uri uri =
- let module C = Cic in
- let module CTP = CicTextualParser0 in
-  let uri' =
-   match uri with
-      CTP.ConUri uri -> UriManager.string_of_uri uri
-    | CTP.VarUri uri -> UriManager.string_of_uri uri
-    | CTP.IndTyUri (uri,tyno) ->
-       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1)
-    | CTP.IndConUri (uri,tyno,consno) ->
-       UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (tyno + 1) ^ "/" ^
-        string_of_int consno
-  in
-   (* 4 = String.length "cic:" *)
-   String.sub uri' 4 (String.length uri' - 4)
-;;
-
-let cic_textual_parser_uri_of_string uri' =
- prerr_endline ("cic_textual_parser_uri_of_string INPUT = " ^ uri');
- try
-  (* Constant *)
-  if String.sub uri' (String.length uri' - 4) 4 = ".con" then
-   CicTextualParser0.ConUri (UriManager.uri_of_string uri')
-  else
-   if String.sub uri' (String.length uri' - 4) 4 = ".var" then
-    CicTextualParser0.VarUri (UriManager.uri_of_string uri')
-   else
-    (try
-      (* Inductive Type *)
-      let uri'',typeno = CicTextualLexer.indtyuri_of_uri uri' in
-       CicTextualParser0.IndTyUri (uri'',typeno)
-     with
-      _ ->
-       (* Constructor of an Inductive Type *)
-       let uri'',typeno,consno =
-        CicTextualLexer.indconuri_of_uri uri'
-       in
-        CicTextualParser0.IndConUri (uri'',typeno,consno)
-    )
- with
-  _ -> raise (IllFormedUri uri')
-;;
-let cic_textual_parser_uri_of_string uri' =
-  let res = cic_textual_parser_uri_of_string uri' in
-  prerr_endline ("RESULT: " ^ (string_of_cic_textual_parser_uri res));
-  res
-
-(* CSC: quick fix: a function from [uri#xpointer(path)] to [uri#path] *)
-let wrong_xpointer_format_from_wrong_xpointer_format' uri =
- try
-  let index_sharp =  String.index uri '#' in
-  let index_rest = index_sharp + 10 in
-   let baseuri = String.sub uri 0 index_sharp in
-   let rest =
-    String.sub uri index_rest (String.length uri - index_rest - 1)
-   in
-    baseuri ^ "#" ^ rest
- with Not_found -> uri
-;;
-
 (* CSC: IMPERATIVE AND NOT VERY CLEAN, TO GET THE LAST ISSUED QUERY *)
 let get_last_query = 
  let query = ref "" in
@@ -135,7 +71,7 @@ module Make(C:Callbacks) =
     let uris =
      List.map
       (function uri,_ ->
-        wrong_xpointer_format_from_wrong_xpointer_format' uri
+        Misc.wrong_xpointer_format_from_wrong_xpointer_format' uri
       ) result in
     let html=
      " <h1>Locate Query: </h1><pre>" ^ get_last_query result ^ "</pre>"
@@ -160,7 +96,7 @@ module Make(C:Callbacks) =
           ~id
           uris
      in
-      List.map cic_textual_parser_uri_of_string uris'
+      List.map Misc.cic_textual_parser_uri_of_string uris'
 
 
    exception ThereDoesNotExistAnyWellTypedInterpretationOfTheInput