]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 86a71cc)
revert from camlp5o to standard syntax
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 5 Jan 2023 22:06:57 +0000 (23:06 +0100)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 14 Feb 2023 14:23:42 +0000 (15:23 +0100)
matita/components/getter/dune patch | blob | history
matita/components/getter/http_getter_const.ml patch | blob | history
matita/components/getter/http_getter_env.ml patch | blob | history
matita/components/getter/http_getter_misc.ml patch | blob | history
matita/components/getter/http_getter_wget.ml patch | blob | history

diff --git a/matita/components/getter/dune b/matita/components/getter/dune
index b7929d4cfac7223a4887ed78589df1cd3f8371ed..046387d39b0c0a9a65a0ad9608472b3be5ee3a75 100644 (file)
--- 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 8103efcfa3cbffb8adb96d40f8abb2184227eb12..2b2ba79baf6ef90e58fb56c55b658025d549ced9 100644 (file)
--- 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
-"<?xml version=\"1.0\"?>
-<html xmlns=\"%s\" xmlns:helm=\"%s\">
+{xxx|<?xml version="1.0"?>
+<html xmlns="%s" xmlns:helm="%s">
   <head>
     <title>HTTP Getter's help message</title>
   </head>
@@ -54,7 +54,7 @@ let usage_string configuration =
     Available commands:
     </p>
     <p>
-      <b><kbd><a href=\"/help\">help</a></kbd></b><br />
+      <b><kbd><a href="/help">help</a></kbd></b><br />
       display this help message
     </p>
     <p>
@@ -70,33 +70,32 @@ let usage_string configuration =
       <b><kbd>getxslt?uri=URI[&amp;patch_dtd=(yes|no)]</kbd></b><br />
     </p>
     <p>
-      <b><kbd><a href=\"/update\">update</a></kbd></b><br />
+      <b><kbd><a href="/update">update</a></kbd></b><br />
     </p>
     <p>
-      <b><kbd><a href=\"clean_cache\">clean_cache</a></kbd></b><br />
+      <b><kbd><a href="clean_cache">clean_cache</a></kbd></b><br />
     </p>
     <p>
       <b><kbd>ls?baseuri=regexp&amp;format=(txt|xml)</kbd></b><br />
     </p>
     <p>
-      <b><kbd>getalluris?format=(<a href=\"/getalluris?format=txt\">txt</a>|<a href=\"/getalluris?format=xml\">xml</a>)</kbd></b><br />
+      <b><kbd>getalluris?format=(<a href="/getalluris?format=txt">txt</a>|<a href="/getalluris?format=xml">xml</a>)</kbd></b><br />
     </p>
     <p>
-      <b><kbd><a href=\"/getempty\">getempty</a></kbd></b><br />
+      <b><kbd><a href="/getempty">getempty</a></kbd></b><br />
     </p>
     <h2>Current configuration</h2>
     <pre>%s</pre>
   </body>
 </html>
-"
+|xxx}
   xhtml_ns helm_ns
   version configuration
 
 let empty_xml =
-"<?xml version=\"1.0\"?>
+{xxx|<?xml version="1.0"?>
 <!DOCTYPE empty [
   <!ELEMENT empty EMPTY>
 ]>
 <empty />
-"
-
+|xxx}
diff --git a/matita/components/getter/http_getter_env.ml b/matita/components/getter/http_getter_env.ml
index af5896ea83707901343e4fadfe6ccda1e60df189..8ac57184aa3e16f4bb69e056648238368f788843 100644 (file)
--- 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 fa5d780b07be470bdfc1cb729375bfea09e82568..1223af468228dc90b29dd4a6be1571c8bfdcc354 100644 (file)
--- 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 0f44f07d590c083fa183dc969cf356175517a7aa..c900fc2d9ae10b03a9093c7e21a2c6fbcea562fc 100644 (file)
--- 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
Unnamed repository; edit this file 'description' to name the repository.