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
12f21150
Commit
12f21150
authored
Mar 25, 2010
by
Andrei Paskevich
Browse files
use zero separator only when there are several goals
parent
304617d7
Changes
2
Hide whitespace changes
Inline
Side-by-side
src/main.ml
View file @
12f21150
...
...
@@ -275,13 +275,14 @@ let do_file env drv src_filename_printer dest_filename_printer file =
match
!
output_file
with
|
None
->
()
|
Some
file
(* we are in the output file mode *)
->
List
.
iter
(
fun
(
th
,
task
,
drv
)
->
let
fmt
=
if
file
=
"-"
then
std_formatter
else
formatter_of_out_channel
(
open_out
file
)
in
fprintf
fmt
"%a
\000
@?"
(
Driver
.
print_task
drv
)
task
)
goals
let
fmt
=
if
file
=
"-"
then
std_formatter
else
formatter_of_out_channel
(
open_out
file
)
in
let
print_task
fmt
(
th
,
task
,
drv
)
=
fprintf
fmt
"@[%a@]"
(
Driver
.
print_task
drv
)
task
in
let
print_zero
fmt
()
=
fprintf
fmt
"
\000
@?"
in
fprintf
fmt
"%a@?"
(
Pp
.
print_list
print_zero
print_task
)
goals
end
;
if
!
call
then
(* we are in the call mode *)
...
...
src/printer/alt_ergo.ml
View file @
12f21150
...
...
@@ -153,7 +153,7 @@ let print_type_decl drv fmt = function
|
Driver
.
Tag
_
->
match
ts
.
ts_args
with
|
[]
->
fprintf
fmt
"type %a"
print_ident
ts
.
ts_name
;
true
|
_
->
fprintf
fmt
"type (%a)%a"
|
_
->
fprintf
fmt
"type (%a)
%a"
(
print_list
comma
print_tvsymbols
)
ts
.
ts_args
print_ident
ts
.
ts_name
;
true
end
...
...
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