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
e9c93948
Commit
e9c93948
authored
Oct 17, 2012
by
MARCHE Claude
Browse files
fixed filenames issues in session XML files
parent
05599d48
Changes
3
Hide whitespace changes
Inline
Side-by-side
examples/hello_proof/why3session.xml
View file @
e9c93948
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/us
ers/demons/melquion/src/why3/share
/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/us
r/local/share/why3
/why3session.dtd">
<why3session
name=
"./hello_proof/why3session.xml"
shape_version=
"2"
>
shape_version=
"2"
>
<prover
id=
"0"
name=
"Alt-Ergo"
...
...
@@ -9,7 +9,7 @@
<prover
id=
"1"
name=
"Coq"
version=
"8.3pl
4
"
/>
version=
"8.3pl
3
"
/>
<prover
id=
"2"
name=
"Simplify"
...
...
@@ -17,10 +17,10 @@
<file
name=
"../hello_proof.why"
verified=
"false"
expanded=
"
fals
e"
>
expanded=
"
tru
e"
>
<theory
name=
"HelloProof"
locfile=
".
/hello_proof/.
./hello_proof.why"
locfile=
"../hello_proof.why"
loclnum=
"1"
loccnumb=
"7"
loccnume=
"17"
verified=
"false"
expanded=
"true"
>
...
...
@@ -28,7 +28,7 @@
name=
"My very first Why3 theory"
/>
<goal
name=
"G1"
locfile=
".
/hello_proof/.
./hello_proof.why"
locfile=
"../hello_proof.why"
loclnum=
"3"
loccnumb=
"7"
loccnume=
"9"
sum=
"4daf9675e70ee6481b1153fe95f7c750"
proved=
"true"
...
...
@@ -45,7 +45,7 @@
</goal>
<goal
name=
"G2"
locfile=
".
/hello_proof/.
./hello_proof.why"
locfile=
"../hello_proof.why"
loclnum=
"5"
loccnumb=
"7"
loccnume=
"9"
sum=
"b16d2c9608c416dc0059ba3e95264abe"
proved=
"false"
...
...
@@ -73,7 +73,7 @@
expanded=
"true"
>
<goal
name=
"G2.1"
locfile=
".
/hello_proof/.
./hello_proof.why"
locfile=
"../hello_proof.why"
loclnum=
"5"
loccnumb=
"7"
loccnume=
"9"
sum=
"b84cad55140412a1b6f988cba7a0ebd1"
proved=
"false"
...
...
@@ -88,26 +88,26 @@
<result
status=
"unknown"
time=
"0.00"
/>
</proof>
<proof
prover=
"
2
"
prover=
"
1
"
timelimit=
"4"
memlimit=
"0"
edited=
"hello_proof_HelloProof_G2_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.
00
"
/>
<result
status=
"unknown"
time=
"0.
76
"
/>
</proof>
<proof
prover=
"
1
"
prover=
"
2
"
timelimit=
"4"
memlimit=
"0"
edited=
"hello_proof_HelloProof_G2_1.v"
obsolete=
"false"
archived=
"false"
>
<result
status=
"unknown"
time=
"0.
49
"
/>
<result
status=
"unknown"
time=
"0.
00
"
/>
</proof>
</goal>
<goal
name=
"G2.2"
locfile=
".
/hello_proof/.
./hello_proof.why"
locfile=
"../hello_proof.why"
loclnum=
"5"
loccnumb=
"7"
loccnume=
"9"
sum=
"fdf75c799e5829c6e57c69e76f88886a"
proved=
"true"
...
...
@@ -134,7 +134,7 @@
</goal>
<goal
name=
"G3"
locfile=
".
/hello_proof/.
./hello_proof.why"
locfile=
"../hello_proof.why"
loclnum=
"9"
loccnumb=
"7"
loccnume=
"9"
sum=
"e2296194dcf5f95896f599f6da2c8adf"
proved=
"true"
...
...
share/why3session.dtd
View file @
e9c93948
<!ELEMENT why3session (prover*, file*)>
<!ATTLIST why3session name CDATA #REQUIRED>
<!ATTLIST why3session shape_version CDATA #IMPLIED>
<!ELEMENT prover EMPTY>
...
...
src/session/session.ml
View file @
e9c93948
...
...
@@ -461,6 +461,7 @@ let goal_expl g = Util.def_option g.goal_name.Ident.id_string g.goal_expl
open
Format
let
db_filename
=
"why3session.xml"
let
session_dir_for_save
=
ref
"."
let
save_string
fmt
s
=
for
i
=
0
to
String
.
length
s
-
1
do
...
...
@@ -518,6 +519,7 @@ let save_ident fmt id =
|
None
->
()
|
Some
loc
->
let
file
,
lnum
,
cnumb
,
cnume
=
Loc
.
get
loc
in
let
file
=
Sysutil
.
relativize_filename
!
session_dir_for_save
file
in
fprintf
fmt
"@ locfile=
\"
%a
\"
@ loclnum=
\"
%i
\"
loccnumb=
\"
%i
\"
loccnume=
\"
%i
\"
"
save_string
file
lnum
cnumb
cnume
...
...
@@ -650,8 +652,13 @@ let save fname config session =
fprintf
fmt
"<!DOCTYPE why3session SYSTEM
\"
%a
\"
>@
\n
"
save_string
(
Filename
.
concat
(
Whyconf
.
datadir
(
Whyconf
.
get_main
config
))
"why3session.dtd"
);
(*
let rel_file = Sysutil.relativize_filename !session_dir_for_save fname in
fprintf fmt "@[<v 1><why3session@ name=\"%a\" shape_version=\"%d\">"
save_string
fname
session
.
session_shape_version
;
save_string rel_file session.session_shape_version;
*)
fprintf
fmt
"@[<v 1><why3session shape_version=
\"
%d
\"
>"
session
.
session_shape_version
;
let
provers
,_
=
Sprover
.
fold
(
save_prover
fmt
)
(
get_used_provers
session
)
(
Mprover
.
empty
,
0
)
in
PHstr
.
iter
(
save_file
provers
fmt
)
session
.
session_files
;
...
...
@@ -662,6 +669,7 @@ let save fname config session =
let
save_session
config
session
=
let
f
=
Filename
.
concat
session
.
session_dir
db_filename
in
Sysutil
.
backup_file
f
;
session_dir_for_save
:=
session
.
session_dir
;
save
f
config
session
(*******************************)
...
...
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