- moved exception IllFormedUri, string_of_cic_textual_parser_uri,

  cic_textual_parser_uri_of_string,
  wrong_xpointer_format_from_wrong_xpointer_format' to MQueryMisc
- moved here strip_xml_headings from gTopLevel.ml

diff --git a/helm/gTopLevel/misc.ml b/helm/gTopLevel/misc.ml
index 15cd39f73d1c04a6fc586066b885b006cb73b6c5..e42a0c5f7d1117c8ced9e0e7f2fc30f94e27cb03 100644 (file)
--- a/helm/gTopLevel/misc.ml
+++ b/helm/gTopLevel/misc.ml
@@ -33,67 +33,15 @@
 (*                                                                            *)
 (******************************************************************************)
 
-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
+let domImpl = Gdome.domImplementation ();;
+let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;
 
-(* 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
+  (* TODO BRRRRR .... *)
+  (** strip first 4 line of a string, used to strip xml declaration and doctype
+  declaration from XML strings generated by Xml.pp_to_string *)
+let strip_xml_headings =
+  let xml_headings_RE = Pcre.regexp "^.*\n.*\n.*\n.*\n" in
+  fun s ->
+    Pcre.replace ~rex:xml_headings_RE s
 ;;
 
-let domImpl = Gdome.domImplementation ();;
-let helmns = Gdome.domString "http://www.cs.unibo.it/helm";;

diff --git a/helm/gTopLevel/misc.mli b/helm/gTopLevel/misc.mli
index ac36cfdc0e8d149425d2d81f1db66bad8e5796d4..65ad26c6faa3cfa29ec2f09edb0a6df0e62679d2 100644 (file)
--- a/helm/gTopLevel/misc.mli
+++ b/helm/gTopLevel/misc.mli
@@ -33,11 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
-exception IllFormedUri of string
-val string_of_cic_textual_parser_uri : CicTextualParser0.uri -> string
-val cic_textual_parser_uri_of_string : string -> CicTextualParser0.uri
-
-val wrong_xpointer_format_from_wrong_xpointer_format' : string -> string
-
 val domImpl : Gdome.domImplementation
 val helmns : Gdome.domString
+
+val strip_xml_headings: string -> string
+