Commit ab24d4f9 authored by MARCHE Claude's avatar MARCHE Claude

Merge branch 'master' into new_system+itp

# Conflicts:
#	src/util/strings.ml
parents f172f2e5 cb83244e
......@@ -98,8 +98,8 @@ INCLUDES = @ZIPINCLUDE@ @MENHIRINCLUDE@
WARNINGS = A-4-9-41-44-45-50-52@5@48
OFLAGS = -w $(WARNINGS) -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
OFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
BFLAGS = -w $(WARNINGS) -safe-string -keep-locs -bin-annot -dtypes -g -I lib/why3 $(INCLUDES)
OLINKFLAGS = -linkall $(EXTCMXA)
BLINKFLAGS = -linkall $(EXTCMA)
......
......@@ -477,15 +477,18 @@ dnl AC_CHECK_PROG(enable_ide,lablgtk2,yes,no) not always available (Win32)
dnl AC_CHECK_PROG(OCAMLWEB,ocamlweb,ocamlweb,true)
# js_of_ocaml
JSOFOCAML=$(ocamlfind query js_of_ocaml)
if test -z "$JSOFCAML"; then
HASJSOFOCAML=no
reason_jsofocaml=" (js_of_ocaml not found)"
# checking for js_of_ocaml
if test "$USEOCAMLFIND" = yes; then
JSOFOCAML=$(ocamlfind query js_of_ocaml)
if test -z "$JSOFOCAML"; then
HASJSOFOCAML=no
reason_jsofocaml=" (js_of_ocaml not found)"
else
HASJSOFOCAML=yes
fi
else
HASJSOFOCAML=yes
HASJSOFOCAML=no
reason_jsofocaml=" (ocamlfind not available)"
fi
# Coq
......
......@@ -55,12 +55,12 @@ let send_request_string msg =
let to_write = String.length msg in
let rec write pointer =
if pointer < to_write then
let written = Unix.write sock msg pointer (to_write - pointer) in
let written = Unix.write_substring sock msg pointer (to_write - pointer) in
write (pointer + written)
in write 0
let read_from_client =
let buf = String.make 1024 ' ' in
let buf = Bytes.make 1024 ' ' in
fun blocking ->
match !socket with
| None -> raise NotConnected
......@@ -73,7 +73,7 @@ let read_from_client =
in
if do_read then
let read = Unix.read sock buf 0 1024 in
String.sub buf 0 read
Bytes.sub_string buf 0 read
else ""
(* TODO/FIXME: should we be able to change this setting when
......
This diff is collapsed.
......@@ -129,7 +129,7 @@ let files : string Queue.t = Queue.create ()
let opt_parser = ref None
let spec = Arg.align [
let spec = [
"-F", Arg.String (fun s -> opt_parser := Some s),
"<format> select input format (default: \"why\")";
"--format", Arg.String (fun s -> opt_parser := Some s),
......
......@@ -9,7 +9,6 @@
(* *)
(********************************************************************)
open Why3.Strings
open Format
let blocking = false
......@@ -51,28 +50,29 @@ let decode s =
match s.[i] with
'%' when i + 2 < String.length s ->
let v = hexa_val s.[i + 1] * 16 + hexa_val s.[i + 2] in
set s1 i1 (Char.chr v); i + 3
| '+' -> set s1 i1 ' '; succ i
| x -> set s1 i1 x; succ i
Bytes.set s1 i1 (Char.chr v); i + 3
| '+' -> Bytes.set s1 i1 ' '; succ i
| x -> Bytes.set s1 i1 x; succ i
in
copy_decode_in s1 i (succ i1)
else s1
in
let rec strip_heading_and_trailing_spaces s =
if String.length s > 0 then
if s.[0] == ' ' then
let sl = Bytes.length s in
if sl > 0 then
if Bytes.get s 0 == ' ' then
strip_heading_and_trailing_spaces
(String.sub s 1 (String.length s - 1))
else if s.[String.length s - 1] == ' ' then
(Bytes.sub s 1 (sl - 1))
else if Bytes.get s (sl - 1) == ' ' then
strip_heading_and_trailing_spaces
(String.sub s 0 (String.length s - 1))
(Bytes.sub s 0 (sl - 1))
else s
else s
in
if need_decode 0 then
let len = compute_len 0 0 in
let s1 = create len in
strip_heading_and_trailing_spaces (copy_decode_in s1 0 0)
let s1 = Bytes.create len in
Bytes.to_string (strip_heading_and_trailing_spaces (copy_decode_in s1 0 0))
else s
let special =
......@@ -101,22 +101,23 @@ let encode s =
if i < String.length s then
let i1 =
match s.[i] with
' ' -> set s1 i1 '+'; succ i1
' ' -> Bytes.set s1 i1 '+'; succ i1
| c ->
if special c then
begin
set s1 i1 '%';
set s1 (i1 + 1) (hexa_digit (Char.code c / 16));
set s1 (i1 + 2) (hexa_digit (Char.code c mod 16));
Bytes.set s1 i1 '%';
Bytes.set s1 (i1 + 1) (hexa_digit (Char.code c / 16));
Bytes.set s1 (i1 + 2) (hexa_digit (Char.code c mod 16));
i1 + 3
end
else begin set s1 i1 c; succ i1 end
else begin Bytes.set s1 i1 c; succ i1 end
in
copy_code_in s1 (succ i) i1
else s1
in
if need_code 0 then
let len = compute_len 0 0 in copy_code_in (create len) 0 0
let len = compute_len 0 0 in
Bytes.to_string (copy_code_in (Bytes.create len) 0 0)
else s
let nl = "\013\010"
......@@ -176,7 +177,8 @@ let print_exc exc =
let print_err_exc exc = print_exc exc; flush stderr
let case_unsensitive_eq s1 s2 = lowercase s1 = lowercase s2
let case_unsensitive_eq s1 s2 =
Why3.Strings.lowercase s1 = Why3.Strings.lowercase s2
let rec extract_param name stop_char =
function
......@@ -196,26 +198,25 @@ let rec extract_param name stop_char =
else extract_param name stop_char l
| [] -> ""
let buff = ref (create 80)
let store len x =
if len >= String.length !buff then
buff := !buff ^ create (String.length !buff);
set !buff len x;
succ len
let get_buff len = String.sub !buff 0 len
let get_request strm =
let rec loop len (strm__ : _ Stream.t) =
let buff = Buffer.create 80 in
let rec loop (strm__ : _ Stream.t) =
match Stream.peek strm__ with
Some '\010' ->
Stream.junk strm__;
let s = strm__ in
if len == 0 then [] else let str = get_buff len in str :: loop 0 s
| Some '\013' -> Stream.junk strm__; loop len strm__
| Some c -> Stream.junk strm__; loop (store len c) strm__
| _ -> if len == 0 then [] else [get_buff len]
| Some '\010' ->
Stream.junk strm__;
if Buffer.length buff = 0 then []
else
let str = Buffer.contents buff in
let () = Buffer.clear buff in
str :: loop strm__
| Some '\013' -> Stream.junk strm__; loop strm__
| Some c ->
Stream.junk strm__;
Buffer.add_char buff c;
loop strm__
| _ -> if Buffer.length buff = 0 then [] else [Buffer.contents buff]
in
loop 0 strm
loop strm
let get_request_and_content strm =
let request = get_request strm in
......@@ -223,15 +224,11 @@ let get_request_and_content strm =
match extract_param "content-length: " ' ' request with
"" -> ""
| x ->
let str = create (int_of_string x) in
for i = 0 to String.length str - 1 do
set str i (
let (strm__ : _ Stream.t) = strm in
match Stream.peek strm__ with
Some x -> Stream.junk strm__; x
| _ -> ' ')
done;
str
String.init (int_of_string x) (fun _ ->
let (strm__ : _ Stream.t) = strm in
match Stream.peek strm__ with
| Some x -> Stream.junk strm__; x
| _ -> ' ')
in
request, content
......@@ -244,9 +241,9 @@ let sockaddr_of_string s = Unix.ADDR_UNIX s
let treat_connection _tmout callback addr fd fmt =
let (request, contents__) =
let strm =
let c = " " in
let c = Bytes.create 1 in
Stream.from
(fun _ -> if Unix.read fd c 0 1 = 1 then Some c.[0] else None)
(fun _ -> if Unix.read fd c 0 1 = 1 then Some (Bytes.get c 0) else None)
in
get_request_and_content strm
in
......
......@@ -491,10 +491,10 @@ let read_old_proof =
Vernacular
end in
let len = pos_in ch - !start in
let s = Strings.create len in
let s = Bytes.create len in
seek_in ch !start;
really_input ch s 0 len;
Query (name, k, s)
Query (name, k, Bytes.unsafe_to_string s)
with StringValue s -> Other s
(* Load old-style proofs where users were confined to a few sections. *)
......
......@@ -11,7 +11,7 @@
val compression_supported : bool
module type S = sig
module type S = sig
type out_channel
......@@ -19,7 +19,7 @@ val open_out: string -> out_channel
val output_char: out_channel -> char -> unit
val output: out_channel -> string -> int -> int -> unit
val output_substring: out_channel -> string -> int -> int -> unit
val output_string: out_channel -> string -> unit
......@@ -29,9 +29,9 @@ type in_channel
val open_in: string -> in_channel
val input: in_channel -> string -> int -> int -> int
val input: in_channel -> bytes -> int -> int -> int
val really_input: in_channel -> string -> int -> int -> unit
val really_input: in_channel -> bytes -> int -> int -> unit
val input_char: in_channel -> char
......
......@@ -9,9 +9,10 @@
(* *)
(********************************************************************)
#13 "src/session/compress_none.ml"
let compression_supported = false
module type S = sig
module type S = sig
type out_channel
......@@ -19,7 +20,7 @@ val open_out: string -> out_channel
val output_char: out_channel -> char -> unit
val output: out_channel -> string -> int -> int -> unit
val output_substring: out_channel -> string -> int -> int -> unit
val output_string: out_channel -> string -> unit
......@@ -29,9 +30,9 @@ type in_channel
val open_in: string -> in_channel
val input: in_channel -> string -> int -> int -> int
val input: in_channel -> bytes -> int -> int -> int
val really_input: in_channel -> string -> int -> int -> unit
val really_input: in_channel -> bytes -> int -> int -> unit
val input_char: in_channel -> char
......
......@@ -9,9 +9,10 @@
(* *)
(********************************************************************)
#13 "src/session/compress_z.ml"
let compression_supported = true
module type S = sig
module type S = sig
type out_channel
......@@ -19,7 +20,7 @@ val open_out: string -> out_channel
val output_char: out_channel -> char -> unit
val output: out_channel -> string -> int -> int -> unit
val output_substring: out_channel -> string -> int -> int -> unit
val output_string: out_channel -> string -> unit
......@@ -29,9 +30,9 @@ type in_channel
val open_in: string -> in_channel
val input: in_channel -> string -> int -> int -> int
val input: in_channel -> bytes -> int -> int -> int
val really_input: in_channel -> string -> int -> int -> unit
val really_input: in_channel -> bytes -> int -> int -> unit
val input_char: in_channel -> char
......@@ -50,9 +51,9 @@ let open_out fn = Gzip.open_out ~level:6 fn
let output_char = Gzip.output_char
let output = Gzip.output
let output_substring = Gzip.output_substring
let output_string ch s = output ch s 0 (String.length s)
let output_string ch s = output_substring ch s 0 (String.length s)
let close_out = Gzip.close_out
......
......@@ -799,8 +799,10 @@ end
(* Specific to auto-focus at initialization of itp_server *)
focus_on_label node;
P.notify (New_node (new_id, parent, node_type, node_name, node_detached));
(*
if node_type = NFile then
read_and_send node_name;
*)
get_node_proved new_id node;
new_id
......@@ -1001,6 +1003,7 @@ end
in
Debug.dprintf debug "sending initialization infos@.";
P.notify (Initialized infos);
load_files_session ();
Debug.dprintf debug "reloading source files@.";
let b = reload_files d.cont ~use_shapes in
if b then
......@@ -1011,8 +1014,6 @@ end
focus on a specific node. *)
get_focused_label := None
end
else
load_files_session ()
(* ----------------- Schedule proof attempt -------------------- *)
......@@ -1356,9 +1357,10 @@ end
end
| Add_file_req f ->
add_file_to_session d.cont f;
let f = Sysutil.relativize_filename
(* let f = Sysutil.relativize_filename
(Session_itp.get_dir d.cont.controller_session) f in
read_and_send f
read_and_send f *)
()
(*
| Open_session_req file_or_dir_name ->
let b = init_cont file_or_dir_name in
......
......@@ -1182,9 +1182,9 @@ exception ShapesFileError of string
module ReadShapes (C:Compress.S) = struct
let shape = Buffer.create 97
let sum = Strings.create 32
let read_sum_and_shape ch =
let sum = Bytes.create 32 in
let nsum = C.input ch sum 0 32 in
if nsum = 0 then raise End_of_file;
if nsum <> 32 then
......@@ -1195,7 +1195,7 @@ let read_sum_and_shape ch =
raise
(ShapesFileError
("shapes files corrupted (checksum '" ^
(String.sub sum 0 nsum) ^
(Bytes.sub_string sum 0 nsum) ^
"' too short), ignored"))
end;
if try C.input_char ch <> ' ' with End_of_file -> true then
......@@ -1211,7 +1211,7 @@ let read_sum_and_shape ch =
with
| End_of_file ->
raise (ShapesFileError "shapes files corrupted (premature end of file), ignored");
| Exit -> Strings.copy sum, Buffer.contents shape
| Exit -> Bytes.unsafe_to_string sum, Buffer.contents shape
let use_shapes = ref true
......
......@@ -81,7 +81,7 @@ let send_request = Protocol_shell.send_request
(* files of the current task *)
let files = Queue.create ()
let spec = Arg.align []
let spec = []
(* --help *)
let usage_str = Format.sprintf
......
......@@ -43,10 +43,7 @@ let cmdline_split s =
| '\\' -> cstate := Escape
| c when is_blank c ->
let n = Queue.length cur_arg in
let s = Strings.create n in
for i = 0 to pred n do
Strings.set s i (Queue.take cur_arg)
done;
let s = String.init n (fun _ -> Queue.take cur_arg) in
argv := s :: !argv;
cstate := Blank
| c -> Queue.add c cur_arg
......
......@@ -98,10 +98,10 @@ and string = parse
let nb = ref 0 in
String.iter (fun c -> if c = '_' then incr nb) s;
!nb in
let t = Strings.create (String.length s - count) in
let t = Bytes.create (String.length s - count) in
let i = ref 0 in
String.iter (fun c -> if c <> '_' then (Strings.set t !i c; incr i)) s;
t
String.iter (fun c -> if c <> '_' then (Bytes.set t !i c; incr i)) s;
Bytes.unsafe_to_string t
end else s
}
......@@ -209,9 +209,11 @@ let force_support support do_it v =
let simplify_max_int = BigInt.of_string "2147483646"
let remove_minus e =
if e.[0] = '-' then
(let e' = Strings.copy e in Strings.set e' 0 'm'; e')
else e
if e.[0] = '-' then begin
let e = Bytes.of_string e in
Bytes.set e 0 'm';
Bytes.unsafe_to_string e
end else e
let print_dec_int support fmt i =
let fallback i =
......
......@@ -64,20 +64,20 @@ let escape_string s =
| _ -> 1)
done;
if !n = String.length s then s else begin
let s' = Strings.create !n in
let s' = Bytes.create !n in
n := 0;
for i = 0 to String.length s - 1 do
let c = String.unsafe_get s i in
begin match c with
| ('"' | '\\' | '\n' | '\r' | '\t') ->
Strings.set s' !n '\\'; incr n
Bytes.set s' !n '\\'; incr n
| _ -> ()
end;
Strings.set s' !n
Bytes.set s' !n
(match c with '\n' -> 'n' | '\r' -> 'r' | '\t' -> 't' | _ -> c);
incr n
done;
s'
Bytes.unsafe_to_string s'
end
let print_rc_value fmt = function
......
......@@ -13,10 +13,6 @@
OCaml version at least 4.03.0 *)
let char_is_uppercase c = c = Char.uppercase c
let create = String.create
let copy = String.copy
let set = String.set
let lowercase = String.lowercase
let capitalize = String.capitalize
let uncapitalize = String.uncapitalize
......@@ -55,10 +51,10 @@ let rec join sep l =
let pad_right c s i =
let sl = String.length s in
if sl < i then
let p = create i in
String.blit s 0 p 0 sl;
String.fill p sl (i-sl) c;
p
let p = Bytes.create i in
Bytes.blit_string s 0 p 0 sl;
Bytes.fill p sl (i-sl) c;
Bytes.unsafe_to_string p
else if sl > i
then String.sub s 0 i
else s
......
......@@ -13,10 +13,6 @@
(** {2 Wrappers for deprecated string functions of OCaml stdlib} *)
val create : int -> string
val copy : string -> string
val set : string -> int -> char -> unit
val lowercase : string -> string
val capitalize : string -> string
val uncapitalize : string -> string
......
......@@ -17,22 +17,22 @@ let backup_file f =
end
let channel_contents_fmt cin fmt =
let buff = String.make 1024 ' ' in
let buff = Bytes.create 1024 in
let n = ref 0 in
while n := input cin buff 0 1024; !n <> 0 do
Format.pp_print_string fmt
(if !n = 1024 then
buff
Bytes.unsafe_to_string buff
else
String.sub buff 0 !n)
Bytes.sub_string buff 0 !n)
done
let channel_contents_buf cin =
let buf = Buffer.create 1024
and buff = String.make 1024 ' ' in
let buf = Buffer.create 1024 in
let buff = Bytes.create 1024 in
let n = ref 0 in
while n := input cin buff 0 1024; !n <> 0 do
Buffer.add_substring buf buff 0 !n
Buffer.add_subbytes buf buff 0 !n
done;
buf
......@@ -83,7 +83,7 @@ let open_temp_file ?(debug=false) filesuffix usefile =
let copy_file from to_ =
let cin = open_in from in
let cout = open_out to_ in
let buff = String.make 1024 ' ' in
let buff = Bytes.create 1024 in
let n = ref 0 in
while n := input cin buff 0 1024; !n <> 0 do
output cout buff 0 !n
......
......@@ -26,7 +26,7 @@ let opt_title = ref None
let opt_body = ref false
let opt_queue = Queue.create ()
let option_list = Arg.align [
let option_list = [
"-o", Arg.String (fun s -> opt_output := Some s),
"<dir> print files in <dir>";
"--output", Arg.String (fun s -> opt_output := Some s),
......
......@@ -279,7 +279,7 @@ let rec ask_yn () =
let ask_yn_nonblock ~callback =
let b = Buffer.create 3 in
let s = Strings.create 1 in
let s = Bytes.create 1 in
Format.printf "(y/n)@.";
fun () ->
match Unix.select [Unix.stdin] [] [] 0. with
......@@ -288,8 +288,9 @@ let ask_yn_nonblock ~callback =
if Unix.read Unix.stdin s 1 0 = 0 then
begin (* EndOfFile *) callback false; false end
else begin
if s.[0] <> '\n'
then (Buffer.add_char b s.[0]; true)
let c = Bytes.get s 0 in
if c <> '\n'
then (Buffer.add_char b c; true)
else
match Buffer.contents b with
| "y" -> callback true; false
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment