Commit 6689ab52 authored by MARCHE Claude's avatar MARCHE Claude

Make why3session.xml fully XML compliant

parent 16a73dbe
......@@ -216,6 +216,7 @@ install_no_local::
cp -f drivers/*.drv drivers/*.gen $(DATADIR)/why3/drivers
cp -f share/provers-detection-data.conf $(DATADIR)/why3/
cp -f share/images/*.png $(DATADIR)/why3/images
cp -f share/why3session.dtd $(DATADIR)/why3
cp -rf share/javascript $(DATADIR)/why3/javascript
cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el
cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang
......
......@@ -360,15 +360,26 @@ let save_ident fmt id =
let save_label fmt s =
fprintf fmt "@\n@[<v 1><label@ name=\"%s\"/>@]" s.Ident.lab_string
let save_string fmt s =
for i=0 to String.length s - 1 do
match String.get s i with
| '\"' -> pp_print_string fmt "&quot;"
| '\'' -> pp_print_string fmt "&apos;"
| '<' -> pp_print_string fmt "&lt;"
| '>' -> pp_print_string fmt "&gt;"
| '&' -> pp_print_string fmt "&amp;"
| c -> pp_print_char fmt c
done
let rec save_goal provers fmt g =
assert (g.goal_shape <> "");
fprintf fmt
"@\n@[<v 1><goal@ %a@ %asum=\"%s\"@ proved=\"%b\"@ \
expanded=\"%b\"@ shape=\"%s\">"
expanded=\"%b\"@ shape=\"%a\">"
save_ident g.goal_name
(opt "expl") g.goal_expl
g.goal_checksum g.goal_verified g.goal_expanded
g.goal_shape;
save_string g.goal_shape;
Ident.Slab.iter (save_label fmt) g.goal_name.Ident.id_label;
PHprover.iter (save_proof_attempt provers fmt) g.goal_external_proofs;
PHstr.iter (save_trans provers fmt) g.goal_transformations;
......
......@@ -167,9 +167,25 @@ and value = parse
and string_val = parse
| '"'
{ Buffer.contents buf }
| "&lt;"
{ Buffer.add_char buf '<';
string_val lexbuf }
| "&gt;"
{ Buffer.add_char buf '>';
string_val lexbuf }
| "&quot;"
{ Buffer.add_char buf '"';
string_val lexbuf }
| "&apos;"
{ Buffer.add_char buf '\'';
string_val lexbuf }
| "&amp;"
{ Buffer.add_char buf '&';
string_val lexbuf }
| [^ '\\' '"'] as c
{ Buffer.add_char buf c;
string_val lexbuf }
(*
| '\\' (['\\''\"'] as c)
{ Buffer.add_char buf c;
string_val lexbuf }
......@@ -180,6 +196,7 @@ and string_val = parse
{ Buffer.add_char buf '\\';
Buffer.add_char buf c;
string_val lexbuf }
*)
| eof
{ parse_error "unterminated string" }
......
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