Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
e0149985
Commit
e0149985
authored
Jun 25, 2010
by
Andrei Paskevich
Browse files
hide builtin symbols (but not tuples) in print-namespace
parent
f112a95c
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/core/pretty.ml
View file @
e0149985
...
...
@@ -375,11 +375,21 @@ module NsTree = struct
let
contents
ns
=
let
add_ns
s
ns
acc
=
Namespace
(
s
,
ns
)
::
acc
in
let
add_s
k
s
_
acc
=
Leaf
(
k
^
s
)
::
acc
in
let
acc
=
Mnm
.
fold
add_ns
ns
.
ns_ns
[]
in
let
acc
=
Mnm
.
fold
(
add_s
"prop "
)
ns
.
ns_pr
acc
in
let
acc
=
Mnm
.
fold
(
add_s
"logic "
)
ns
.
ns_ls
acc
in
let
acc
=
Mnm
.
fold
(
add_s
"type "
)
ns
.
ns_ts
acc
in
acc
let
add_pr
s
_
acc
=
Leaf
(
"prop "
^
s
)
::
acc
in
let
add_ls
s
ls
acc
=
if
s
=
"infix ="
&&
ls_equal
ls
ps_equ
then
acc
else
if
s
=
"infix <>"
&&
ls_equal
ls
ps_neq
then
acc
else
Leaf
(
"logic "
^
s
)
::
acc
in
let
add_ts
s
ts
acc
=
if
s
=
"int"
&&
ts_equal
ts
ts_int
then
acc
else
if
s
=
"real"
&&
ts_equal
ts
ts_real
then
acc
else
Leaf
(
"type "
^
s
)
::
acc
in
let
acc
=
Mnm
.
fold
add_ns
ns
.
ns_ns
[]
in
let
acc
=
Mnm
.
fold
add_pr
ns
.
ns_pr
acc
in
let
acc
=
Mnm
.
fold
add_ls
ns
.
ns_ls
acc
in
let
acc
=
Mnm
.
fold
add_ts
ns
.
ns_ts
acc
in
acc
let
decomp
=
function
|
Namespace
(
s
,
ns
)
->
s
,
contents
ns
...
...
Write
Preview
Supports
Markdown
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