From: Claudio Sacerdoti Coen Date: Thu, 5 Jan 2023 22:06:57 +0000 (+0100) Subject: revert from camlp5o to standard syntax X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b161347767b1cb67c4f5b115e4414b85ac4b2183;p=helm.git revert from camlp5o to standard syntax --- diff --git a/matita/components/getter/dune b/matita/components/getter/dune index b7929d4cf..046387d39 100644 --- a/matita/components/getter/dune +++ b/matita/components/getter/dune @@ -1,7 +1,6 @@ (library (name helm_getter) (libraries http unix pcre helm_xml helm_logger helm_ng_kernel helm_registry) - (preprocess (action (system "camlp5o %{input-file}"))) (wrapped false) (modules (:standard \ test))) (env diff --git a/matita/components/getter/http_getter_const.ml b/matita/components/getter/http_getter_const.ml index 8103efcfa..2b2ba79ba 100644 --- a/matita/components/getter/http_getter_const.ml +++ b/matita/components/getter/http_getter_const.ml @@ -39,8 +39,8 @@ let helm_ns = "http://www.cs.unibo.it/helm" (* TODO provide a better usage string *) let usage_string configuration = sprintf -" - +{xxx| + HTTP Getter's help message @@ -54,7 +54,7 @@ let usage_string configuration = Available commands:

- help
+ help
display this help message

@@ -70,33 +70,32 @@ let usage_string configuration = getxslt?uri=URI[&patch_dtd=(yes|no)]

- update
+ update

- clean_cache
+ clean_cache

ls?baseuri=regexp&format=(txt|xml)

- getalluris?format=(txt|xml)
+ getalluris?format=(txt|xml)

- getempty
+ getempty

Current configuration

%s
-" +|xxx} xhtml_ns helm_ns version configuration let empty_xml = -" +{xxx| ]> -" - +|xxx} diff --git a/matita/components/getter/http_getter_env.ml b/matita/components/getter/http_getter_env.ml index af5896ea8..8ac57184a 100644 --- a/matita/components/getter/http_getter_env.ml +++ b/matita/components/getter/http_getter_env.ml @@ -97,17 +97,17 @@ let env_to_string () = | l -> "\n" ^ String.concat "\n" (List.map pp_prefix l) in sprintf -"HTTP Getter %s +{xxx|HTTP Getter %s prefixes:%s -dtd_dir:\t%s -host:\t\t%s -port:\t\t%d -my_own_url:\t%s -dtd_base_urls:\t%s -log_file:\t%s -log_level:\t%d -" +dtd_dir: %s +host: %s +port: %d +my_own_url: %s +dtd_base_urls: %s +log_file: %s +log_level: %d +|xxx} version (pp_prefixes (Lazy.force prefixes)) (match Lazy.force dtd_dir with Some dir -> dir | None -> "NONE") diff --git a/matita/components/getter/http_getter_misc.ml b/matita/components/getter/http_getter_misc.ml index fa5d780b0..1223af468 100644 --- a/matita/components/getter/http_getter_misc.ml +++ b/matita/components/getter/http_getter_misc.ml @@ -300,7 +300,7 @@ let temp_file_of_uri uri = let flat_string s s' c = let cs = Bytes.of_string s in for i = 0 to (String.length s) - 1 do - if String.contains s' s.[i] then cs.[i] <- c + if String.contains s' s.[i] then Bytes.set cs i c done; Bytes.to_string cs in diff --git a/matita/components/getter/http_getter_wget.ml b/matita/components/getter/http_getter_wget.ml index 0f44f07d5..c900fc2d9 100644 --- a/matita/components/getter/http_getter_wget.ml +++ b/matita/components/getter/http_getter_wget.ml @@ -51,7 +51,7 @@ let get_and_save_to_tmp url = let flat_string s s' c = let cs = Bytes.of_string s in for i = 0 to (String.length s) - 1 do - if String.contains s' s.[i] then cs.[i] <- c + if String.contains s' s.[i] then Bytes.set cs i c done; Bytes.to_string cs in