Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
dc39e01f
Commit
dc39e01f
authored
Mar 25, 2013
by
Jean-Christophe Filliâtre
Browse files
fixed checksums
parent
73425da5
Changes
1
Show whitespace changes
Inline
Side-by-side
src/session/termcode.ml
View file @
dc39e01f
...
...
@@ -174,14 +174,13 @@ module Checksum = struct
let
option
e
b
=
function
None
->
char
b
'
n'
|
Some
x
->
char
b
'
s'
;
e
b
x
let
list
e
b
l
=
char
b
'
[
'
;
List
.
iter
(
e
b
)
l
;
char
b
'
]
'
(* let ident_printer = Ident.create_ident_printer [] *)
(* let ident b id = string b (Ident.id_unique ident_printer id) *)
let
hident
=
Ident
.
Hid
.
create
17
let
ident
=
let
ident
,
clear_ident
=
let
hident
=
Ident
.
Hid
.
create
17
in
let
c
=
ref
0
in
fun
b
id
->
(
fun
b
id
->
int
b
(
try
Ident
.
Hid
.
find
hident
id
with
Not_found
->
incr
c
;
Ident
.
Hid
.
add
hident
id
!
c
;
!
c
)
with
Not_found
->
incr
c
;
Ident
.
Hid
.
add
hident
id
!
c
;
!
c
))
,
(
fun
()
->
Ident
.
Hid
.
clear
hident
;
c
:=
0
)
let
const
b
c
=
let
buf
=
Buffer
.
create
17
in
...
...
@@ -319,9 +318,8 @@ module Checksum = struct
let
task
t
=
let
b
=
Buffer
.
create
8192
in
(* Ident.forget_all ident_printer; *)
Task
.
task_iter
(
tdecl
b
)
t
;
Ident
.
Hid
.
clear
h
ident
;
clear
_
ident
()
;
let
s
=
Buffer
.
contents
b
in
Digest
.
to_hex
(
Digest
.
string
s
)
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment